CVC(1) USER COMMANDS CVC(1)
NAME
cvc - CMU VHDL temporal logic model checker (release 1.b.1)
SYNOPSIS
cvc [-option ...] specification_file
DESCRIPTION
This manual documents cvc, a program for the formal verifi-
cation of temporal properties of systems described in a sub-
set of VHDL.
OPTIONS
cvc recognizes the following command-line switches:
-v,--version
shows the current version of cvc.
-h,--help
prints a summary of the options.
-hstill-inputs
this restricts the verification to the simulations
where the signals of mode in are stable during delta-
delay simulation cycles.
-fproject,-fno-project
turns on (off) an optimization heuristic that consists
in the elimination of the parts of the model that are
not relevant for the specification being checked
(default on).
-freorder-level n
sets BDD variable reordering level to n; n must be
comprised in the interval [0, 4] (3 is the default
value).
-fsize-mult-coeff n
multiplicative coefficient used to determine the amount
of memory initially allocated to the verifier; n must
be greater or equal than 2 (300 is the default).
DETAILED DESCRIPTION
VHDL descriptions verified with cvc must comply to some res-
trictions (see cva (1) for a description of the subset).
A detailed description of the specification can be found in
the document specification-language.html. Briefly, a
specification is composed of assumptions, guarantees, and
abbreviations. Assumptions describe the behavior of the
environment of the description. Guarantees describe the
behavior of the description.
An assumption is a condition (i.e. a boolean expression) on
the signals of mode in. There are two sorts of assumptions:
invariant assumptions and fairness assumptions. A simula-
tion satisfies an invariant assumption if for every simula-
tion cycle the condition is satisfied. A simulation satis-
fies a fairness assumption if the condition is satisfied
infinitely often.
A guarantee is a temporal logic property on the signals of
the description. It is the purpose of cvc to check that
guarantees are satisfied for all possible simulations of the
model that satisfy the assumptions of the specification.
An abbreviation is used to define identifiers that denote
complex expressions about the VHDL descriptions. They are a
simple facility to write more concise and clearer specifica-
tions.
SEE ALSO
cva(1), cv(3)
AUTHOR
David Deharbe
cmuvhdl@cs.cmu.edu.
Cvc Release 1.b.1 Last change: 12 December 1996
Documentation Sections: cva(1) VHDL Grammar cvc(1) Specification Language
Main Sections: Introduction Installation Documentation Examples