An efficient system-level to RTL verification framework for computation-intensive applications

Nikolaos D. Liveris*, Zhou Hai, Prithviraj Banerjee

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution

3 Scopus citations

Abstract

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.

Original languageEnglish (US)
Title of host publicationProceedings - 14th Asian Test Symposium, ATS 2005
Pages28-33
Number of pages6
DOIs
StatePublished - 2005
Event14th Asian Test Symposium, ATS 2005 - Calcutta, India
Duration: Dec 18 2005Dec 21 2005

Publication series

NameProceedings of the Asian Test Symposium
Volume2005
ISSN (Print)1081-7735

Other

Other14th Asian Test Symposium, ATS 2005
CountryIndia
CityCalcutta
Period12/18/0512/21/05

ASJC Scopus subject areas

  • Electrical and Electronic Engineering

Fingerprint Dive into the research topics of 'An efficient system-level to RTL verification framework for computation-intensive applications'. Together they form a unique fingerprint.

Cite this