Package Documentation


abs Incremental CTL model checker.
amc Model Check using over(under)-approximation of the transition
baig Binary AND/INVERTER graph
bmc bounded model checking (BMC) header file.
cmd Implements command line interface, and miscellaneous commands.
ctlp Routines for parsing, writing and accessing CTL formulas.
ctlsp Routines for parsing, writing and accessing CTL* formulas.
eqv Provides commands for doing combinational and sequential
fsm Finite state machine abstraction of a network.
grab Abstraction refinement for large scale invariant checking.
hrc Hierarchical representation of a design.
imc Model Check using over(under)-approximation with automatic
img Methods for performing image computations.
io Routines for reading and writing BLIF-MV files.
ltl Internal declarations.
maig multi-valued AND/INVERTER graph
mark Data structures used in Markovian analysis.
mc Fair CTL model checker and debugger.
mvf Creation and manipulation of MDD-based multi-valued functions.
mvfaig Creation and manipulation of AndInv-based multi-valued functions.
ntk Flat network of multi-valued combinational nodes and latches.
ntm Construction of MDDs from a flattened network.
ntmaig Construction of mAigs from a flattened network.
ord Routines for ordering MDD variables of a flattened network.
part Partition of a system and creation of MDDs.
puresat Abstraction refinement for large scale invariant checking using SAT as the only decision procedure.
res Combinational verification by residue arithmetic.
restr External header file for STG restructuring package.
rst Restructuring package for restructuring the hierarchy
rt Regression test
sat A CNF AIG hybrid SAT solver
sim Simulation of a flattened network.
spfd SPFD-based wire removal and replacement algorithm for
synth Symbolic synthesis package.
tbl Routines for manipulating a multi-valued relation representation.
truesim Exported functions and data structures for the truesim package.
tst Test package illustrating VIS conventions.
var Multi-valued variables.
vm "Main" package of VIS ("vm" = VIS main).

Last updated on 20050519 00h50