Model Checking, Invariants and Abstraction The model_check command calls CTL model checking in VIS. Formulas to be checked are specified in a file which is an argument to the command. An important class of CTL formulas is invariants. These are formulas of the form AG  f, where f is a quantifier-free formula. The semantics of AG  f is that f is true in all reachable states. The command check_invariant implements an algorithm that is specialized for these formulas. When performing model checking and checking invariant properties, one can use the reduce option -r, to perform model checking on a ``pruned'' FSM, i.e., one where parts of the network that do not affect the formula (directly or indirectly) have been removed. This mechanism can be combined with the abstraction mechanism available through the command flatten_hierarchy -a <file>. <file> contains the names of variables to ``abstract''. For each variable x appearing in <file>, a new primary input node named x$ABS is created to drive all the nodes that were previously driven by x. Hence, the node x will not have any fanouts; however, x and its transitive fanins will remain in the network. Abstracting a net effectively allows it to take any value in its range, at every clock cycle. This mechanism can be used to perform manual abstractions.

Contact 

©2002-2018 U.C. Regents