Towards Tight Interaction of ASP and SMT Solving for System-Level Decision Making

Conference: ARCS 2014 - 27th International Conference on Architecture of Computing Systems
02/25/2014 - 02/28/2014 at Luebeck, Deutschland

Proceedings: ARCS 2014

Pages: 7Language: englishTyp: PDF

Personal VDE Members are entitled to a 10% discount on this title

Biewer, Alexander; Gladigau, Jens (Robert Bosch GmbH, Germany)
Haubelt, Christian (Applied Microelectronics and Computer Engineering, University of Rostock, Germany)

Future embedded real-time systems require more performance to fulfill customer demands. Many-core architectures implementing a network-on-chip (NoC) are proposed as scalable solutions. Software execution on such many-core architectures requires fundamental design decisions: spatial binding of software components to processing elements, multi-hop transaction routing, and scheduling for shared resources. Amongst others, respecting intrinsic many-core platform properties like non-uniform memory access (NUMA) and contention on the NoC is crucial. As a remedy, we introduce a formal model as key enabler for the system-level decision making process for embedded control applications. Thereby, the system model allows for a correct-by-construction decision making approach. In this paper, we propose to exploit answer set programming (ASP) to compute spatial bindings and multi-hop routes for communication, combined with a satisfiability modulo theories (SMT) solver providing scheduling decisions. Further, we present the dedicated ASP encoding and early experimental results. In the context of related work, we then highlight directions to further pursue the proposed approach.