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

Authors: Alessandro Bezerra Trindade; Renato De Faria Degelo; Edilson Galvão Dos Santos Junior; Hussama Ibrahim Ismail; Helder Cruz Da Silva; Lucas Carvalho Cordeiro

Addresses: Federal University of Amazonas, Av. Rodrigo Otávio, 3000, Campus Universitário, Manaus, ZIP 69077-000, Brazil ' Federal University of Amazonas, Av. Rodrigo Otávio, 3000, Campus Universitário, Manaus, ZIP 69077-000, Brazil ' Federal University of Amazonas, Av. Rodrigo Otávio, 3000, Campus Universitário, Manaus, ZIP 69077-000, Brazil ' Federal University of Amazonas, Av. Rodrigo Otávio, 3000, Campus Universitário, Manaus, ZIP 69077-000, Brazil ' Federal University of Amazonas, Av. Rodrigo Otávio, 3000, Campus Universitário, Manaus, ZIP 69077-000, Brazil ' Federal University of Amazonas, Av. Rodrigo Otávio, 3000, Campus Universitário, Manaus, ZIP 69077-000, Brazil

Abstract: 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.

Keywords: hardware-software co-design; hardware-software partitioning; optimisation; model checking; multi-core; maximum satisfiability; MaxSAT.

DOI: 10.1504/IJES.2017.088044

International Journal of Embedded Systems, 2017 Vol.9 No.6, pp.570 - 582

Received: 19 Dec 2015
Accepted: 22 Sep 2016

Published online: 20 Nov 2017 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article