CV: Examples
The examples are intentionnally small and serve to
illustrate the different features of the model checker.
- Temporal logic: most temporal logic operators are explained on
the specification of a latch.
- Fairness constraints: how fairness constraints can be used
to specify and check progress properties is explained on a small
token ring.
- Invariant constraints: the use of invariants to constrain the
values of the inputs is explained on a stack.
Main sections:
Introduction
Installation
Documentation
Examples
CV /
Carnegie Mellon University /
cmuvhdl@cs.cmu.edu /
Revised December 1996