Traces for hardware verification
Roger Stokes · ACM SIGARCH Computer Architecture News · 1986
Traces are histories of signal values. Traces can be used for describing and formally reasoning about digital circuits, at the register-transfer level where there is synchronous logic. Two proofs are given for an example circuit, and proved with the aid of a mechanical theorem-prover. The first proof is of correctness - that the required behaviour is a consequence of internal structure. The second proof is of consistency - that the given structure can in fact exist.