Applying Multi-core Model Checking to Hardware-Software Partitioning in Embedded Systems
Alessandro Bezerra Trindade, Hussama Ibrahim Ismail, Lucas Carvalho Cordeiro · 2015
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.