init_verify.
Regardless of the options, no 'false positives' or 'false negatives'
will occur: the result is correct for the given circuit.
Properties to be verified should be provided as CTL formulas in the
file ctl_file. Note that the support of any wire
referred to in a formula should consist only of latches. For the
precise syntax of CTL formulas, see the VIS CTL and LTL syntax manual.
Properties of the form AG f, where f is a formula not
involving path quantifiers are referred to as invariants; for such properties
it may be substantially faster to use the
check_invariant command.
A fairness constraint can be specified by invoking the
read_fairness command;
if none is specified, all paths are taken to be fair.
If some initial states
do not lie on a fair path, the model checker prints a message to this effect.
A formula passes iff it is true for all initial states of the system. Therefore, in the presence of multiple initial states, if a formula fails, the negation of the formula may also fail.
If a formula does not pass, a (potentially partial) proof of failure
(referred to as a debug trace) is demonstrated. Fair paths are
represented by a finite sequence of states (the stem) leading to a
fair cycle, i.e. a cycle on which there is a state from each
fairness condition. The level of detail of the proof can be
specified (see option -d).
Both backward (future tense CTL formulas) and forward (past tense CTL formulas) model checking can be performed. Forward model checking is based on Iwashita's ICCAD96 paper. Future tense CTL formulas are automatically converted to past tense ones as much as possible in forward model checking.
Command options:
<dbg_level>
dbg_level must be one of the following:
0: No debugging performed.
dbg_level=0 is the default.
1: Debugging with minimal output: generate counter-examples
for universal formulas (formulas of the form AX|AF|AU|AG) and
witnesses for existential formulas (formulas of the form
EX|EF|EU|EG). States on a path are not further analyzed.
2: Same as dbg_level=1, but more
verbose. (The subformulas are printed, too.)
3: Maximal automatic debugging: as for level 1,
except that states occurring on paths will be recursively analyzed.
4: Manual debugging: at each state, the user is queried if
more feedback is desired.
dbg_file>
dbg_file.
This option is incompatible with -F.
Notes: when you use -d4 (interactive mode), -f is not recommended, since you
can't see the output of vis on stdout.hints_file> hints_file contains a series of hints. A hint is a formula that
does not contain any temporal operators, so hints_file has the
same syntax as a file of invariants used for check_invariant. The hints are
used in the order given to change the transition relation. In the case of
least fixpoints (EF, EU), the transition relation is conjoined with the hint,
whereas for greatest fixpoints the transition relation is disjoined with the
negation of the hint. If the hints are cleverly chosen, this may speed up
the computation considerably, because a search with the changed transition
relation may be much simpler than one with the original transition relation,
and results obtained can be reused, so that we may never have to do a
complicated search with the original relation. Note: hints in terms of
primary inputs are not useful for greatest fixpoints. See also: Ravi and
Somenzi, Hints to accelerate symbolic traversal. CHARME'99; Bloem, Ravi, and
Somenzi, Efficient Decision Procedures for Model Checking of Linear Time
Logic Properties, CAV'99; Bloem, Ravi, and Somenzi, Symbolic Guided Search
for CTL Model Checking, DAC'00.
For formulae that contain both least and greatest fixpoints, the
behavior depends on the flag guided_search_hint_type.
If it is set to local (default) then every subformula is evaluated
to completion, using all hints in order, before the next subformula
is started. For pure ACTL or pure ECTL formulae, we can also set
guided_search_hint_type to global, in which case the entire formula
is evaluated for one hint before moving on to the next hint, using
underapproximations. The description of the options for guided
search can be found in the help page for
print_guided_search_options.
model_check will call reachability without any guided search, even if -g is used. If you want to perform reachability with guided search, call rch directly.
Incompatible with -F.
flatten_hierarchy).
These parts are effectively removed when this option is invoked; this may
result in more efficient model checking.
<timeOutPeriod>
<verbosity_level>
verbosity_level must be one of the following:
0: No feedback provided. This is the default.
1: Feedback on code location.
2: Feedback on code location and CPU usage.
<dc_level>
dc_level must be one of the following:
0 : No don't cares are used.
1 : Use unreachable states as don't cares. This is the
default.
2 : Use unreachable states as don't cares and in the EU
computation, use 'frontiers' for image computation.
3 : First compute an overapproximation of the reachable states
(ARDC), and use that as the cares set. Use `frontiers' for image
computation. For help on controlling options for ARDC, look up help on the
command: print_ardc_options. Refer
to Moon, Jang, Somenzi, Pixley, Yuan, "Approximate Reachability Don't Cares
for {CTL} Model Checking", ICCAD98, and to two papers by Cho et al, IEEE TCAD
December 1996: one is for State Space Decomposition and the other is for
Approximate FSM Traversal.
<schedule>
<schedule> must be one of the following:
EL : EU and EX operators strictly alternate. This
is the default.
EL1 : EX is applied once for every application of all EUs.
EL2 : EX is applied repeatedly after each application of
all EUs.
budget : a hybrid of EL and EL2.
random : enabled operators are applied in
(pseudo-)random order.
off : GSH is disabled, and the old algorithm is
used instead. The old algorithm uses the EL schedule, but
the termination checks are less sophisticated than in GSH.
node_file>
This option invoked the algorithm to generate an error trace divided
into fated and free segements. Fate represents the inevitability and
free is asserted when there is no inevitability. This can be formulated
as a two-player concurrent reachability game. The two players are
the environment and the system. The node_file is given to specify the
variables the are controlled by the system.
<ctl_file>
init_verify.
A fairness constraint can be read in by calling the
read_fairness command;
if none is specified, all paths are taken to be fair.
The system is reduced automatically with respect to the set of fairness constraints. If the language is not empty, a proof of this fact is generated. A proof is a fair path starting at an initial state. This is represented by a finite sequence of states starting at an initial state (the stem) leading to a fair cycle, i.e., a cycle on which there lies a state from each fairness condition.
Command options:
<dbg_level>
dbg_level must be one of the following:
0 : No debugging performed. This is the default.
1 : Generate a path to a fair cycle.
dbg_file>
dbg_file.
simulate command.
<timeOutPeriod>
<verbosity_level>
verbosity_level must be one of the following:
0 : No feedback provided. This is the default.
1 : Feedback on code location.
2 : Feedback on code location and CPU usage.
<le_method>
le_method must be one of the following:
0 : no use of Divide and Compose (Default).
1 : use Divide and Compose.
<dc_level>
dc_level must be one of the following:
0 : No don't cares are used.
1 : Use unreachable states as don't cares. This is the
default.
<schedule>
<schedule> must be one of the following:
EL : EU and EX operators strictly alternate. This
is the default.
EL1 : EX is applied once for every application of all EUs.
EL2 : EX is applied repeatedly after each application of
all EUs.
budget : a hybrid of EL and EL2.
random : enabled operators are applied in
(pseudo-)random order.
off : GSH is disabled, and the old algorithm is
used instead. The old algorithm uses the EL , but the
termination checks are less sophisticated than in GSH.
<lockstep_mode>
<lockstep_mode> must be one of the following:
off : Lockstep is disabled. This is the default.
Language emptiness is checked by computing a hull of the fair SCCs.
on : Lockstep is enabled.
all : Lockstep is enabled; all fair SCCs are
enumerated instead of terminating as soon as one is found. This can
be used to study the SCCs of a graph, but it is slower than the
default option.
n : (n is a positive integer). Lockstep is
enabled and up to n fair SCCs are enumerated. This
is less expensive than all , but still less efficient
than on , even when n = 1 .
hints_file>\] \[-f\] \[-h\] \[-i\] \[-m\] \[-r\]
\[-t <time_out_period>\] \[-v <verbosity_level>\] \[-A <reachability_analysis_type>\] \[-D\] <invar_file>]
CommandDescription [Performs invariant checking on a flattened
network. Before calling this command, the user should have
initialized the design by calling the command init_verify.
If the option -A3 (abstraction refinement method GRAB) is used, the command
build_partition_maigs
should also have been executed. However, in this case, the default BDD
manager and network partition are not mandatory, though they will be used if
available. (In other words, the user must run the commands flatten_hierarchy and build_partition_maigs, but
doesn't have to run the commands static_order and build_partition_mdds before
calling this command.) For extremely large networks, it is actually favorable
not to build them for the entire concrete model, but let this procedure
assign bdd ids and construct the partition incrementally.
Option -A4 means abstraction refinement approach using puresat algorithm, which is entirely based on SAT solver.
An invariant is a set of states. Checking the invariant is the process of determining that all states reachable from the initial states lie in the invariant.
One way of defining an invariant is through a CTL formula which has no path operators.
Such formulas should be specified in the file invar_file.
Note that the support of any wire referred to in a formula should consist only
of latches.
For the precise syntax of CTL formulas,
see the VIS CTL and LTL syntax manual.
check_invariant ignores all fairness conditions associated with the FSM.
Command options:
0: (default) Breadth First Search. No approximate reachability computation.
1: High Density Reachability Analysis (HD). Computes reachable states in a
manner that keeps BDD sizes under control. May be faster than BFS in some
cases. For larger circuits, this option could compute more reachable states
than the -A 0 option for the same memory constraints, consequently may prove
more invariants false. For help on controlling options for HD, look up help
on the command: print_hd_options
2. Approximate Reachability Don't Cares(ARDC). Computes over-approximated
reachable states in the reachability analysis step. This may be faster than
the -A 0 option . The invariants are checked in the over-approximation. This
may produce false negatives, but these are resolved internally using the
exact reachable states. The final results produced are the same as those for
exact reachable states. For help on controlling options for ARDC, look up
help on the command: print_ardc_options.
3. The GRAB Abstraction Refinement Method. Conducts the reachability
analysis on an abstract model. If the invariants are true in the
abstract model, they are also true in the original model. If the
invariants are false, the abstract counter-examples are used to
refine the abstract model (since it is still inconclusive). This
procedure iterates until a conclusive result is reached. Note that,
with this option, "build_partitioned_mdds" and "static_order" does
not have to be executed before calling "check_invariants," though
the default BDD partition and order will be reused if available.
(When checking extremely large models, skipping either or both
"static_order" and "build_partitioned_mdds" can often make the
verification much faster.) The grainularity of abstraction
refinement also depends on the parameter "partition_threshold",
which by default is 5000; one can use the VIS command "set
partition_threshold 1000" to change its value. For experienced users
who want to fine-tune the different parameters of GRAB, please try
the test command "_grab_test" ("_grab_test -h" prints out its usage
information). Refer to Wang et al., ICCAD2003 and ICCD2004 for more
information about the GRAB algorithm. Note that this option is
incompatible with the "-d 1" and "-g" options.
4. Abstraction refinement approach using puresat algorithm, which is
entirely based on SAT solver. It has several parts:
* Localization base Abstraction
* K-induction to prove the truth of a property
* Bounded Model Checking to find bugs
* Incremental concretization based methods to verify abstract bugs
* UNSAT proof based method to obtain refinement
* Refinement minization to guarrantee a minimal refinement
For more information, please check the BMC'03 and STTT'05
paper of Li et al., "A satisfiability-based appraoch to abstraction
refinement in model checking", and " Abstraction in symbolic model checking
using satisfiability as the only decision procedure"
]
SideEffects []
SeeAlso [CommandMc]
******************************************************************************/
static int
CommandInv(
Hrc_Manager_t **hmgr,
int argc,
char **argv)
{
int i, j;
mdd_t *tautology;
McOptions_t *options;
FILE *invarFile;
array_t *invarArray, *formulas, *sortedFormulaArray;
static Fsm_Fsm_t *totalFsm, *modelFsm;
mdd_manager *mddMgr;
Ntk_Network_t *network;
Mc_VerbosityLevel verbosity;
Mc_DcLevel dcLevel;
array_t *invarNormalFormulaArray, *invarStatesArray;
int timeOutPeriod = 0;
int debugFlag;
int buildOnionRings;
Fsm_RchType_t approxFlag;
int ardc;
int someLeft;
Ctlp_Formula_t *invarFormula;
mdd_t *invarFormulaStates;
mdd_t *reachableStates;
array_t *fsmArray;
int printStep = 0;
long initTime, finalTime;
array_t *careSetArray;
FILE *guideFile;
FILE *systemFile;
st_table *systemVarBddIdTable;
Ctlp_FormulaArray_t *hintsArray = NIL(Fsm_HintsArray_t);
array_t *hintsStatesArray = NIL(array_t); /* array of mdd_t* */
error_init();
initTime = util_cpu_time();
/* get command line options */
if (!(options = ParseInvarOptions(argc, argv))) {
return 1;
}
verbosity = McOptionsReadVerbosityLevel(options);
dcLevel = McOptionsReadDcLevel(options);
invarFile = McOptionsReadCtlFile(options);
timeOutPeriod = McOptionsReadTimeOutPeriod(options);
approxFlag = McOptionsReadInvarApproxFlag(options);
buildOnionRings = (int)McOptionsReadInvarOnionRingsFlag(options);
/* read the array of invariants */
invarArray = Ctlp_FileParseFormulaArray(invarFile);
fclose(invarFile);
if (invarArray == NIL(array_t)) {
(void) fprintf(vis_stderr, "** inv error: Error in parsing invariants from file\n");
McOptionsFree(options);
return 1;
}
if (array_n(invarArray) == 0) {
(void) fprintf(vis_stderr, "** inv error: No formula in file\n");
McOptionsFree(options);
return 1;
}
/* read the netwrok */
network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
if (network == NIL(Ntk_Network_t)) {
fprintf(vis_stderr, "%s\n", error_string());
error_init();
McOptionsFree(options);
return 1;
}
/**************************************************************************
* if "-A 3" is enabled (using the abstraction refinement method GRAB ),
* call GRAB.
**************************************************************************/
if (approxFlag == Fsm_Rch_Grab_c) {
if (Ntk_NetworkReadMAigManager(network) == NIL(mAig_Manager_t)) {
McOptionsFree(options);
fprintf(vis_stderr,
"** inv error: To use GRAB, please run build_partition_maigs first\n");
/*McOptionsFree(options);*/
return 1;
}
if (timeOutPeriod > 0) {
/* Set the static variables used by the signal handler. */
mcTimeOut = timeOutPeriod;
alarmLapTime = util_cpu_ctime();
(void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
(void) alarm(timeOutPeriod);
if (setjmp(timeOutEnv) > 0) {
(void) fprintf(vis_stdout,
"# INV: Checking Invariant: timeout occurred after %d seconds.\n",
timeOutPeriod);
(void) fprintf(vis_stdout, "# INV: data may be corrupted.\n");
alarm(0);
return 1;
}
}
Grab_NetworkCheckInvariants(network,
invarArray,
"GRAB", /* refineAlgorithm, */
TRUE, /* fineGrainFlag, */
TRUE, /* refineMinFlag, */
FALSE, /* useArdcFlag, */
2, /* cexType = SOR */
verbosity,
McOptionsReadDbgLevel(options),
McOptionsReadPrintInputs(options),
McOptionsReadDebugFile(options),
McOptionsReadUseMore(options),
"INV" /* driverName */
);
McOptionsFree(options);
return 0;
}
if (approxFlag == Fsm_Rch_PureSat_c) {
if (Ntk_NetworkReadMAigManager(network) == NIL(mAig_Manager_t)) {
McOptionsFree(options);
fprintf(vis_stderr,
"** inv error: Please run build_partition_maigs first\n");
McOptionsFree(options);
return 1;
}
if (timeOutPeriod > 0) {
/* Set the static variables used by the signal handler. */
mcTimeOut = timeOutPeriod;
alarmLapTime = util_cpu_ctime();
(void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
(void) alarm(timeOutPeriod);
if (setjmp(timeOutEnv) > 0) {
(void) fprintf(vis_stdout,
"# INV by PURESAT: Checking Invariant using PURESAT: timeout occurred after %d seconds.\n",
timeOutPeriod);
(void) fprintf(vis_stdout, "# INV by PURESAT: data may be corrupted.\n");
alarm(0);
return 1;
}
}
PureSat_CheckInvariant(network,invarArray,
(int)options->verbosityLevel,
options->dbgLevel,McOptionsReadDebugFile(options),
McOptionsReadPrintInputs(options),options->incre,
options->sss, options->flatIP, options->IPspeed);
McOptionsFree(options);
return 0;
}
guideFile = McOptionsReadGuideFile(options);
if(guideFile != NIL(FILE) ){
hintsArray = Mc_ReadHints(guideFile);
fclose(guideFile); guideFile = NIL(FILE);
if( hintsArray == NIL(array_t) ){
McOptionsFree(options);
return 1;
}
} /* if guided search */
if(Img_UserSpecifiedMethod() != Img_Iwls95_c &&
Img_UserSpecifiedMethod() != Img_Monolithic_c &&
Img_UserSpecifiedMethod() != Img_Mlp_c &&
guideFile != NIL(FILE)){
fprintf(vis_stdout,
"** inv error: The Tfm and Hybrid image methods are incompatible with -g\n");
McOptionsFree(options);
return 1;
}
if (dcLevel == McDcLevelArdc_c)
ardc = 1;
else
ardc = 0;
/* obtain the fsm and mdd manager */
totalFsm = Fsm_NetworkReadOrCreateFsm(network);
if (totalFsm == NIL(Fsm_Fsm_t)) {
fprintf(vis_stderr, "%s\n", error_string());
error_init();
McOptionsFree(options);
return 1;
}
systemVarBddIdTable = 0;
systemFile = McOptionsReadSystemFile(options);
if(systemFile != NIL(FILE) ){
systemVarBddIdTable = Mc_ReadSystemVariablesFAFW(totalFsm, systemFile);
fclose(systemFile); systemFile = NIL(FILE);
if(systemVarBddIdTable == (st_table *)-1 ){
McOptionsFree(options);
return 1;
}
} /* if FAFW */
if(options->FAFWFlag && systemVarBddIdTable == 0) {
systemVarBddIdTable = Mc_SetAllInputToSystem(totalFsm);
}
mddMgr = Fsm_FsmReadMddManager(totalFsm);
tautology = mdd_one(mddMgr);
/* set time out */
if (timeOutPeriod > 0) {
/* Set the static variables used by the signal handler. */
mcTimeOut = timeOutPeriod;
alarmLapTime = util_cpu_ctime();
(void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
(void) alarm(timeOutPeriod);
if (setjmp(timeOutEnv) > 0) {
(void) fprintf(vis_stdout, "# INV: Checking Invariant: timeout occurred after %d seconds.\n", timeOutPeriod);
(void) fprintf(vis_stdout, "# INV: data may be corrupted.\n");
alarm(0);
return 1;
}
}
/* debugFlag = 1 -> need to store/compute onion shells, else not */
debugFlag = (McOptionsReadDbgLevel(options) != McDbgLevelNone_c);
/* use formula tree if reduce option and dont-care level is high */
if ((McOptionsReadReduceFsm(options) == TRUE) &&
(dcLevel != McDcLevelNone_c)) {
McOptionsSetUseFormulaTree(options, TRUE);
}
/* derive the normalized array of invariant formulas */
if (McOptionsReadUseFormulaTree(options) == TRUE) {
invarNormalFormulaArray =
Ctlp_FormulaArrayConvertToExistentialFormTree(invarArray);
} else {
array_t *temp = Ctlp_FormulaArrayConvertToDAG( invarArray );
array_free( invarArray );
invarArray = temp;
invarNormalFormulaArray = Ctlp_FormulaDAGConvertToExistentialFormDAG(
invarArray );
}
if (array_n(invarNormalFormulaArray) == 0) {
array_free(invarNormalFormulaArray);
Ctlp_FormulaArrayFree(invarArray);
mdd_free(tautology);
return 1;
}
fsmArray = array_alloc(Fsm_Fsm_t *, 0);
sortedFormulaArray = SortFormulasByFsm(totalFsm, invarNormalFormulaArray,
fsmArray, options);
if (sortedFormulaArray == NIL(array_t)) {
array_free(invarNormalFormulaArray);
Ctlp_FormulaArrayFree(invarArray);
mdd_free(tautology);
return 1;
}
assert(array_n(fsmArray) == array_n(sortedFormulaArray));
careSetArray = array_alloc(mdd_t *, 0);
/* main loop for array of array of formulas. Each of the latter
arrays corresponds to one reduced fsm. */
arrayForEachItem(array_t *, sortedFormulaArray, i, formulas) {
int *resultArray;
int fail;
/* initialize pass, fail array */
resultArray = ALLOC(int, array_n(formulas));
for (j = 0; j < array_n(formulas); j++) {
resultArray[j] = 1;
}
/* get reduced fsm for this set of formulas */
modelFsm = array_fetch(Fsm_Fsm_t *, fsmArray, i);
/* evaluate hints for this reduced fsm, stop if the hints contain variables
* outside this model FSM.
*/
if (hintsArray != NIL(Ctlp_FormulaArray_t)) {
int k;
hintsStatesArray = Mc_EvaluateHints(modelFsm, hintsArray);
if( hintsStatesArray == NIL(array_t)) { /* something wrong, clean up */
int l;
fprintf(vis_stdout, "Hints dont match the reduced FSM for this set of invariants.\n");
fprintf(vis_stdout, "Continuing with the next set of invariants\n");
for (k = i; k < array_n(sortedFormulaArray); k++) {
formulas = array_fetch(array_t *, sortedFormulaArray, k);
arrayForEachItem(Ctlp_Formula_t *, formulas, l, invarFormula) {
Ctlp_FormulaFree(invarFormula);
}
array_free(formulas);
/* get reduced fsm for this set of formulas */
modelFsm = array_fetch(Fsm_Fsm_t *, fsmArray, k);
/* free the Fsm if it was reduced here */
if (modelFsm != totalFsm) Fsm_FsmFree(modelFsm);
}
array_free(careSetArray);
array_free(fsmArray);
array_free(sortedFormulaArray);
array_free(invarNormalFormulaArray);
(void) fprintf(vis_stdout, "\n");
Ctlp_FormulaArrayFree(invarArray);
McOptionsFree(options);
mdd_free(tautology);
return 1;
}
}/* hints exist */
if(options->FAFWFlag > 1) {
reachableStates = Fsm_FsmComputeReachableStates(
modelFsm, 0, verbosity , 0, 0, 1, 0, 0,
approxFlag, ardc, 0, 0, (verbosity > 1),
hintsStatesArray);
mdd_free(reachableStates);
}
invarStatesArray = array_alloc(mdd_t *, 0);
array_insert(mdd_t *, careSetArray, 0, tautology);
arrayForEachItem(Ctlp_Formula_t *, formulas, j, invarFormula) {
/* compute the set of states represented by the invariant. */
invarFormulaStates =
Mc_FsmEvaluateFormula(modelFsm, invarFormula, tautology,
NIL(Fsm_Fairness_t), careSetArray,
MC_NO_EARLY_TERMINATION,
NIL(Fsm_HintsArray_t), Mc_None_c,
verbosity, dcLevel, buildOnionRings,
McGSH_EL_c);
array_insert_last(mdd_t *, invarStatesArray, invarFormulaStates);
}
printStep = (verbosity == McVerbosityMax_c) && (totalFsm == modelFsm);
/* main loop to check a set of invariants. */
do {
boolean compute = FALSE;
/* check if the computed reachable set in the total FSM already violates an invariant. */
compute = TestInvariantsInTotalFsm(totalFsm, invarStatesArray, (debugFlag ||
buildOnionRings));
/* compute reachable set or until early failure */
if (compute)
reachableStates = Fsm_FsmComputeReachableStates(
modelFsm, 0, verbosity , 0, 0, (debugFlag || buildOnionRings), 0, 0,
approxFlag, ardc, 0, invarStatesArray, (verbosity > 1),
hintsStatesArray);
else if (debugFlag || buildOnionRings) {
(void)Fsm_FsmReachabilityOnionRingsStates(totalFsm, &reachableStates);
} else {
reachableStates = mdd_dup(Fsm_FsmReadCurrentReachableStates(totalFsm));
}
ardc = 0; /* once ardc is applied, we don't need it again. */
/* updates result array and sets fail if any formula failed.*/
fail = UpdateResultArray(reachableStates, invarStatesArray, resultArray);
mdd_free(reachableStates);
someLeft = 0;
if (fail) {
/* some invariant failed */
if (debugFlag) {
assert (approxFlag != Fsm_Rch_Oa_c);
Fsm_FsmSetFAFWFlag(modelFsm, options->FAFWFlag);
Fsm_FsmSetSystemVariableFAFW(modelFsm, systemVarBddIdTable);
InvarPrintDebugInformation(modelFsm, formulas, invarStatesArray,
resultArray, options, hintsStatesArray);
Fsm_FsmSetFAFWFlag(modelFsm, 0);
Fsm_FsmSetSystemVariableFAFW(modelFsm, 0);
} else if (approxFlag == Fsm_Rch_Oa_c) {
assert(!buildOnionRings);
/* May be a false negative */
/* undo failed results in the result array, report passed formulae */
arrayForEachItem(mdd_t *, invarStatesArray, j, invarFormulaStates) {
if (invarFormulaStates == NIL(mdd_t)) continue;
/* print all formulae that are known to have passed */
if (resultArray[j] == 1) {
mdd_free(invarFormulaStates);
array_insert(mdd_t *, invarStatesArray, j, NIL(mdd_t));
(void) fprintf(vis_stdout, "# INV: Early detection - formula passed --- ");
invarFormula = array_fetch(Ctlp_Formula_t *, formulas, j);
Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(invarFormula));
fprintf(vis_stdout, "\n");
} else resultArray[j] = 1;
}
fprintf(vis_stdout, "# INV: Invariant violated by over-approximated reachable states\n");
fprintf(vis_stdout, "# INV: Switching to BFS (exact computation) to resolve false negatives\n");
/* compute reachable set or until early failure */
reachableStates = Fsm_FsmComputeReachableStates(
modelFsm, 0, verbosity , 0, 0, 0, 0, 0, Fsm_Rch_Bfs_c, ardc, 0,
invarStatesArray, (verbosity > 1), hintsStatesArray);
/* either invariant has failed or all reachable states are computed */
/* updates result array */
fail = UpdateResultArray(reachableStates, invarStatesArray, resultArray);
mdd_free(reachableStates);
}
/* remove the failed invariants from the invariant list. */
if (fail) {
arrayForEachItem(mdd_t *, invarStatesArray, j, invarFormulaStates) {
if (invarFormulaStates == NIL(mdd_t)) continue;
/* free the failed invariant mdds */
if (resultArray[j] == 0) {
mdd_free(invarFormulaStates);
array_insert(mdd_t *, invarStatesArray, j, NIL(mdd_t));
if (!debugFlag) {
(void) fprintf(vis_stdout, "# INV: Early detection - formula failed --- ");
invarFormula = array_fetch(Ctlp_Formula_t *, formulas, j);
Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(invarFormula));
fprintf(vis_stdout, "\n");
}
} else {
someLeft = 1;
}
}
}
} /* end of recomputation dur to over approximate computation */
} while (someLeft);
arrayForEachItem(mdd_t *, invarStatesArray, j, invarFormulaStates) {
if (invarFormulaStates == NIL(mdd_t)) continue;
/* free the passed invariant mdds */
mdd_free(invarFormulaStates);
}
array_free(invarStatesArray);
if (printStep) {
finalTime = util_cpu_time();
Fsm_FsmReachabilityPrintResults(modelFsm,finalTime-initTime ,approxFlag);
}
/* free the Fsm if it was reduced here */
if (modelFsm != totalFsm) Fsm_FsmFree(modelFsm);
PrintInvPassFail(formulas, resultArray);
arrayForEachItem(Ctlp_Formula_t *, formulas, j, invarFormula) {
Ctlp_FormulaFree(invarFormula);
}
array_free(formulas);
FREE(resultArray);
} /* end of processing the sorted array of array of invariants */
if(hintsStatesArray != NIL(array_t))
mdd_array_free(hintsStatesArray);
if(hintsArray)
Ctlp_FormulaArrayFree(hintsArray);
array_free(careSetArray);
array_free(fsmArray);
array_free(sortedFormulaArray);
array_free(invarNormalFormulaArray);
(void) fprintf(vis_stdout, "\n");
if (options->FAFWFlag) {
st_free_table(systemVarBddIdTable);
}
Ctlp_FormulaArrayFree(invarArray);
McOptionsFree(options);
mdd_free(tautology);
alarm(0);
return 0;
}
/**Function********************************************************************
Synopsis [Parse command line options for invar.]
SideEffects []
******************************************************************************/
static McOptions_t *
ParseInvarOptions(
int argc,
char **argv)
{
unsigned int i;
int c;
boolean useMore = FALSE;
boolean reduceFsm = FALSE;
boolean printInputs = FALSE;
boolean useFormulaTree = FALSE;
FILE *inputFp=NIL(FILE);
FILE *debugOut=NIL(FILE);
char *debugOutName=NIL(char);
McDbgLevel dbgLevel = McDbgLevelNone_c;
Mc_VerbosityLevel verbosityLevel = McVerbosityNone_c;
int timeOutPeriod = 0;
McOptions_t *options = McOptionsAlloc();
int approxFlag = 0, ardc = 0, shellFlag = 0;
Fsm_RchType_t rchType;
FILE *guideFile;
FILE *systemFile = NIL(FILE);
boolean FAFWFlag = FALSE;
boolean GFAFWFlag = FALSE;
char *guideFileName = NIL(char);
char *variablesForSystem = NIL(char);
int incre, speed;
/* int sss; */
/*
* Parse command line options.
*/
util_getopt_reset();
while ((c = util_getopt(argc, argv, "ifcrt:g:hmv:d:A:DO:Ww:I:SPs:")) != EOF) {
switch(c) {
case 'g':
guideFileName = util_strsav(util_optarg);
break;
case 'h':
goto usage;
case 't':
timeOutPeriod = atoi(util_optarg);
break;
case 'v':
for (i = 0; i < strlen(util_optarg); i++) {
if (!isdigit((int)util_optarg[i])) {
goto usage;
}
}
verbosityLevel = (Mc_VerbosityLevel) atoi(util_optarg);
break;
case 'd':
for (i = 0; i < strlen(util_optarg); i++) {
if (!isdigit((int)util_optarg[i])) {
goto usage;
}
}
dbgLevel = (McDbgLevel) atoi(util_optarg);
break;
case 'f':
shellFlag = 1;
break;
case 'r' :
reduceFsm = TRUE;
break;
case 'm':
useMore = TRUE;
break;
case 'i' :
printInputs = TRUE;
break;
case 'c' :
useFormulaTree = TRUE;
break;
case 'A':
approxFlag = atoi(util_optarg);
if ((approxFlag > 4) || (approxFlag < 0)) {
goto usage;
}
break;
case 'D':
ardc = 1;
break;
case 'O':
debugOutName = util_strsav(util_optarg);
break;
case 'w':
variablesForSystem = util_strsav(util_optarg);
case 'W':
FAFWFlag = 1;
break;
case 'G':
GFAFWFlag = 1;
break;
case 'I':
incre = atoi(util_optarg);
options->incre = (incre==0)? FALSE:TRUE;
break;
case 'S':
/*sss = atoi(util_optarg);*/
/*options->sss = (sss==0)? FALSE:TRUE;*/
options->sss = TRUE;
break;
case 'P':
options->flatIP = TRUE;
break;
case 's':
speed = atoi(util_optarg);
options->IPspeed = speed;
break;
default:
goto usage;
}
}
if((FAFWFlag > 0 || GFAFWFlag > 0) && dbgLevel == 0) {
fprintf(vis_stderr, "** inv warning : -w and -W options are ignored without -d option\n");
}
if((FAFWFlag > 0 || GFAFWFlag > 0) && printInputs == 0) {
fprintf(vis_stderr, "** inv warning : -i is recommended with -w or -W option\n");
}
if(FAFWFlag) {
if (bdd_get_package_name() != CUDD) {
fprintf(vis_stderr, "** inv warning : -w and -W option is only available with CUDD\n");
FAFWFlag = 0;
FREE(variablesForSystem);
variablesForSystem = NIL(char);
}
}
/* translate approx flag */
switch(approxFlag) {
case 0: rchType = Fsm_Rch_Bfs_c; break;
case 1: rchType = Fsm_Rch_Hd_c; break;
case 2: rchType = Fsm_Rch_Oa_c; break;
case 3: rchType = Fsm_Rch_Grab_c; break;
case 4: rchType = Fsm_Rch_PureSat_c; break;
default: rchType = Fsm_Rch_Default_c; break;
}
if ((approxFlag == 1) && (bdd_get_package_name() != CUDD)) {
fprintf(vis_stderr, "** inv error: check_invariant with -A 1 option is currently supported by only CUDD.\n");
return NIL(McOptions_t);
}
if (rchType == Fsm_Rch_Oa_c) {
if (dbgLevel > 0) {
fprintf(vis_stdout, "Over approximation and debug level 1 are incompatible\n");
fprintf(vis_stdout, "Read check_invariant help page\n");
goto usage;
} else if (shellFlag == 1) {
fprintf(vis_stdout, "Over approximation and shell flag are incompatible\n");
fprintf(vis_stdout, "Read check_invariant help page\n");
goto usage;
}
}
if (rchType == Fsm_Rch_Grab_c) {
if (guideFileName != NIL(char)) {
fprintf(vis_stdout, "Abstraction refinement Grab and guided search are incompatible\n");
fprintf(vis_stdout, "Read check_invariant help page\n");
goto usage;
}
}
if (rchType == Fsm_Rch_PureSat_c) {
if (guideFileName != NIL(char)) {
fprintf(vis_stdout, "Abstraction refinement PureSat and guided search are incompatible\n");
fprintf(vis_stdout, "Read check_invariant help page\n");
goto usage;
}
}
if (guideFileName != NIL(char)) {
guideFile = Cmd_FileOpen(guideFileName, "r", NIL(char *), 0);
FREE(guideFileName);
if (guideFile == NIL(FILE)) {
McOptionsFree(options);
return NIL(McOptions_t);
}
McOptionsSetGuideFile(options, guideFile);
}
/*
* Open the ctl file.
*/
if (argc - util_optind == 0) {
(void) fprintf(vis_stderr, "** inv error: file containing invariant formulas not provided\n");
goto usage;
}
else if (argc - util_optind > 1) {
(void) fprintf(vis_stderr, "** inv error: too many arguments\n");
goto usage;
}
McOptionsSetUseMore(options, useMore);
McOptionsSetReduceFsm(options, reduceFsm);
McOptionsSetPrintInputs(options, printInputs);
McOptionsSetUseFormulaTree(options, useFormulaTree);
McOptionsSetTimeOutPeriod(options, timeOutPeriod);
McOptionsSetInvarApproxFlag(options, rchType);
if (ardc)
McOptionsSetDcLevel(options, McDcLevelArdc_c);
else
McOptionsSetDcLevel(options, McDcLevelNone_c);
McOptionsSetInvarOnionRingsFlag(options, shellFlag);
McOptionsSetFAFWFlag(options, FAFWFlag + GFAFWFlag);
inputFp = Cmd_FileOpen(argv[util_optind], "r", NIL(char *), 0);
if (inputFp == NIL(FILE)) {
McOptionsFree(options);
return NIL(McOptions_t);
}
McOptionsSetCtlFile(options, inputFp);
if (debugOutName != NIL(char)) {
debugOut = Cmd_FileOpen(debugOutName, "w", NIL(char *), 0);
if (debugOut == NIL(FILE)) {
McOptionsFree(options);
return NIL(McOptions_t);
}
}
McOptionsSetDebugFile(options, debugOut);
if ((verbosityLevel != McVerbosityNone_c) &&
(verbosityLevel != McVerbosityLittle_c) &&
(verbosityLevel != McVerbositySome_c) &&
(verbosityLevel != McVerbosityMax_c)) {
goto usage;
}
else {
McOptionsSetVerbosityLevel(options, verbosityLevel);
}
if ((dbgLevel != McDbgLevelNone_c) &&
(dbgLevel != McDbgLevelMin_c)) {
if(((rchType == Fsm_Rch_Grab_c) && (dbgLevel == McDbgLevelMinVerbose_c)))
{
McOptionsSetDbgLevel(options, dbgLevel);
}
else
{
if((rchType == Fsm_Rch_PureSat_c) && (options->flatIP == TRUE) && (dbgLevel == McDbgLevelMinVerbose_c))
{
McOptionsSetDbgLevel(options, dbgLevel);
}
else
{
if((rchType == Fsm_Rch_Bfs_c) && (dbgLevel == McDbgLevelMinVerbose_c))
{
McOptionsSetDbgLevel(options, dbgLevel);
}
else
{
goto usage;
}
}
}
}
else {
McOptionsSetDbgLevel(options, dbgLevel);
}
if (variablesForSystem != NIL(char)) {
systemFile = Cmd_FileOpen(variablesForSystem, "r", NIL(char *), 0);
if (systemFile == NIL(FILE)) {
fprintf(vis_stderr, "** inv error: cannot open system variables file for FAFW %s.\n",
variablesForSystem);
FREE(variablesForSystem);
variablesForSystem = NIL(char);
McOptionsFree(options);
return NIL(McOptions_t);
}
FREE(variablesForSystem);
variablesForSystem = NIL(char);
}
McOptionsSetVariablesForSystem(options, systemFile);
return options;
usage:
(void) fprintf(vis_stderr, "usage: check_invariant [-c][-d dbg_level][-f][-g check_invariant involves reachability analysis where at
every step of the reachability computation all the specified
invariants are checked in the reachable states computed thus
far. If some invariant does not hold, a proof of failure is
demonstrated. This consists of a path starting from an initial
state to a state lying outside the invariant. This path is made as
short as possible. For the -A 0 option or default -A option, it is
the shortest path leading to a state outside the invariant. If a
set of invariants is specified, the failed formulas are reported as
soon as they are detected. The check is continued with the
remaining invariants.
<dbg_level>
dbg_level must be one of the following:
0 : No debugging performed. This is the default.
1 : Generate a path from an initial state to a state
lying outside the invariant. This option stores the onion rings just
as specifying -f would have. Therefore, it may take more time and
memory if the formula passes. This option is incompatible with -A 2
option. hints_file>hints_file contains a
series of hints. A hint is a formula that does not contain any
temporal operators, so hints_file has the same syntax
as a file of invariants used for check_invariant. The hints are
used in the order given to change the transition relation. The
transition relation is conjoined with the hint to yield an
underapproximation of the transition relation. If the hints are
cleverly chosen, this may speed up the computation considerably,
because a search with the changed transition relation may be much
simpler than one with the original transition relation, and results
obtained can be reused, so that we may never have to do an expensive
search with the original relation. See also: Ravi and Somenzi,
Hints to accelerate symbolic traversal. CHARME'99; Bloem, Ravi, and
Somenzi, Efficient Decision Procedures for Model Checking of Linear
Time Logic Properties, CAV'99; Bloem, Ravi, and Somenzi, Symbolic
Guided Search for CTL Model Checking, DAC'00. This option is not
compatible with -A 2 option. The description of some options for
guided search can be found in the help page for
print_guided_search_options. flatten_hierarchy).
These parts are effectively removed when this option is invoked; this may result in
more efficient invariant checking.
<timeOutPeriod>
<verbosity_level>
verbosity_level must be one of the following:
0 : No feedback provided. This is the default. 1 : Feedback on code location. 2 : Feedback on code location and CPU usage.
print_hd_options. Refer Ravi & Somenzi, ICCAD95. The path
generated for a failed invariant using this method may not be the shortest
path. This option is available only when compiled with the CUDD package. print_ardc_options Refer
2 papers in TCAD96 Dec. Cho et al, one is for State Space Decomposition and
the other is for Approximate FSM Traversal. This option is incompatible with
-d 1 and -g options.set. This option is incompatible with -g. dbg_file>
dbg_file.
node_file>
This option invokes the algorithm to generate an error trace divided
into fated and free segements. Fate represents the inevitability and
free is asserted when there is no inevitability. This can be formulated
as a two-player concurrent reachability game. The two players are
the environment and the system. The node_file is given to specify the
variables the are controlled by the system.