Although the circuit verification problem is NP-hard as measured in the size of the circuit description, several techniques can reduce the simulation complexity to a manageable level for many practical circuits. The theme of this paper is that a logic simulator can form the basis of a formal verifier. It proposes a behavioral approach to circuit verification, which complements the structural verification methodologies commonly used. The author also assumes that the abstract model provided by the simulator faithfully captures the behavior of the actual circuit. The paper is well organized, starting with an introduction to structural and behavioral approaches to verification and their relative merits.
Several examples illustrate the verification methodology proposed.
A good introduction to mathematical aspects of simulation, specification, and verification is provided. Bryant discusses the capabilities and limitations of black-box simulation as applied to verification as well as how those limitations are overcome by state transition simulation. The use of input weakening and symbolic simulation techniques to improve the performance of the verifier is described. The author has succeeded in both of these efforts. Although much work is needed to make this approach attractive, the paper is a good contribution to verification.