**K. L. McMillan
Cadence Berkeley Labs
2001 Addison St.
Berkeley, CA 94704
USA
mcmillan@cadence.com**

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.

- Contents
- Introduction
- Modeling, specifying and verifying

- Symbolic model checking

- Refinement verification
- Layers
- Refinement maps
- Decomposing large data structures
- Exploiting Symmetry
- Decomposing large structures in the implementation
- Case analysis
- Data type reductions
- Proof by induction
- Instruction processors
- An out-of-order instruction processor
- Bit vectors as scalarsets
- Propagation of unknown values
- Conditional proof statements, and course-of-values induction

- Synchronous Verilog
- Basic concepts
- Example - traffic light controller
- Example - buffer allocation controller
- Synthesizable Verilog and SMV
- Symmetry and Synchronous Verilog

- Handling very large input files
- About this document ...

2003-01-07