An Efficient System-Level to RTL Verification Framework for Computation-Intensive Applications

In this paper, a new framework for formal verification is presented. The new framework called EVRM (efficient verification based on Mathematica) 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 (Clarke et al., 2003) 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