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 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. Categories and Subject Descriptors B6.3 [Design Aids]: Verification General Terms Algorithms, Verification Keywords Property checking, arithmetic bit level normalization, SAT

• Type: Conference
• Year: 2005
• Where: DAC
• Authors: Markus Wedler, Dominik Stoffel, Wolfgang Kunz
• Keywords: Arithmetic Bit Level, Arithmetic Circuit, Arithmetic Circuit Parts, Computer Architecture, DAC 2005