Universität Ulm, Fakultät für Informatik, Abt. KI - Our Papers on Using PVS

Hierarchical Verification of Two-Dimensional High-Speed Multiplication in PVS: A Case Study

H. Rueß

Appeared in: Proceedings of the Conference on Formal Methods in Computer-Aided Design (FMCAD'96).


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. Altogether, 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.

Available as Postscript (238 KB) or compressed Postscript (85 KB).

BibTeX Entry

 TITLE     = {Hierarchical {V}erification of {T}wo-{D}imensional {H}igh-{S}peed
              {M}ultiplication in {P}{V}{S}: {A} {C}ase {S}tudy},
 AUTHOR    = {Harald Rue{\ss}},
 BOOKTITLE = {Formal Methods in Computer-Aided Design (FMCAD '96)},
 EDITOR    = {M. Srivas},
 PAGES     = {79--93},
 PUBLISHER = {Springer-Verlag},
 SERIES    = {Lecture Notes in Computer Science},
 VOLUME    = 1166,
 MONTH     = nov,
 YEAR      = 1996,
 ADDRESS   = {Palo Alto, CA}

Harald Rueß - March 4, 1997 - Mail to Webmaster