Hierarchical Verification of Two-Dimensional
High-Speed Multiplication in PVS:
A Case Study
Presented at FMCAD'96, Palo Alto, CA, November 1996. © Springer-Verlag.
Authors
Harald Rueß
Abstract
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.
gzipped postscript
or
postscript
BibTeX Entry
@Article{Ruess:FMCAD1996,
author = {Harald Rue{\ss}},
title = {Hierarchical Verification of Two-Dimensional
High-Speed Multiplication in {PVS}: A Case Study},
publisher = {Springer-Verlag},
journal = {Lecture Notes in Computer Science},
volume = 1166,
year = 1996
}
Harald Ruess:
ruess@csl.sri.com
