Verifying full-custom multipliers by Boolean equivalence checking and an arithmetic bit level proof

In this paper we describe a practical methodology to formally verify highly optimized, industrial multipliers. We define a multiplier description language which abstracts from low-level optimizations and which can model a wide range of common implementations at a structural and arithmetic level. The correctness of the created model is established by bit level transformations matching the model against a standard multiplication specification. The model is also translated into a gate netlist to be compared with the full-custom implementation of the multiplier by standard equivalence checking. The advantage of this approach is that we use a high level language to provide the correlation between structure and bit level arithmetic. This compares favorably with other approaches that have to spend considerable effort on extracting this information from highly optimized implementations. Our approach is easily portable and proved applicable to a wide variety of state-of-the-art industrial designs.