TY - GEN
T1 - An efficient system-level to RTL verification framework for computation-intensive applications
AU - Liveris, Nikolaos D.
AU - Hai, Zhou
AU - Banerjee, Prithviraj
PY - 2005
Y1 - 2005
N2 - In this paper a new framework for formal verification is presented. The new framework called EVRM (Efficient VeRification based on Mathematica [1]) can be used for the property verification of a Register Transfer Level implementation using a System Level description as the golden model. EVRM is based on word level techniques and uses the Mathematica tool for the satisfiability procedure. Results show that it can be orders of magnitude faster than CBMC [2] in proving property correctness or providing a counterexample for computation-intensive applications. For certain applications CBMC requires more than 5 hours to provide an answer, while EVRM provides an answer in less than 10 minutes.
AB - In this paper a new framework for formal verification is presented. The new framework called EVRM (Efficient VeRification based on Mathematica [1]) can be used for the property verification of a Register Transfer Level implementation using a System Level description as the golden model. EVRM is based on word level techniques and uses the Mathematica tool for the satisfiability procedure. Results show that it can be orders of magnitude faster than CBMC [2] in proving property correctness or providing a counterexample for computation-intensive applications. For certain applications CBMC requires more than 5 hours to provide an answer, while EVRM provides an answer in less than 10 minutes.
UR - http://www.scopus.com/inward/record.url?scp=33846919940&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=33846919940&partnerID=8YFLogxK
U2 - 10.1109/ATS.2005.24
DO - 10.1109/ATS.2005.24
M3 - Conference contribution
AN - SCOPUS:33846919940
SN - 0769524818
SN - 9780769524818
T3 - Proceedings of the Asian Test Symposium
SP - 28
EP - 33
BT - Proceedings - 14th Asian Test Symposium, ATS 2005
T2 - 14th Asian Test Symposium, ATS 2005
Y2 - 18 December 2005 through 21 December 2005
ER -