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

Modular Verification of SRT Division

H. Rueß, N. Shankar, M. Srivas

Appeared in: Proceedings of the Conference on Computer-Aided Verification (CAV'96)


We describe a formal specification and verification in PVS for the general theory of SRT division, and for the hardware design of a specific implementation. The specification demonstrates how attributes of the 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 PVS 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 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.

Available as Postscript (209 KB) or compressed Postscript (81 KB).

BibTeX Entry

  TITLE     = {Modular {V}erification of {S}{R}{T} Division},
  AUTHOR    = {H. Rue{\ss} and N. Shankar and M. K. Srivas},
  BOOKTITLE = {Computer-Aided Verification, CAV '96},
  EDITOR    = {Rajeev Alur and Thomas A. Henzinger},
  PAGES     = {123--134},
  PUBLISHER = {Springer-Verlag},
  SERIES    = {Lecture Notes in Computer Science},
  VOLUME    = 1102,
  MONTH     = {July/August},
  YEAR      = 1996,
  ADDRESS   = {New Brunswick, NJ}

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