SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
  SRI Logo

Hierarchical Verification of Two-Dimensional High-Speed Multiplication in PVS: A Case Study
 by Harald Rueß.

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.


About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2018 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy