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

  • External authors:
  • Alessandro Bezerra Trindade
  • Renato De Faria Degelo
  • Edilson Galvao Dos Santos Junior
  • Hussama Ibrahim Ismail
  • Helder Cruz Da Silva

Standard

Multi-core model checking and maximum satisfiability applied to hardware-software partitioning. / Trindade, Alessandro Bezerra; Degelo, Renato De Faria; Galvao Dos Santos Junior, Edilson; Ismail, Hussama Ibrahim; Silva, Helder Cruz Da; Cordeiro, Lucas Carvalho.

In: International Journal of Embedded Systems, Vol. 9, No. 6, 2017, p. 570.

Research output: Contribution to journalArticle

Harvard

Trindade, AB, Degelo, RDF, Galvao Dos Santos Junior, E, Ismail, HI, Silva, HCD & Cordeiro, LC 2017, 'Multi-core model checking and maximum satisfiability applied to hardware-software partitioning', International Journal of Embedded Systems, vol. 9, no. 6, pp. 570. https://doi.org/10.1504/IJES.2017.088044

APA

Trindade, A. B., Degelo, R. D. F., Galvao Dos Santos Junior, E., Ismail, H. I., Silva, H. C. D., & Cordeiro, L. C. (2017). Multi-core model checking and maximum satisfiability applied to hardware-software partitioning. International Journal of Embedded Systems, 9(6), 570. https://doi.org/10.1504/IJES.2017.088044

Vancouver

Trindade AB, Degelo RDF, Galvao Dos Santos Junior E, Ismail HI, Silva HCD, Cordeiro LC. Multi-core model checking and maximum satisfiability applied to hardware-software partitioning. International Journal of Embedded Systems. 2017;9(6):570. https://doi.org/10.1504/IJES.2017.088044

Author

Trindade, Alessandro Bezerra ; Degelo, Renato De Faria ; Galvao Dos Santos Junior, Edilson ; Ismail, Hussama Ibrahim ; Silva, Helder Cruz Da ; Cordeiro, Lucas Carvalho. / Multi-core model checking and maximum satisfiability applied to hardware-software partitioning. In: International Journal of Embedded Systems. 2017 ; Vol. 9, No. 6. pp. 570.

Bibtex

@article{d00fdad3addb4c31bb62027ab923a15e,
title = "Multi-core model checking and maximum satisfiability applied to hardware-software partitioning",
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.",
author = "Trindade, {Alessandro Bezerra} and Degelo, {Renato De Faria} and {Galvao Dos Santos Junior}, Edilson and Ismail, {Hussama Ibrahim} and Silva, {Helder Cruz Da} and Cordeiro, {Lucas Carvalho}",
year = "2017",
doi = "10.1504/IJES.2017.088044",
language = "English",
volume = "9",
pages = "570",
journal = "International Journal of Embedded Systems",
issn = "1741-1068",
publisher = "Inderscience Enterprises Ltd",
number = "6",

}

RIS

TY - JOUR

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

AU - Trindade, Alessandro Bezerra

AU - Degelo, Renato De Faria

AU - Galvao Dos Santos Junior, Edilson

AU - Ismail, Hussama Ibrahim

AU - Silva, Helder Cruz Da

AU - Cordeiro, Lucas Carvalho

PY - 2017

Y1 - 2017

N2 - 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.

AB - 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.

U2 - 10.1504/IJES.2017.088044

DO - 10.1504/IJES.2017.088044

M3 - Article

VL - 9

SP - 570

JO - International Journal of Embedded Systems

JF - International Journal of Embedded Systems

SN - 1741-1068

IS - 6

ER -