# Improving Symbolic System-Level Synthesis by Solver Coordination and Domain-Specific Heuristics
## 1 Introduction  
In the process of developing a novel embedded system, developers often start at the electronic system level. During system synthesis, the fundamental design decision _binding, routing_ and _scheduling_ are decided [1]. A binding contains for each computational task of an application model an assignment to a processing element (PE) of a platform model. If information between computational tasks is exchanged via messages, a routing for each message consists of an ordered set of connected hardware resources. Finally, scheduling resolves concurrent access to shared resources by applying a suitable policy. In recent years, system synthesis has become more and more challenging due to increasing system complexity. Concerning the automotive domain, one major contribution to this complexity are parallel hardware architectures. These parallel architectures have become a necessity in the control-dominated systems in the automotive industry in order to meet performance requirements, e.g., due to customer demands for new features or the need to implement sophisticated algorithms to meet environmental goals. While multi-core architectures offer enough performance to realize the currently requested requirements [2], many-core architectures will become necessary in the foreseeable future. Regarding the interconnect implemented by these hardware architectures, it is likely that one or more network-on-chip (NoC) interconnects are a reasonable choice as they scale well with an increasing number of PEs and are very power-efficient [3; 4]. Despite that many-core architectures with NoCs offer scalable performance, they introduce a new set of challenges for system synthesis in control-dominated domains like the automotive domain. First of all, synthesis approaches have to handle a significant increase in the number of entities for which binding, routing and scheduling have to be decided. Additionally, and most of the time far more challenging, the timing constraints of automotive hard real-time applications have to be satisfied. Here, satisfying the timing constraints becomes a considerably challenging task if system specifications become more intricate and decisions during synthesis become interdependent. As manual approaches are likely to fail in this setting, symbolic approaches based on satisfiability modulo theories (SMT) emerged as scalable automated decision making approaches in the area of system synthesis, e.g., [5; 6; 7]. In SMT-based system synthesis, the workload of synthesis is split between a logic solver and a background theory solver (\(\mathcal{T}\)-solver), see Figure 1. This decoupling enables more scalable symbolic synthesis for hard real-time systems [6]. In the paper at hand, similar to [6], the logic solver decides the binding of computational tasks to PEs of the hardware architecture and the multi-hop routing of messages. These decisions are then the input for the \(\mathcal{T}\)-solver in order to decide schedulability of the logic solver's assignments. Thus, the solution space for the \(\mathcal{T}\)-solver is constrained. If the \(\mathcal{T}\)-solver proves that there exists no feasible schedule with respect to the decided binding and routing, the background theory computes a _feedback_ that allows to prune the search space of the logic solver. With this feedback, the SMT-based synthesis is able to learn infeasible solutions and therefore is able to avoid them in the subsequent search process. Unfortunately, as we will show in the experimental section (Section 8) of this paper, one can observe that deciding schedulability based on the logic solver's decisions might consume an excessive amount of time if the logic solver is allowed to perform its decisions in arbitrary orders and particularly without knowledge of the downstream scheduling task. As a result, the feedback of the background theory is considerably deferred, hence limiting the applicability and scalability of SMT-based system synthesis.