Applying multi-core model checking to hardware-software partitioning in embedded systems

Alessandro Trindade, Hussama Ismail, Lucas Cordeiro

Research output: Contribution to journalArticlepeer-review


We present an alternative approach to solve the hardware and software partitioning problem, which uses Bounded Model Checking (BMC) based on Satisfiability Modulo Theories (SMT) in conjunction with a multi-core support using Open Multi-Processing. The multi-core approach allows initializing many verification instances based on processors cores numbers available to the model checker. Each instance checks for a different optimum value until the optimization problem is satisfied. The goal is to show that multi-core model-checking techniques can be effective, in particular cases, to find the optimal solution of the hardware-software partitioning problem. We compare the experimental results of our proposed approach with conventional algorithms.
Original languageEnglish
Pages (from-to)102-105
JournalBrazilian Symposium on Computing System Engineering : proceedings
Publication statusPublished - 2015


  • hardware-software co-design
  • hardware-software partitioning
  • optimization
  • model checking
  • multi-core
  • OpenMP


Dive into the research topics of 'Applying multi-core model checking to hardware-software partitioning in embedded systems'. Together they form a unique fingerprint.

Cite this