next up previous contents
Next: A buffer allocation controller Up: Getting started with SMV Previous: A traffic light controller   Contents

Symbolic model checking

A model checker verifies a property by building a graph of all of the states in the model. In SMV, the number of states in the model is $2^n$, where $n$ is the number of state variables in the cone of the property. In fact, it is only necessary for the model checker to consider the states that are ``reachable'' from an initial state. However, as you might expect, the amount of computational effort required to verify a property still tends to grow very rapidly with the number of state variables. This is known as the ``state explosion problem''.

To address this problem, SMV uses a structure called a ``Binary Decision Diagram'' (BDD) to implicitly represent the state graph of the model, and sets of states satisfying given properties. For some models and properties, the use of BDD's (implicit enumeration) allows SMV to handle models with many orders of magnitude more states than could be handled by considering individual states (explicit enumeration). In this section, we'll see some examples of circuits and systems with very large states spaces that can still be handled efficiently using BDD's. Later we'll consider what to do when a direct approach using BDD's doesn't work.



Subsections
next up previous contents
Next: A buffer allocation controller Up: Getting started with SMV Previous: A traffic light controller   Contents
2003-01-07