Using Word-Level Information in Formal Hardware Verification.
Saved in:
| Title: | Using Word-Level Information in Formal Hardware Verification. |
|---|---|
| Authors: | Drechsler, R.1 |
| 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 |
| FullText | Links: – Type: pdflink Text: Availability: 0 |
|---|---|
| Header | DbId: egs DbLabel: Engineering Source An: 16764046 AccessLevel: 6 PubType: Academic Journal PubTypeId: academicJournal PreciseRelevancyScore: 0 |
| IllustrationInfo | |
| Items | – Name: Title Label: Title Group: Ti Data: Using Word-Level Information in Formal Hardware Verification. – Name: Author Label: Authors Group: Au Data: <searchLink fieldCode="AR" term="%22Drechsler%2C+R%2E%22">Drechsler, R.</searchLink><relatesTo>1</relatesTo> – Name: TitleSource Label: Source Group: Src Data: <searchLink fieldCode="JN" term="%22Automation+%26+Remote+Control%22">Automation & Remote Control</searchLink>. Jun2004, Vol. 65 Issue 6, p963-977. 15p. – Name: Subject Label: Subjects Group: Su Data: <searchLink fieldCode="DE" term="%22RTL+%28Computer+program+language%29%22">RTL (Computer program language)</searchLink><br /><searchLink fieldCode="DE" term="%22Programming+languages%22">Programming languages</searchLink><br /><searchLink fieldCode="DE" term="%22Hardware%22">Hardware</searchLink><br /><searchLink fieldCode="DE" term="%22Tools%22">Tools</searchLink><br /><searchLink fieldCode="DE" term="%22Memory%22">Memory</searchLink><br /><searchLink fieldCode="DE" term="%22Abstract+thought%22">Abstract thought</searchLink> – Name: Abstract Label: Abstract Group: Ab Data: 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] – Name: AbstractSuppliedCopyright Label: Group: Ab Data: <i>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.</i> (Copyright applies to all Abstracts.) |
| PLink | https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=16764046 |
| RecordInfo | BibRecord: BibEntity: Identifiers: – Type: doi Value: 10.1023/B:AURC.0000030907.28679.82 Languages: – Code: eng Text: English PhysicalDescription: Pagination: PageCount: 15 StartPage: 963 Subjects: – SubjectFull: RTL (Computer program language) Type: general – SubjectFull: Programming languages Type: general – SubjectFull: Hardware Type: general – SubjectFull: Tools Type: general – SubjectFull: Memory Type: general – SubjectFull: Abstract thought Type: general Titles: – TitleFull: Using Word-Level Information in Formal Hardware Verification. Type: main BibRelationships: HasContributorRelationships: – PersonEntity: Name: NameFull: Drechsler, R. IsPartOfRelationships: – BibEntity: Dates: – D: 01 M: 06 Text: Jun2004 Type: published Y: 2004 Identifiers: – Type: issn-print Value: 00051179 Numbering: – Type: volume Value: 65 – Type: issue Value: 6 Titles: – TitleFull: Automation & Remote Control Type: main |
| ResultId | 1 |
