Sciweavers

Share
DAC
2006
ACM

Early cutpoint insertion for high-level software vs. RTL formal combinational equivalence verification

10 years 25 days ago
Early cutpoint insertion for high-level software vs. RTL formal combinational equivalence verification
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 highlevel 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 im...
Xiushan Feng, Alan J. Hu
Added 13 Nov 2009
Updated 13 Nov 2009
Type Conference
Year 2006
Where DAC
Authors Xiushan Feng, Alan J. Hu
Comments (0)
books