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

被引：0
作者：
Alessandro B. Trindade
Lucas C. Cordeiro
机构：
[1] Federal University of Amazonas (UFAM),Electronic and Information Research Center
来源：
Design Automation for Embedded Systems | 2016年 / 20卷
关键词：
Hardware/software co-design; Embedded systems; Partitioning; Binary integer programming; Genetic algorithm ; Formal verification;
D O I：
暂无
中图分类号：
学科分类号：
摘要：
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.
引用
收藏
页码：1 / 19
页数：18
相关论文
共 27 条
  • [1] Clarke E(2009)Model checking: algorithmic verification and debugging Commun ACM 52 74-84
  • [2] Emerson E(2004)A tool for checking ANSI-C programs Proc Tools Algorithms Constr Anal Syst LNCS 2988 168-176
  • [3] Sifakis J(2006)Bounded model checking of software using SMT solvers instead of SAT solvers SPIN LNCS 3925 146-162
  • [4] Clarke E(2009)Bounded model checking of software using SMT solvers instead of SAT solvers Int J Softw Tools Technol Transfer 11 69-83
  • [5] Kroening D(2012)SMT-based bounded model checking for embedded ANSI-C software IEEE Trans Softw Eng 38 957-974
  • [6] Lerda F(2004)An integer programming formulation for a case study in university timetabling Eur J Oper Res 153 117-135
  • [7] Armando A(2005)Algorithmic aspects of hardware/software partitioning ACM Trans Des Autom Electron Syst (TODAES) 10 136-156
  • [8] Mantovani J(2006)Application partitioning on programmable platforms using the ant colony optimization J Embed Comput Embed Process Syst 2 119-136
  • [9] Platania L(2010)Algorithmic aspects of hardware/software partitioning: 1D search algorithms IEEE Trans Comput 59 532-544
  • [10] Armando A(undefined)undefined undefined undefined undefined-undefined
123