# Improving Symbolic System-Level Synthesis by Solver Coordination and Domain-Specific Heuristics
## 3 Related Work
[PERSON] and [PERSON] [7] present an SMT-based architecture optimization and scheduling approach. While they focus on time-triggered automotive bus systems, the authors implement several techniques that are also used within the work at hand, e.g., a hierarchical scheduling scheme to increase performance. All the work discussed above leverages (PB-)SAT-solvers as logic solvers in their SMT-based approaches. In [14], [PERSON] et al. show that using answer set programming (ASP) [11; 13] has advantages for highly connected architectures. While their work does not include a background theory to decide scheduling, their work shows that deciding the multi-hop routes of messages is more scalable for NoC-based architectures. Hence, their work encouraged us to leverage ASP to decide the binding and multi-hop routing in our synthesis approach. Regarding ASP and a coupling to a background theory for system synthesis, [PERSON] et al. [9] tightly couple answer set programming with the same background theory as in this paper for scheduling analysis. By leveraging technical advances in a new version of the answer set solver clingo [24] the authors are able to analyze incomplete models which was not possible at the time we developed our _coordinated_ approach. An additional difference to our work is that the authors do not use a hierarchical scheduling scheme and do not investigate the influence of domain-specific heuristics (DSH) in their approach. Furthermore, the experiments in [9] indicate that our _coordinated_ approach based on _partial models_ can have advantages w.r.t. the total synthesis time for feasible system specifications. An extension of the work in [9] can be found in [25]. While the same limitations in comparison to our work exist as in [9], the novelty of [25] lies in the integration of a multi-objective optimization into the background theory allowing for an automatic design space exploration. This extension is orthogonal to our work. Note that all related work presented above does not consider a coordination between the logic solver and the background theory. As we will show in our experimental section (cf. Section 8), an approach without coordination considerably suffers applicability as the feedback by the \(\mathcal{T}\)-solver might not be provided within a reasonable amount of time. Furthermore, we investigate how symbolic system synthesis can be enhanced by domain-specific heuristics within the logic solver in order to increase scalability and robustness. Our approach is based on previous preliminary work [26; 27] that has been extended with refinements in several directions. The work at hand uses a portfolio solving approach in the background theory (see Section 8.2), also in order to show that the _classical_ approach does only scale to a certain limit even if different strategies and configurations are used within the background theory. Additionally, a scheduling constraint within the logic solver (the so-called Korst-constraint, see Section 5) considerably reduces couplings between logic solver and background theory and, to the best of our knowledge, has not been implemented in related symbolic synthesis approaches before. Regarding the modeling of more realistic applications, e.g., from the automotive domain, our application model is based on two terminal series-parallel (TTSP) application graphs [28] that capturing characteristics of today's and future automotive software for (massively) parallel hardware architectures. In our experiments, we evaluated our approach on considerably harder benchmarking instances incorporating TTSP application graphs as compared to [26; 27].