Mechanized verification of circuit descriptions using the Larch Prover
Jörgen Staunstrup, Stephen J. Garland, and John V. Guttag
Theorem Provers in Circuit Design
Nijmegen, The Netherlands, June 22-24, 1992
North-Holland IFIP Transactions A-10, V. Stavridou, T. F. Melham, and R. T.
Boute (editors), pages 277-299
Abstract
This tutorial describes a circuit design technique that features using a
mechanical theorem prover as a design tool, both to locate errors in prelimary
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.