Next: Contents
  Contents
Getting started with SMV
K. L. McMillan
Cadence Berkeley Labs
2001 Addison St.
Berkeley, CA 94704
USA
mcmillan@cadence.com
Abstract:
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.
2003-01-07