Applying SMT-based verification to hardware/software partitioning in embedded systemsCitation formats

Standard

Applying SMT-based verification to hardware/software partitioning in embedded systems. / Trindade, Alessandro B.; Cordeiro, Lucas C.

In: Design Automation for Embedded Systems, Vol. 20, No. 1, 22.04.2015, p. 1-19.

Research output: Contribution to journalArticle

Harvard

APA

Vancouver

Author

Trindade, Alessandro B. ; Cordeiro, Lucas C. / Applying SMT-based verification to hardware/software partitioning in embedded systems. In: Design Automation for Embedded Systems. 2015 ; Vol. 20, No. 1. pp. 1-19.

Bibtex

@article{dc4628de790d47a18d4c0ee1e7d2e757,
title = "Applying SMT-based verification to hardware/software partitioning in embedded systems",
abstract = "When performing hardware/software co-design for embedded systems, the problem of which functions of the system should be implemented in hardware (HW) or in software (SW) emerges. This problem is known as HW/SW partitioning. Over the last 10 years, a significant research effort has been carried out in this area. In this paper, we present two new approaches to solve the HW/SW partitioning problem by using verification techniques based on satisfiability modulo theories (SMT). We compare the results using the traditional technique of integer linear programming, specifically binary integer programming and a modern method of optimization by genetic algorithm. The experimental results show that SMT-based verification techniques can be effective in particular cases to solve the HW/SW partition problem optimally using a state-of-the-art model checker based on SMT solvers, when compared against traditional techniques.",
keywords = "Hardware/software co-design, Embedded systems, Partitioning, Binary integer programming, Genetic algorithm, Formal verification",
author = "Trindade, {Alessandro B.} and Cordeiro, {Lucas C.}",
year = "2015",
month = "4",
day = "22",
doi = "10.1007/s10617-015-9163-z",
language = "English",
volume = "20",
pages = "1--19",
journal = "Design Automation for Embedded Systems",
issn = "0929-5585",
publisher = "Springer Nature",
number = "1",

}

RIS

TY - JOUR

T1 - Applying SMT-based verification to hardware/software partitioning in embedded systems

AU - Trindade, Alessandro B.

AU - Cordeiro, Lucas C.

PY - 2015/4/22

Y1 - 2015/4/22

N2 - When performing hardware/software co-design for embedded systems, the problem of which functions of the system should be implemented in hardware (HW) or in software (SW) emerges. This problem is known as HW/SW partitioning. Over the last 10 years, a significant research effort has been carried out in this area. In this paper, we present two new approaches to solve the HW/SW partitioning problem by using verification techniques based on satisfiability modulo theories (SMT). We compare the results using the traditional technique of integer linear programming, specifically binary integer programming and a modern method of optimization by genetic algorithm. The experimental results show that SMT-based verification techniques can be effective in particular cases to solve the HW/SW partition problem optimally using a state-of-the-art model checker based on SMT solvers, when compared against traditional techniques.

AB - When performing hardware/software co-design for embedded systems, the problem of which functions of the system should be implemented in hardware (HW) or in software (SW) emerges. This problem is known as HW/SW partitioning. Over the last 10 years, a significant research effort has been carried out in this area. In this paper, we present two new approaches to solve the HW/SW partitioning problem by using verification techniques based on satisfiability modulo theories (SMT). We compare the results using the traditional technique of integer linear programming, specifically binary integer programming and a modern method of optimization by genetic algorithm. The experimental results show that SMT-based verification techniques can be effective in particular cases to solve the HW/SW partition problem optimally using a state-of-the-art model checker based on SMT solvers, when compared against traditional techniques.

KW - Hardware/software co-design

KW - Embedded systems

KW - Partitioning

KW - Binary integer programming

KW - Genetic algorithm

KW - Formal verification

U2 - 10.1007/s10617-015-9163-z

DO - 10.1007/s10617-015-9163-z

M3 - Article

VL - 20

SP - 1

EP - 19

JO - Design Automation for Embedded Systems

JF - Design Automation for Embedded Systems

SN - 0929-5585

IS - 1

ER -