Modeling of custom-designed arithmetic components for ABL normalization

Abstract

Arithmetic bit-level (ABL) normalization has been proven a viable approach to formal property checking of datapath designs. It is applicable where arithmetic components and sub-components can be identified at the register-transfer (RT) level of the design and the property. This paper extends the applicability of ABL normalization to cases where some of the arithmetic components are custom-designed entities, e.g., specified using Boolean equations or gates. We transform these entities into ABL building blocks using Reed-Muller expressions as an intermediate representation. We show how Boolean logic expressed in Reed-Muller form can be automatically transformed into ABL components so that such logic blocks can be treated together with the remaining ABL components in a subsequent normalization run. The approach is evaluated on a number of industrial designs generated by a commercial arithmetic module generator.