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

Nikolaos D. Liveris; Zhou Hai; Prithviraj Banerjee

doi:10.1109/ATS.2005.24

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

Nikolaos D. Liveris^*, Zhou Hai, Prithviraj Banerjee

^*Corresponding author for this work

Electrical and Computer Engineering

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English (US)
Title of host publication	Proceedings - 14th Asian Test Symposium, ATS 2005
Pages	28-33
Number of pages	6
DOIs	https://doi.org/10.1109/ATS.2005.24
State	Published - 2005
Event	14th Asian Test Symposium, ATS 2005 - Calcutta, India Duration: Dec 18 2005 → Dec 21 2005

Publication series

Name	Proceedings of the Asian Test Symposium
Volume	2005
ISSN (Print)	1081-7735

Other

Other	14th Asian Test Symposium, ATS 2005
Country/Territory	India
City	Calcutta
Period	12/18/05 → 12/21/05

ASJC Scopus subject areas

Electrical and Electronic Engineering

Access to Document

10.1109/ATS.2005.24

Cite this

@inproceedings{603a6edc0d7d4fe7b71baab211f2fba7,

title = "An efficient system-level to RTL verification framework for computation-intensive applications",

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.",

author = "Liveris, {Nikolaos D.} and Zhou Hai and Prithviraj Banerjee",

year = "2005",

doi = "10.1109/ATS.2005.24",

language = "English (US)",

isbn = "0769524818",

series = "Proceedings of the Asian Test Symposium",

pages = "28--33",

booktitle = "Proceedings - 14th Asian Test Symposium, ATS 2005",

note = "14th Asian Test Symposium, ATS 2005 ; Conference date: 18-12-2005 Through 21-12-2005",

}

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 -

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

Abstract

Publication series

Other

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this