Next: A buffer allocation controller
Up: Getting started with SMV
Previous: A traffic light controller
  Contents
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 , where 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: A buffer allocation controller
Up: Getting started with SMV
Previous: A traffic light controller
  Contents
2003-01-07