14th Asian Test Symposium (ATS'05)
An Efficient System-Level to RTL Verification Framework for Computation-Intensive Applications
Calcutta, India
December 18-December 21
ISBN: 0-7695-2481-8
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 theMathematica 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.
Citation:
Nikolaos D. Liveris, Hai Zhou, Prithviraj Banerjee, "An Efficient System-Level to RTL Verification Framework for Computation-Intensive Applications," ats, pp.28-33, 14th Asian Test Symposium (ATS'05), 2005