Using Word-Level Information in Formal Hardware Verification.

Saved in:

Bibliographic Details
Title:	Using Word-Level Information in Formal Hardware Verification.
Authors:	Drechsler, R.¹
Source:	Automation & Remote Control. Jun2004, Vol. 65 Issue 6, p963-977. 15p.
Subjects:	RTL (Computer program language), Programming languages, Hardware, Tools, Memory, Abstract thought
Abstract:	Reducing run times and the amount of memory needed for computations is one requirement in order to match today's sizes of real world designs in formal hardware verification. Designs are usually given as Register-Transfer-Level (RTL) specifications, but most of today's hardware verification tools are based on bit-level methods. However, designs, like for example ALUs or bus interfaces, often have very regular structures that can be described easily on a higher level of abstraction. This information is lost on bit-level and thus cannot be utilized by verification tools, if verification procedures operate on the basis of bit-level descriptions. Recently, several approaches to formal circuit verification have been proposed that make use of such regularities. These approaches are based on word-level descriptions as they are available on the RTL. We introduce the main concepts of formal verification on the RTL and give a brief overview of existing techniques. Recent developments are outlined, and based on real world examples we show the advantages of the use of word-level information for equivalence checking and property checking. [ABSTRACT FROM AUTHOR]
	Copyright of Automation & Remote Control is the property of Springer Nature and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
Database:	Engineering Source

Description
Abstract:	Reducing run times and the amount of memory needed for computations is one requirement in order to match today's sizes of real world designs in formal hardware verification. Designs are usually given as Register-Transfer-Level (RTL) specifications, but most of today's hardware verification tools are based on bit-level methods. However, designs, like for example ALUs or bus interfaces, often have very regular structures that can be described easily on a higher level of abstraction. This information is lost on bit-level and thus cannot be utilized by verification tools, if verification procedures operate on the basis of bit-level descriptions. Recently, several approaches to formal circuit verification have been proposed that make use of such regularities. These approaches are based on word-level descriptions as they are available on the RTL. We introduce the main concepts of formal verification on the RTL and give a brief overview of existing techniques. Recent developments are outlined, and based on real world examples we show the advantages of the use of word-level information for equivalence checking and property checking. [ABSTRACT FROM AUTHOR]
ISSN:	00051179
DOI:	10.1023/B:AURC.0000030907.28679.82