Other Files for Advanced Users

Cadence SMV Model

We originally coded our monitor specification in the Cadence SMV syntax and checked for contradictions, and the existence of certain characteristics in the specification using their model checker.

Here are the files used for this model.

history.smv
counter.smv
output.smv (the main file, also contains a list of properties that hold for the specification.)

The Properties

Here is a list of properties (CTL formulas) which hold for the formal PCI specification.

properties

IMPORTANT : If you are going to use any of this material for research or commercial application, please cite this website for the above material.

kannas@stanford.edu

Last modified : February 2, 2000