Multicore SMT-BMC for Embedded Co-Design: MaxSMT-Aided Hardware/Software Partitioning at Scale

• Monisha Rengaraj

  Author

This paper targets hardware/software partitioning in embedded systems as a first-class design automation problem, presenting a multicore Bounded Model Checking (BMC) workflow that accelerates exact optimization under real system constraints. The proposed approach parallelizes Satisfiability Modulo Theories (SMT)-based verification with Open Multi-Processing (OpenMP) and augments it with a Maximum Satisfiability Modulo Theories (MaxSMT) backend (vZ) to minimize hardware cost while satisfying software and communication constraints on task-graph models used in co-design. A family of implementations, including the sequential Efficient SMT-Based Context-Bounded Model Checker (ESBMC), multicore ESBMC with sequential, worker, and binary-search controllers, and an ESBMC-(vZ) integration, is developed to exploit contemporary multicore processors without modifying the underlying solver backends. Comparative evaluation against Integer Linear Programming (ILP) and Genetic Algorithm (GA) approaches across standard embedded-system benchmarks (e.g., CRC32, Patricia, Dijkstra, Clustering, RC6, Fuzzy, and Mars) quantifies runtime, optimality, and scalability. The results demonstrate that the MaxSMT-based ESBMC approach achieves superior performance on small-to-medium problem instances, whereas the multicore ESBMC with a parallel binary-search controller (ESBMC-PB) provides substantial speedups for larger task graphs. These findings offer practical guidance for hardware/software co-design workflows: employ ESBMC-(vZ) when exact optimality and rapid turnaround are priorities, utilize multicore ESBMC-PB for large design spaces, and reserve GA for scenarios where approximate solutions are acceptable. Overall, the proposed contributions establish a practical Computer Engineering (CE) design-automation pipeline that effectively integrates formal optimization with parallel verification to address hardware/software trade-offs in embedded system architectures.

• PDF

Copyright (c) 2026 International Journal of Intelligent Systems and Data Science

This work is licensed under a Creative Commons Attribution 4.0 International License.