Modular Verification of SRT Division

Presented at CAV'96, New Brunswick, NJ, August 1996. © Springer-Verlag.

---

Authors

Harald Rueß, M.K. Srivas, N. Shankar

Abstract

We describe a formal specification and verification in {\sc PVS} for the general theory of SRT division, and for the hardware design of a specific implementation. The specification demonstrates how attributes of the {\sc PVS} language (in particular, predicate subtypes) allow the general theory to be developed in a readable manner that is similar to textbook presentations, while the {\sc PVS} {\tt table} construct allows direct specification of the implementation's quotient look-up table. Verification of the derivations in the SRT theory and for the data path and look-up table of the implementation are highly automated and performed for arbitrary, but finite precision; in addition, the theory is verified for general radix, while the implementation is specialized to radix 4. The effectiveness of the automation derives from {\sc PVS}'s tight integration of rewriting with decision procedures for equality, linear arithmetic over integers and rationals, and propositional logic. This example demonstrates that the resources of an expressive specification language and of a general-purpose theorem prover are not inimical to highly automated verification in this domain, and can contribute to clarity, generality, and reuse.

gzipped postscript or postscript

BibTeX Entry

@InProceedings{RuessSrivasShankar:CAV96,
  author =       "Harald Rue{\ss} and N. Shankar and M. K. Srivas",
  title =        "Modular verification of {SRT} division",
  booktitle =    "Proc. of the 8th International Conference for Automated Verification (CAV'96)",
  editors =     "R. Alur and T. Henzinger",
  series =      "Lecture Notes in Computer Science",
  publisher =   "Springer-Verlag",
  month  =      "July/August",
  number =      "1102",
  year =        "1996"
}

---

Harald Ruess: ruess@csl.sri.com