Multi-core model checking and maximum satisfiability applied to hardware-software partitioning

Alessandro Bezerra Trindade, Renato De Faria Degelo, Edilson Galvao Dos Santos Junior, Hussama Ibrahim Ismail, Helder Cruz Da Silva, Lucas Carvalho Cordeiro

Research output: Contribution to journalArticlepeer-review

258 Downloads (Pure)


Bounded model checking (BMC) based on satisfiability modulo theories (SMT) is well-known by its capability to verify software. However, its use as optimisation tool, to solve hardware and software (HW-SW) partitioning problems, is something new. In particular, its integration with the maximum satisfiability solver vZ tool, which provides a portfolio of approaches for solving linear optimisation problems over SMT formulas, is unprecedented. We present new alternative approaches to solve the HW-SW partitioning problem. First, we use SMT-based BMC in conjunction with a multi-core support using open multi-processing to create four variants to solve the partitioning problem. The multi-core SMT-based BMC approaches allow initialising many verification instances based on the number of available processing cores, where each instance checks a different optimum value until the optimisation problem is satisfied. Additionally, we integrate the vZ into the BMC, making it a specialised solution for optimisation in a single-core environment. We implement all five approaches on top of the efficient SMT-based context-bounded model checker (ESBMC) and compare them to a state-of-the-art optimisation tool. Experimental results show that there is no single optimisation tool to solve all HW-SW partitioning benchmarks, but based on medium-size benchmarks, ESBMC-vZ had better performance.
Original languageEnglish
Pages (from-to)570
JournalInternational Journal of Embedded Systems
Issue number6
Publication statusPublished - 2017


Dive into the research topics of 'Multi-core model checking and maximum satisfiability applied to hardware-software partitioning'. Together they form a unique fingerprint.

Cite this