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.


               (                   (