DocumentCode :
2472447
Title :
Early outpoint insertion for high-level software vs. RTL formal combinational equivalence verification
Author :
Feng, Xiushan ; Hu, Alan J.
Author_Institution :
Dept. of Comput. Sci., British Columbia Univ., Vancouver, BC
fYear :
0
fDate :
0-0 0
Firstpage :
1063
Lastpage :
1068
Abstract :
Ever-growing complexity is forcing design to move above RTL. For example, golden functional models are being written as clearly as possible in software and not optimized or intended for synthesis. Thus, equivalence verification between the high-level software functional model and the RTL is needed. The typical approach is to convert the high-level software into RTL or gate-level hardware, via software path enumeration, symbolic execution, or high-level synthesis techniques, and then use hardware combinational equivalence checking. The principle contribution of this paper is to introduce cutpoints - as in gate-level combinational equivalence verification - early during the analysis of the software model, thereby avoiding exponential path enumeration and the potential logical complexity blow-up of merging execution paths that can occur in the usual approach. The method is conservative, but in our experiments, we did not encounter spurious counterexamples, and the method showed large improvements in runtime and memory usage on a family of IA-32 subset instruction length decoders, an industry-suggested challenge problem
Keywords :
computational complexity; equivalence classes; formal verification; high level synthesis; RTL; combinational equivalence verification; early outpoint insertion; formal verification; functional model; high-level software; high-level synthesis; software model; software path enumeration; subset instruction length decoders; symbolic execution; Combinational circuits; Computer aided instruction; Computer industry; Computer science; Decoding; Design optimization; Hardware; Mathematical model; Merging; Runtime; RTL; Verification; cutpoints; formal equivalence checking; software;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Design Automation Conference, 2006 43rd ACM/IEEE
Conference_Location :
San Francisco, CA
ISSN :
0738-100X
Print_ISBN :
1-59593-381-6
Type :
conf
DOI :
10.1109/DAC.2006.229439
Filename :
1688957
Link To Document :
بازگشت