Normalization at the arithmetic bit level

We propose a normalization technique for verifying arithmetic circuits in a bounded model checking environment. Our technique operates on the arithmetic bit level (ABL) description of the arithmetic circuit parts and the property. The ABL description can easily be provided by the front-end of an RTL...

Full description

Saved in:
Bibliographic Details
Main Authors: Wedler, Markus, Stoffel, Dominik, Kunz, Wolfgang
Format: Conference Proceeding
Language:English
Subjects:
Algorithm design and analysis
Arithmetic
Data mining
Digital circuits
Digital signal processing
Electronic design automation and methodology
Hardware > Hardware validation > Functional verification
Microprocessors
Permission
Pipelines
Sequential circuits
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:We propose a normalization technique for verifying arithmetic circuits in a bounded model checking environment. Our technique operates on the arithmetic bit level (ABL) description of the arithmetic circuit parts and the property. The ABL description can easily be provided by the front-end of an RTL property checker. The proposed normalization greatly simplifies the SAT instances to be solved for arithmetic circuit verification. Our approach has been applied successfully to verify the integer pipeline of an industrial microprocessor with advanced DSP capabilities.
ISSN:0738-100X
DOI:10.1145/1065579.1065699