Getting started with SMV
K. L. McMillan
Cadence Berkeley Labs
2001 Addison St.
Berkeley, CA 94704
This tutorial introduces the SMV verification system. It includes examples of
temporal logic model checking, and refinement verification, including techniques
of circular compositional proof, temporal case splitting, symmetry reduction,
data type reduction and induction.
©1998 Cadence Berkeley Labs, Cadence Design Systems.