Efficient SAT-based application mapping and scheduling on multiprocessor systems for throughput maximization

Multiprocessor systems are becoming ubiquitous in today´s embedded systems design. In this paper, we address the problem of mapping an application represented by a Homogeneous Synchronous Dataflow (HSDF) graph onto a real-time multiprocessor platform with the objective of maximizing total throughput. We propose that the optimal solution to the problem is composed of three components: actor-to-processor mapping, retiming, and actor ordering on each processor. The entire problem is systematically modeled into a SAT problem and solved by a modern SAT solver formally such that the optimal solution can be guaranteed. In order to explore the vast solution space more efficiently, we develop a specific HSDF theory solver based on the special characteristics of the timed HSDF, and integrate it into the general search framework of the SAT solver. The enhanced optimization framework implemented in branch and bound is able to conduct early branch pruning in the search space, and the scalability is thus greatly improved. Extensive performance evaluation on synthetic examples and a case study on the realistic H.264 Video Decoder shows that our technique provides as much as 76.9% throughput improvement, and it is scalable to industry-sized applications.