It is shown how to use the PVS specification language and proof checker to present a hierarchical formalization of a two-dimensional, high speed integer multiplier on the gate level. We first give an informal description of iterative array multiplier circuits together with a natural refinement into vertical and horizontal stages, and then show how the various features of PVS can be used to obtain a readable, high-level specification. The verification exploits the tight integration between rewriting, arithmetic decision procedures, and equality that is present in PVS. Al together, this case study demonstrates that the resources of an expressive specification language and of a general-purpose theorem prover permit highly automated verification in this domain, and can contribute to clarity, generality, and reuse.

• fmcad96-ruess.ps