# Improving Symbolic System-Level Synthesis by Solver Coordination and Domain-Specific Heuristics
## 2 Coordinated SMT-Based Synthesis Approach: Motivation & Detailed Overview
### (Classical) SMT-Based System Synthesis  
Figure 2 illustrates the elements of SMT-based synthesis. For the _classical_ synthesis approach, all shown elements are vital, except the two boxes in green and cyan, those are part of our extension within the _coordinated_ synthesis approach. The system specification is the starting point. It consists both of an instance of our application model and platform model (yellow boxes in Figure 2) for which we decide a binding, routing and scheduling during synthesis. Our platform model focuses on scalable tile-based architectures implementing a NoC [4]. Furthermore, our graph-based application model is geared to real-world periodic control applications with hard real-time constraints from the automotive domain. The system specification is an input for the logic solver which decides the static binding of periodic computational tasks from the application model to processing elements (PEs) of the platform model. Furthermore, the logic solver computes the static multi-hop routing of periodic messages between computational tasks. It is important to note that our synthesis approach employs an answer set solver from the area of answer set programming (ASP) [11; 12; 13] as logic solver in contrast to most related approaches that use a Pseudo-Boolean SAT solver for the same task. Here, related work [14] encouraged us to favor an answer set solver since ASP allows a more scalable determination of multi-hop routes of messages for densely connected hardware architectures implementing a NoC. With the logic solver computing a binding and routing implementation candidate, this solution is subsequently passed to the \(\mathcal{T}\)-solver for a scheduling analysis. Here, scheduling instances are generated on basis of _indicator variables_ that have an interpretation in both the logic solver as in the \(\mathcal{T}\)-solver. These indicator variables are also used to express feedback of the \(\mathcal{T}\)-solver to the logic solver in order to learn unschedulable bindings and routings. In our approach, the indicator variables correspond to the binding of a computational task to a PE and the hops in the route of a message. Deciding the scheduling in the background theory solver to resolve resource access conflicts assumes a time-triggered scheduling policy on all resources of the hardware platform. Here, each computational task on a PE and each packet of a message on each resource on the message's route through the NoC is assigned a dedicated start time. At this start time, the resource starts the associated computations or the transfer of a packet. The \(\mathcal{T}\)-solver decides whether a time-triggered schedule exists such that all timing constraints of computational tasks and messages are satisfied. If a schedule exists for all computational tasks and all messages based on the logic solver's binding and routing decisions, the synthesis stops and returns a feasible implementation. However, in the first iteration of SMT-based synthesis approaches it is unlikely that the background theory will find a feasible scheduling right at the start. Usually, the \(\mathcal{T}\)-solver proves that early bindings and routes computed by the logic solver cannot be scheduled. Similar to other work [7], in order to speed up the time to decide schedulability, we propose a hierarchical scheduling scheme (orange box in Figure 2). In our hierarchical scheduling scheme, the \(\mathcal{T}\)-solver decides feasibility of smaller sub-problems before the feasibility of the scheduling for the complete system is decided. Usually proving the infeasibility of  
Figure 2: Detailed overview of SMT-based system synthesis with the extensions of the scheduling-aware binding and routing refinement (green box) in the _coordinated_ synthesis approach and the _coordinated+DSH_ approach (green and cyan box). small sub-problems is much faster than proving the infeasibility of the complete system scheduling. If a sub-problem is already deemed infeasible it follows that the complete system cannot be scheduled.