next up previous contents
Next: Contents   Contents

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.