Normalization at the arithmetic bit level

The authors proposed a normalization technique for verifying arithmetic circuits in a bounded model checking environment. The presented technique operates on the arithmetic bit level (ABL) description of the arithmetic circuit parts and the property. The ABL description could 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. The approach has been applied successfully to verify the integer pipeline of an industrial microprocessor with advanced DSP capabilities.