Alternative Approaches to Hardware Verification

BDD-based symbolic model checking has received a great deal of attention because of its potential for solving hardware verification problems. However, there are other, qualitatively different, approaches that are also quite promising (which having different strengths and weaknesses). This tutorial surveys a variety of approaches based on symbolic simulation.Symbolic simulation allows the user to set inputs to variables instead of constants, and propagates expressions containing those variables through the operators and expressions of the circuit. Symbolic simulation is attractive, because it works for large designs and can be made to degrade gracefully when designs become too large. It has the disadvantage that it is difficult or impossible to compute invariants automatically. By comparison, the main strength of model checking is its ability to computer invariants via iterative fixed point computations.The tutorial discusses different approaches to symbolic simulation and applications that make effective use of it, including abstraction methods and self-comparison.