Applying SMT-based verification to hardware/software partitioning in embedded systems

Alessandro B. Trindade, Lucas C. Cordeiro

Research output: Contribution to journalArticlepeer-review


When performing hardware/software co-design for embedded systems, the problem of which functions of the system should be implemented in hardware (HW) or in software (SW) emerges. This problem is known as HW/SW partitioning. Over the last 10 years, a significant research effort has been carried out in this area. In this paper, we present two new approaches to solve the HW/SW partitioning problem by using verification techniques based on satisfiability modulo theories (SMT). We compare the results using the traditional technique of integer linear programming, specifically binary integer programming and a modern method of optimization by genetic algorithm. The experimental results show that SMT-based verification techniques can be effective in particular cases to solve the HW/SW partition problem optimally using a state-of-the-art model checker based on SMT solvers, when compared against traditional techniques.
Original languageEnglish
Pages (from-to)1-19
JournalDesign Automation for Embedded Systems
Issue number1
Publication statusPublished - 22 Apr 2015


  • Hardware/software co-design
  • Embedded systems
  • Partitioning
  • Binary integer programming
  • Genetic algorithm
  • Formal verification


Dive into the research topics of 'Applying SMT-based verification to hardware/software partitioning in embedded systems'. Together they form a unique fingerprint.

Cite this