This is a short tutorial introduction to SMV, a verification system for hardware designs, based on a technique called ``symbolic model checking''. SMV is a formal verification tool, which means that when you write a specification for a given system, it verifies that every possible behavior of the system satisfies the specification. This is in contrast to a simulator, which can only verify the system's behavior for the particular vectors that you provide.
A specification for SMV is a collection of properties. A property can be as simple as a statement that a particular pair of signals are never asserted at the same time, or it might state some complex relationship in the values or timing of the signals. Properties are specified in a notation called temporal logic. This allows concise specifications about temporal relationships between signals, and can be automatically verified.
SMV is quite effective in automatically verifying properties of combinational logic and interacting finite state machines. Sometimes, when checking properties of complex control logic, the verifier will automatically produce a counterexample. This is a behavioral trace of the finite state machines that violates the specified property. This makes SMV a very effective debugging tool, as well as a formal verification system.
For large designs, especially those including substantial data path components, the user must break the correctness proof down into small enough pieces for SMV to verify. There are two mechanisms provided for this purpose. In the compositional method, you verify temporal logic properties of one part of the system and use these properties as assumptions when verifying another part of the system. In the refinement method, you use a high level model of the system as a specification, and verify separately that each system component implements its part of the high level specification.
This tutorial will present examples of all of the above techniques.