Verification of VLSI Circuits Using LP
Stephen Garland, John V. Guttag, Jørgen Staunstrup · DAIMI Report Series · 1988
We pressent an approach to reasoning about the functional behaviour of circuits. The approach begins and culminates 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.