Verifying pipelined hardware using symbolic logic simulation

A method is presented for automated verification of synchronous pipelined circuits, based on symbolic simulation and the well-known program verification concept of representation functions. The use of representation functions to allow straightforward formulation of readable and intuitive specifications is demonstrated, along with the use of a symbolic switch-level simulator to automatically prove that a circuit meets its specification. As an example, a systolic stack with more than 5000 transistors can be formally verified in a few minutes on a VAX 8800.< <ETX xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">></ETX>