Efficient SAT-Based Mapping and Scheduling of Homogeneous Synchronous Dataflow Graphs for Throughput Optimization

As Moore´s law comes to an end, multiprocessor systems are becoming ubiquitous in today´s embedded systems design. In this paper, we address the problem of mapping a homogeneous synchronous dataflow (HSDF) graph onto a multiprocessor platform with the objective of maximizing system throughput. We present two optimization approaches based on branch-and-bound and SAT-solving to explore the design space of all possible actor-to-processor mappings and static order schedules on each processor. In the logic-based benders decomposition (LBBD) approach, we decompose the problem into a master problem of finding a feasible actor mapping and scheduling, and a sub-problem of deadlock-checking and throughput computation. In the integrated approach, we integrate branch-and-bound search into the SAT engine to achieve more effective search tree pruning and better scalability. Performance evaluation shows that the integrated approach outperforms the LBBD approach by a large margin.