“Verification of VLSI circuits using LP”

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

The Fusion of Hardware Design and Verification, pages 329–345, Glasgow, Scotland, July 4–6, 1988. IFIP WG 10.2, North Holland.

We present an approach to reasoning about the functional behavior of circuits. The approach begins with a technique, Synchronized Transitions, for specifying circuits and culminates with a technique for constructing machine checked proofs that invariants are preserved. We also report on some successful experiments using the approach to verify properties of simple, but nontrivial, VLSI circuits.

Back to Publications of Stephen J. Garland