Bridging the formal methods gap: a computer-aided verification tool for hardware designs

The author describes a computer-aided verification tool, called Spectool, for synchronous hardware designs. The tool reduces the effort required for verifying a design in the targeted class by automating most of the routine, but cumbersome, parts of the verification process. The input to the tool is a circuit diagram of the design drawn using the graphical user interface provided by the tool. Spectool has been used on several examples including a large pipelined microprocessor design.<>