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.