“Mechanized verification of circuit descriptions using the Larch Prover”

Jørgen Staunstrup, Stephen J. Garland, and John V. Guttag

Theorem Provers in Circuit Design, Victoria Stavridou, Thomas F. Melham, and Raymond T. Boute (editors), IFIP Transactions A-10, pages 277–299, Nijmegen, The Netherlands, June 22–24, 1992. North-Holland.

This tutorial describes a circuit design technique that features using a mechanical theorem prover as a design tool, both to locate errors in preliminary designs and to verify certain aspects of completed designs. The design technique is based on SYNCHRONIZED TRANSITIONS, a high-level notation for describing circuits as collections of simple concurrent processes. It uses several different compilers to translate high-level circuit designs into formats suitable for circuit synthesis, simulation, and verification.

Back to Publications of Stephen J. Garland