TY - GEN
T1 - Model reduction techniques for the formal verification of hardware dependent software
AU - Ecker, Wolfgang
AU - Esen, Volkan
AU - Findenig, Rainer Leonhard
AU - Steininger, Thomas
AU - Velten, Michael
PY - 2010
Y1 - 2010
N2 - Contemporary researches provide many solutions for formally verifying both hardware and software systems. In this paper, we describe the formal verification of assembly programs, which are part of the HW/SW interface in hybrid systems. We have developed several methods to model assembly programs in VHDL in order to verify their functionality. Our discussion will show that, by applying different reduction methods, we managed to formally verify the correctness of iterative algorithms with execution times higher than 6000 clock cycles.
AB - Contemporary researches provide many solutions for formally verifying both hardware and software systems. In this paper, we describe the formal verification of assembly programs, which are part of the HW/SW interface in hybrid systems. We have developed several methods to model assembly programs in VHDL in order to verify their functionality. Our discussion will show that, by applying different reduction methods, we managed to formally verify the correctness of iterative algorithms with execution times higher than 6000 clock cycles.
KW - Control flow analysis
KW - Correctness of assembly programs
KW - Cycle accurate modeling
KW - Cycle optimized modeling
KW - Formal verification
UR - http://www.scopus.com/inward/record.url?scp=77958135588&partnerID=8YFLogxK
U2 - 10.1109/HLDVT.2010.5496647
DO - 10.1109/HLDVT.2010.5496647
M3 - Conference contribution
SN - 9781424478057
T3 - Proceedings - IEEE International High-Level Design Validation and Test Workshop, HLDVT
SP - 148
EP - 153
BT - HLDVT'10 - IEEE International High Level Design Validation and Test Workshop, Conference Proceedings
PB - IEEE
T2 - High Level Design Validation and Test Workshop (HLDVT)
Y2 - 11 June 2010 through 12 June 2010
ER -