A Normalization Method for Arithmetic Data-Path Verification

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 property. The ABL description can easily be provided by the front-end of a register transfer level property checker. The proposed normalization greatly simplifies the SAT instances to be solved for arithmetic circuit verification. Our approach has been successfully applied to verify the integer pipeline of an industrial microprocessor with advanced DSP capabilities.