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
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;
Conference_Titel :
Design Automation Conference, 2006 43rd ACM/IEEE
Conference_Location :
San Francisco, CA
Print_ISBN :
1-59593-381-6
DOI :
10.1109/DAC.2006.229439