Verification of VLSI Circuits Using LP - Garland, Stephen; Guttag, John; Staunstrup, Jørgen (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.