This is a short tutorial introduction to SMV, a verification system for hardware designs. 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 stimulus 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. Temporal logic specifications about finite state systems can be automatically formally verified by a technique called model checking.
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 produce a counterexample. This is a behavioral trace that violates the specified property. This makes SMV a very effective debugging tool, as well as a formal verification system.
Model checking by itself is limited to fairly small designs, because it must search every possible state that a system can reach. For large designs, especially those including substantial data path components, the user must break the correctness proof down into parts small enough for SMV to verify. This is known as compositional verification. SMV provides a number of tools to help the user reduce the verification of large, complex systems to small finite state problems. These techniques include refinement verification, symmetry reduction, temporal case splitting, data type reduction, and induction.
This tutorial will introduce all of the above techniques by example.