#include "grabInt.h"
Include dependency graph for grab.c:
Go to the source code of this file.
Functions | |
| static int | CommandGrab (Hrc_Manager_t **hmgr, int argc, char **argv) |
| static void | TimeOutHandle (void) |
| void | Grab_Init (void) |
| void | Grab_End (void) |
| void | Grab_NetworkCheckInvariants (Ntk_Network_t *network, array_t *InvariantFormulaArray, char *refineAlgorithm, int fineGrainFlag, int refineMinFlag, int useArdcFlag, int cexType, int verbosity, int dbgLevel, int printInputs, FILE *debugFile, int useMore, char *driverName) |
Variables | |
| static jmp_buf | timeOutEnv |
Function Documentation
| static int CommandGrab | ( | Hrc_Manager_t ** | hmgr, |
| int | argc, | ||
| char ** | argv | ||
| ) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [Implements the test command for Grab.]
CommandName [_grab_test]
CommandSynopsis [Performs invairant checking on a flattened network with the GRAB abstraction refinement algorithm.]
CommandArguments [ \[-a <refine_algorithm>\] \[-c <cex_type>\] \[-d <dbg_level>\] \[-F\] \[-M\] \[-i\] \[-m\] \[-t <time_out_period>\] \[-v <verbosity_level>\] \[-f <dbg_file>\] \[-h\] <inv_file>]
CommandDescription [Performs invairant checking on a flattened network with the GRAB abstraction refinement algorithm. Before calling this command, the user should have created the flattened netowrk by calling the commands flatten_hierarchy and build_partition_maigs. The default BDD manager and network partition are not mandatory for calling this command, though they will be used if available. (In other words, the user doesn't have to run the commands static_order and build_partition_mdds before calling this command.)
Regardless of the options, no 'false positive' or 'false negatives' will occurs: the result is correct for the given model.
Properties to be verified should be provided as invariant formulae in the file inv_file. Node that the support of any wire referred to in a formula should consist only of latches. For the precise syntax of CTL and LTL formulas, see the VIS CTL and LTL syntax manual.
If a formula does not pass, a proof of failure (referred to as a counter-example) is demonstrated. Whether demostrate the proof or not can be specified (see option -d).
Command options:
- -a
<refine_algorithm> Specify the refinement variable selection algorithm.
refine_algorithmmust be one of the following:GRAB: the GRAB refinement method (Default).- -c
<cex_type> Specify the type of abstract counter-examples used in the analysis.
cex_typemust be one of the following:0: minterm state counter-example.1: cube state counter-example.2: synchronous onion rings (Default).- -d
<dbg_level> Specify whether to demonstrate a counter-example when the system fails a formula being checked.
dbg_levelmust be one of the following:0: No debugging performed.dbg_level=0is the default.1: Generate a counter-example (a path to a fair cycle).- -F
<finegrain_flag> Enable or disable the use of fine-grain abstraction.
finegrain_flagmust be one of the following:0: disable fine-grain abstraction.1: enable fine-grain abstraction (Default).- -M
<refinemin_flag> Enable or disable the use of greedy refinement minimization.
refinemin_flagmust be one of the following:0: disable greedy refinement minimization.1: enable greedy refinement minimization (Default).- -i
Print input values causing transitions between states during debugging. Both primary and pseudo inputs are printed.
- -m
Pipe debugger output through the UNIX utility more.
- -t
<timeOutPeriod> Specify the time out period (in seconds) after which the command aborts. By default this option is set to infinity.
- -v
<verbosity_level> Specify verbosity level. This sets the amount of feedback on CPU usage and code status.
verbosity_levelmust 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.- -f
<dbg_out> Specify the name of the file ot which error trace is written.
- -h
Print the command usage.
See also commands : model_check, check_invariant ]
SideEffects []
Definition at line 914 of file grab.c.
{
int c, verbosity;
char InvFileName[256];
FILE *FP, *dbgFile;
array_t *InvariantFormulaArray;
Ntk_Network_t *network;
static int timeOutPeriod = 0;
char refineAlgorithm[256];
int cexType = 0;
int refineMinFlag;
int fineGrainFlag;
int useArdcFlag = 0;
long startTime, endTime;
char *dbgFileName = NIL(char);
int dbgLevel, printInputs, useMore;
startTime = util_cpu_ctime();
Img_ResetNumberOfImageComputation(Img_Both_c);
/* the default setting is Grab+,
* Generational Refinement of Ariadne's Bundle of SORs
*/
strcpy(refineAlgorithm, "GRAB");
cexType = GRAB_CEX_SOR;
fineGrainFlag = 1;
refineMinFlag = 1;
verbosity = 0;
dbgLevel = 0;
printInputs = 0;
useMore = 0;
/*
* Parse command line options.
*/
util_getopt_reset();
while ((c = util_getopt(argc, argv, "a:c:d:F:M:imt:v:f:h")) != EOF) {
switch(c) {
case 'a':
strcpy(refineAlgorithm, util_optarg);
break;
case 'F':
fineGrainFlag = atoi(util_optarg);
break;
case 'M':
refineMinFlag = atoi(util_optarg);
break;
case 'c':
cexType = atoi(util_optarg);
break;
case 'D':
useArdcFlag = 1;
break;
case 't':
timeOutPeriod = atoi(util_optarg);
break;
case 'v':
verbosity = atoi(util_optarg);
break;
case 'd':
dbgLevel = atoi(util_optarg);
break;
case 'i':
printInputs = 1;
break;
case 'm':
useMore = 1;
break;
case 'f':
dbgFileName = util_strsav(util_optarg);
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if (strcmp(refineAlgorithm, "GRAB")) {
fprintf(vis_stdout, "\nunknown refinement algorithm: %s\n",
refineAlgorithm);
goto usage;
}
/* Make sure the flattened network is available
*/
network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
if (network == NIL(Ntk_Network_t)) {
fprintf(vis_stdout, "%s\n", error_string());
error_init();
return 1;
}
/* Make sure the AIG graph is available
*/
if (Ntk_NetworkReadMAigManager(network) == NIL(mAig_Manager_t)) {
fprintf(vis_stderr,
"** grab error: please run buid_partiton_maigs first\n");
return 1;
}
/* Open the InvFile. (It must contain a single invariant property)
*/
if (argc - util_optind == 0) {
(void) fprintf(vis_stderr,
"** grab error: file containing inv formula not provided\n");
goto usage;
}else if (argc - util_optind > 1) {
(void) fprintf(vis_stderr, "** grab error: too many arguments\n");
goto usage;
}
strcpy(InvFileName, argv[util_optind]);
/* Parsing the InvFile
*/
FP = Cmd_FileOpen(InvFileName, "r", NIL(char *), 0);
if (FP == NIL(FILE)) {
(void) fprintf(vis_stdout, "** grab error: error in opening file %s\n",
InvFileName);
return 1;
}
InvariantFormulaArray = Ctlp_FileParseFormulaArray(FP);
fclose(FP);
if (InvariantFormulaArray == NIL(array_t)) {
(void) fprintf(vis_stdout,
"** grab error: error in parsing formulas from file %s\n",
InvFileName);
return 1;
}
if (dbgFileName != NIL(char))
dbgFile = Cmd_FileOpen(dbgFileName, "r", NIL(char *), 0);
else
dbgFile = NIL(FILE);
/* Set time out processing (if timeOutPeriod is set)
*/
if (timeOutPeriod > 0) {
(void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
(void) alarm(timeOutPeriod);
if (setjmp(timeOutEnv) > 0) {
fprintf(vis_stdout,
"\n# GRAB: abstract-refine - timeout occurred after %d seconds.\n",
timeOutPeriod);
(void) fprintf(vis_stdout, "# GRAB: data may be corrupted.\n");
endTime = util_cpu_ctime();
fprintf(vis_stdout, "# GRAB: elapsed time is %5.1f.\n",
(double)(endTime - startTime)/1000.0);
if (verbosity) {
fprintf(vis_stdout,
"-- total %d image computations and %d preimage computations\n",
Img_GetNumberOfImageComputation(Img_Forward_c),
Img_GetNumberOfImageComputation(Img_Backward_c));
}
alarm(0);
return 1;
}
}
/* Check invariants with the abstraction refinement algorithm GRAB
*/
Grab_NetworkCheckInvariants(network,
InvariantFormulaArray,
refineAlgorithm,
fineGrainFlag,
refineMinFlag,
useArdcFlag,
cexType,
verbosity,
dbgLevel,
printInputs,
dbgFile,
useMore,
"GRAB"
);
/* Total cost
*/
if (verbosity >= 2) {
endTime = util_cpu_ctime();
fprintf(vis_stdout, "# GRAB: elapsed time is %5.1f.\n",
(double)(endTime - startTime)/1000.0);
fprintf(vis_stdout,
"-- total %d image computations and %d preimage computations\n",
Img_GetNumberOfImageComputation(Img_Forward_c),
Img_GetNumberOfImageComputation(Img_Backward_c));
}
alarm(0);
return 0; /* normal exit */
usage:
(void) fprintf(vis_stderr, "usage: _grab_test [-a refine_algorithm] [-c cex_type] [-d dbg_level] [-F finegrain_flag] [-M refmin_flag] [-i] [-m] [-t period] [-v verbosity_level] [-f dbg_out] [-h] <invar_file>\n");
(void) fprintf(vis_stderr, " -a <refine_algorithm>\n");
(void) fprintf(vis_stderr, " refine_algorithm = GRAB => the GRAB refinement method (Default)\n");
(void) fprintf(vis_stderr, " -c <cex_type>\n");
(void) fprintf(vis_stderr, " cex_type = 0 => minterm state counter-example\n");
(void) fprintf(vis_stderr, " cex_type = 1 => cube state counter-example\n");
(void) fprintf(vis_stderr, " cex_type = 2 => synchronous onion rings (Default)\n");
(void) fprintf(vis_stderr, " -d <dbg_level>\n");
(void) fprintf(vis_stderr, " debug_level = 0 => no debugging (Default)\n");
(void) fprintf(vis_stderr, " debug_level = 1 => print path to state failing invariant\n");
(void) fprintf(vis_stderr, " -F <finegrain_flag>\n");
(void) fprintf(vis_stderr, " finegrain_flag = 0 => disable fine-grain abstraction\n");
(void) fprintf(vis_stderr, " finegrain_flag = 1 => enable fine-grain abstraction (Default)\n");
(void) fprintf(vis_stderr, " -M <refinemin_flag>\n");
(void) fprintf(vis_stderr, " refinemin_flag = 0 => disable greedy refinement minimization\n");
(void) fprintf(vis_stderr, " refinemin_flag = 1 => enable greedy refinement minimization (Default)\n");
(void) fprintf(vis_stderr, " -i \tPrint input values in debug traces.\n");
(void) fprintf(vis_stderr, " -m pipe debugger output through UNIX utility more\n");
(void) fprintf(vis_stderr, " -t <period> Time out period.\n");
(void) fprintf(vis_stderr, " -v <verbosity_level>\n");
(void) fprintf(vis_stderr, " verbosity_level = 0 => no feedback (Default)\n");
(void) fprintf(vis_stderr, " verbosity_level = 1 => code status\n");
(void) fprintf(vis_stderr, " verbosity_level = 2 => code status and CPU usage profile\n");
(void) fprintf(vis_stderr, " -f <dbg_out>\n");
(void) fprintf(vis_stderr, " write error trace to dbg_out\n");
(void) fprintf(vis_stderr, " <invar_file> The input file containing invariants to be checked.\n");
(void) fprintf(vis_stderr, " -h\t\t print the command usage\n");
return 1; /* error exit */
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void Grab_End | ( | void | ) |
| void Grab_Init | ( | void | ) |
AutomaticEnd Function********************************************************************
Synopsis [Initializes the grab package. The added command is for testing purpose only; the same algorithm can be activated by the check_invariant command.]
SideEffects []
SeeAlso [Refine_End]
Definition at line 80 of file grab.c.
{
/*
* Add a command to the global command table. By using the leading
* underscore, the command will be listed under "help -a" but not "help".
*/
Cmd_CommandAdd("_grab_test", CommandGrab, 0);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void Grab_NetworkCheckInvariants | ( | Ntk_Network_t * | network, |
| array_t * | InvariantFormulaArray, | ||
| char * | refineAlgorithm, | ||
| int | fineGrainFlag, | ||
| int | refineMinFlag, | ||
| int | useArdcFlag, | ||
| int | cexType, | ||
| int | verbosity, | ||
| int | dbgLevel, | ||
| int | printInputs, | ||
| FILE * | debugFile, | ||
| int | useMore, | ||
| char * | driverName | ||
| ) |
Function********************************************************************
Synopsis [Check invariant formulae with abstraction refinement method Grab.]
Description [Check invariant formulae with the GRAB abstraction refinement method. For each formula, an small initial abstract model is constructed, which contains only the state variables mentioned by the formula. The abstract model is then gradually refined by adding more state variables and Boolean network variables (Bnvs), until it is sufficient to decided the property. Bnvs are internal nodes of the circuit---they are selected in order to partition large combinational logic cones into smaller pieces. The selection of refinement variables (both state vars and Bnvs) is based on the analysis of all the shortest counter-examples, which are captured by a data structure called the Synchronous Onion Rings (SORs). For the algorithmic details, please check the ICCAD'03 paper of Wang et al., "Improving Ariadne's Bundle by Following Multiple Counter-Examples in Abstraction Refinement," and the ICCD'04 paper of Wang et al., "Fine-Grain Abstraction and Sequential Don't Cares for Large Scale Model Checking."
The existence of a network partition is not mandatory for calling this function. However, if it does exist, it will be used by this function; otherwise, the network partition will be constructed incrementally as the abstract model grows. If the default bdd manager is not available, this function will create one and assign bdd ids incrementally as the abstract model grows. (For extremely large models, it is favorable to let the procedure assign bdd ids and construct the partition incrementally.)
The parameter refineAlgorithm specifies the refinement variable selection algorithm---currently, only GRAB is available. When fineGrainFlag is FALSE, only latches are considered as the abstraction "atoms"; When fineGrainFlag is TRUE, both Bnvs and latches are considered "atoms." To disable the greedy minimization of refinement sets, set refineMinFlag to FALSE. The parameter useArdcFlag is not used at this point. By default, all the shortest counter-examples are analyzed (cexType==GRAB_CEX_SOR); when cexType is set to GRAB_CEX_MINTERM or GRAB_CEX_CUBE, only a minterm or cube state path is analyzed---these two options may be helpful if there is too much overhead of computing the entire SORs.]
SideEffects [Nothing related to the network is changed: if the default partition and mdd manager are available, they will be left intact; if they are not available, the incrementally created new partition and mdd manager will be freed before exit.]
Definition at line 156 of file grab.c.
{
mdd_manager *mddManager = NIL(mdd_manager);
graph_t *partition;
Ctlp_Formula_t *invFormula;
Ctlsp_Formula_t *invFormula_sp;
array_t *invStatesArray;
array_t *resultArray;
st_table *absLatchTable, *absBnvTable;
st_table *coiLatchTable, *coiBnvTable;
Fsm_Fsm_t *absFsm;
array_t *visibleVarMddIds, *invisibleVarMddIds;
int concreteLatchCount, abstractLatchCount;
int concreteBnvCount, abstractBnvCount;
st_table *nodeToFaninNumberTable;
mdd_t *rchStates, *invStates = NIL(mdd_t); /*=mdd_one(mddManager);*/
array_t *SORs, *save_SORs;
boolean refineDirection, runMinimization, isLastStep;
int staticOrderFlag, partitionFlag;
int cexLength, refineIteration;
array_t *addedVarsAtCurrentLevel = NIL(array_t);
array_t *addedBnvsAtCurrentLevel = NIL(array_t);
int auxValue1, auxValue2, flag, i;
long startTime, endTime, totalTime;
long mcStartTime, mcEndTime, mcTime;
long sorEndTime, sorTime;
long conEndTime, conTime;
long dirStartTime, dirEndTime, dirTime;
long refStartTime, refEndTime, refTime;
long miniStartTime, miniEndTime, miniTime;
if ( strcmp(refineAlgorithm, "GRAB") ) {
fprintf(vis_stdout,
"** ci error: Abstraction refinement method %s not available\n",
refineAlgorithm);
return;
}
/* if the mddIds haven't been assigned to the network nodes,
* we assign them incrementally (i.e., staticOrderFlag==1).
*/
mddManager = Ntk_NetworkReadMddManager(network);
if (mddManager == NIL(mdd_manager))
staticOrderFlag = 1;
else
staticOrderFlag = 0;
if (staticOrderFlag) {
GrabNtkClearAllMddIds(network);
mddManager = Ntk_NetworkInitializeMddManager(network);
if (verbosity >= 2)
bdd_dynamic_reordering(mddManager, BDD_REORDER_SIFT,
BDD_REORDER_VERBOSITY);
else
bdd_dynamic_reordering(mddManager, BDD_REORDER_SIFT,
BDD_REORDER_NO_VERBOSITY);
}
/* if the partition hasn't been created, we create the partition
* incrementally (i.e., partitionFlag==1)
*/
partition = Part_NetworkReadPartition(network);
if (partition == NIL(graph_t))
partitionFlag = GRAB_PARTITION_BUILD;
else
partitionFlag = GRAB_PARTITION_NOCHANGE;
/* used by the refinement algorithm as a tie-breaker */
nodeToFaninNumberTable = st_init_table(st_ptrcmp, st_ptrhash);
/***************************************************************************
* check the invariants
***************************************************************************/
resultArray = array_alloc(int, array_n(InvariantFormulaArray));
arrayForEachItem(Ctlp_Formula_t *, InvariantFormulaArray, i, invFormula) {
invFormula_sp = Ctlsp_CtlFormulaToCtlsp(invFormula);
/* this is required for the following code to function correctly */
visibleVarMddIds = invisibleVarMddIds = NIL(array_t);
invStatesArray = SORs = save_SORs = NIL(array_t);
mcTime = sorTime = conTime = dirTime = refTime = miniTime = 0;
startTime = util_cpu_ctime();
/* record the number of latches in the cone-of-influence */
coiLatchTable = GrabComputeCOIAbstraction(network, invFormula);
concreteLatchCount = st_count(coiLatchTable);
/* build the initial abstract model */
absLatchTable = GrabComputeInitialAbstraction(network, invFormula);
abstractLatchCount = st_count(absLatchTable);
if (verbosity >= 3) {
GrabPrintNodeHashTable("InitialAbstractLatches", absLatchTable);
}
/* initialize the abs./concrete table for boolean network variables*/
coiBnvTable = st_init_table(st_ptrcmp, st_ptrhash);
abstractBnvCount = concreteBnvCount = 0;
if (fineGrainFlag == 1) {
absBnvTable = st_init_table(st_ptrcmp, st_ptrhash);
}else {
absBnvTable = NIL(st_table);
}
/* if the concrete partition is available, retrieve form it the
* bnvs; otherwise, we incrementally create bnvs (for the current
* absLatches only)---this is designed for performance concerns */
if (partitionFlag == GRAB_PARTITION_NOCHANGE) {
Part_PartitionReadOrCreateBnvs(network, coiLatchTable, coiBnvTable);
concreteBnvCount = st_count(coiBnvTable);
}
/* Outer Loop---Over Refinements For Different SOR Lengths
*/
refineIteration = 0;
isLastStep = 0;
while(1) {
long grabStartTime = util_cpu_ctime();
/* Build the Abstract Finite State Machine */
absFsm = GrabCreateAbstractFsm(network, coiBnvTable, absLatchTable,
absBnvTable, partitionFlag, TRUE);
concreteBnvCount = st_count(coiBnvTable);
invisibleVarMddIds = GrabGetInvisibleVarMddIds(absFsm, absLatchTable,
absBnvTable);
visibleVarMddIds = GrabGetVisibleVarMddIds(absFsm, absLatchTable);
/* sanity check */
isLastStep = (array_n(invisibleVarMddIds)==0);
if (isLastStep) {
assert(abstractLatchCount == concreteLatchCount);
}
/* Compute The Invariant States If They Are Not Available */
if (invStatesArray == NIL(array_t)) {
mdd_t * tautology = mdd_one(mddManager);
array_t *careSetArray = array_alloc(mdd_t *, 0);
array_insert(mdd_t *, careSetArray, 0, tautology);
invStates = Mc_FsmEvaluateFormula(absFsm, invFormula, tautology,
NIL(Fsm_Fairness_t), careSetArray,
MC_NO_EARLY_TERMINATION,
NIL(Fsm_HintsArray_t), Mc_None_c,
McVerbosityNone_c, McDcLevelNone_c,
0, McGSH_EL_c);
mdd_array_free(careSetArray);
invStatesArray = array_alloc(mdd_t *, 0);
array_insert(mdd_t *, invStatesArray, 0, invStates);
}
/* Conduct Forward Reachability Analysis */
rchStates = GrabFsmComputeReachableStates(absFsm,
absLatchTable,
absBnvTable,
invStatesArray,
verbosity);
mcEndTime = util_cpu_ctime();
mcTime += (mcEndTime - grabStartTime);
if (verbosity >= 1) {
fprintf(vis_stdout,
"-- grab: absLatch [%d/%d], absBnv [%d/%d], mc time is %5g s\n",
abstractLatchCount, concreteLatchCount,
abstractBnvCount, concreteBnvCount,
(double)(mcEndTime-grabStartTime)/1000.0);
}
/* if bad states cannot be reached, the property is true;
* if absFsm is concrete, the property is false
*/
flag = mdd_lequal(rchStates, invStates, 1, 1);
mdd_free(rchStates);
if (flag || isLastStep) {
/* set the debugging info, if necessary */
if (!flag)
SORs = mdd_array_duplicate(Fsm_FsmReadReachabilityOnionRings(absFsm));
Fsm_FsmSubsystemFree(absFsm);
absFsm = NIL(Fsm_Fsm_t);
array_free(invisibleVarMddIds);
array_free(visibleVarMddIds);
break;
}
/* Build The Synchronous Onion Rings (SORs) */
Fsm_FsmFreeImageInfo(absFsm);
SORs = GrabFsmComputeSynchronousOnionRings(absFsm, absLatchTable,
absBnvTable, NIL(array_t),
invStates, cexType,
verbosity);
sorEndTime = util_cpu_ctime();
sorTime += (sorEndTime - mcEndTime);
/* Concretize Multiple Counter-Examples */
cexLength = array_n(SORs)-1;
flag = !Bmc_AbstractCheckAbstractTraces(network, SORs, coiLatchTable,
0, dbgLevel, printInputs);
conEndTime = util_cpu_ctime();
conTime += (conEndTime - sorEndTime);
if (!flag) {
if (verbosity >= 1)
fprintf(vis_stdout,
"-- grab: find length-%d concrete counter-examples\n",
cexLength);
Fsm_FsmSubsystemFree(absFsm);
absFsm = NIL(Fsm_Fsm_t);
array_free(invisibleVarMddIds);
array_free(visibleVarMddIds);
break;
}else {
if (verbosity >= 2)
fprintf(vis_stdout,
"-- grab: find length-%d spurious counter-examples\n",
cexLength);
}
/* Innor Loop---Over Refinements For The Same SOR Length
*/
save_SORs = mdd_array_duplicate(SORs);
addedVarsAtCurrentLevel = array_alloc(int, 0);
addedBnvsAtCurrentLevel = array_alloc(int, 0);
refineDirection = 1;
runMinimization = 0;
while (1) {
int skip_refinement = 0;
/* Get the appropriate refinement direction:
* runMinimization==1 --> BOOLEAN
* fineGrainFlag==0 --> SEQUENTIAL
* coiBnvTable is empty --> SEQUENTIAL
* refineDirection==0 --> BOOLEAN
*/
if ( !runMinimization && refineDirection) {
if ( fineGrainFlag && st_count(coiBnvTable)>0 ) {
dirStartTime = util_cpu_ctime();
#if 0
refineDirection = !GrabTestRefinementSetSufficient(network,
save_SORs,
absLatchTable,
verbosity);
#endif
runMinimization = (refineDirection==0);
dirEndTime = util_cpu_ctime();
dirTime += (dirEndTime - dirStartTime);
}
}
if (verbosity >= 3 && refineDirection==0)
fprintf(vis_stdout, "refinement is in %s direction\n",
(refineDirection? "both":"boolean"));
/* Minimize the refinement set of latches */
if (runMinimization) {
int n_latches = st_count(absLatchTable);
int break_flag;
if (refineMinFlag && array_n(addedVarsAtCurrentLevel) > 1) {
miniStartTime = util_cpu_ctime();
GrabMinimizeLatchRefinementSet(network,
&absLatchTable,
&absBnvTable,
addedVarsAtCurrentLevel,
&addedBnvsAtCurrentLevel,
save_SORs,
verbosity);
abstractLatchCount = st_count(absLatchTable);
abstractBnvCount = absBnvTable? st_count(absBnvTable):st_count(coiBnvTable);
array_free(addedVarsAtCurrentLevel);
addedVarsAtCurrentLevel = array_alloc(int, 0);
miniEndTime = util_cpu_ctime();
miniTime += (miniEndTime - miniStartTime);
}
/* if the refinement set of bnvs is also sufficient, break */
break_flag = 1;
if (fineGrainFlag && st_count(coiBnvTable)>0) {
dirStartTime = util_cpu_ctime();
break_flag = GrabTestRefinementBnvSetSufficient(network,
coiBnvTable,
save_SORs,
absLatchTable,
absBnvTable,
verbosity);
dirEndTime = util_cpu_ctime();
dirTime += (dirEndTime - dirStartTime);
}
if (break_flag) {
if (verbosity >= 1)
fprintf(vis_stdout,
"-- grab: remove length-%d spurious counter-examples\n\n",
cexLength);
break;
}
/* Otherwise, skip this refinement step, because the
* current absFsm is not well-defined (some latches have
* been droped)
*/
SORs = mdd_array_duplicate(save_SORs);
if (n_latches > st_count(absLatchTable))
skip_refinement = 1;
refineDirection = 0;
runMinimization = 0;
}
/* compute the refinement (by Grab)
*/
if (!skip_refinement) {
array_t *addedVars = array_alloc(int, 0);
array_t *addedBnvs = array_alloc(int, 0);
auxValue1 = st_count(absLatchTable) +
((absBnvTable==NIL(st_table))? 0:st_count(absBnvTable));
refStartTime = util_cpu_ctime();
/* create the abstract fsm */
Fsm_FsmSubsystemFree(absFsm);
absFsm = GrabCreateAbstractFsm(network, coiBnvTable, absLatchTable,
absBnvTable,
GRAB_PARTITION_NOCHANGE,
FALSE);
/* pick refinement variables */
GrabRefineAbstractionByGrab(absFsm,
SORs,
absLatchTable,
absBnvTable,
addedVars,
addedBnvs,
refineDirection,
nodeToFaninNumberTable,
verbosity);
array_append(addedVarsAtCurrentLevel, addedVars);
array_append(addedBnvsAtCurrentLevel, addedBnvs);
array_free(addedVars);
array_free(addedBnvs);
/* Sanity check! */
auxValue2 = st_count(absLatchTable) +
((absBnvTable==NIL(st_table))? 0:st_count(absBnvTable));
assert(auxValue1 < auxValue2);
abstractLatchCount = st_count(absLatchTable);
abstractBnvCount = absBnvTable? st_count(absBnvTable):st_count(coiBnvTable);
refEndTime = util_cpu_ctime();
refTime += (refEndTime - refStartTime);
if (verbosity >= 3) {
fprintf(vis_stdout,
"-- grab: absLatch [%d/%d], absBnv [%d/%d], ref time is %5g s\n",
abstractLatchCount, concreteLatchCount,
abstractBnvCount, concreteBnvCount,
(double)(refEndTime - refStartTime)/1000.0);
}
refineIteration++;
}
/* Create The Refined Abstract FSM */
Fsm_FsmSubsystemFree(absFsm);
array_free(invisibleVarMddIds);
array_free(visibleVarMddIds);
absFsm = GrabCreateAbstractFsm(network, coiBnvTable, absLatchTable,
absBnvTable, partitionFlag, TRUE);
invisibleVarMddIds = GrabGetInvisibleVarMddIds(absFsm, absLatchTable,
absBnvTable);
visibleVarMddIds = GrabGetVisibleVarMddIds(absFsm, absLatchTable);
concreteBnvCount = st_count(coiBnvTable);
/* sanity check */
isLastStep = (array_n(invisibleVarMddIds)==0);
if (isLastStep) {
assert(abstractLatchCount == concreteLatchCount);
}
/* Reduce The Current SORs (with forward reachability analysis) */
mcStartTime = util_cpu_ctime();
rchStates = GrabFsmComputeConstrainedReachableStates(absFsm,
absLatchTable,
absBnvTable,
SORs,
verbosity);
mdd_array_free(SORs);
SORs = NIL(array_t);
mcEndTime = util_cpu_ctime();
mcTime += (mcEndTime - mcStartTime);
if (verbosity >= 2) {
fprintf(vis_stdout,
"-- grab: absLatch [%d/%d], absBnv [%d/%d], mc time is %5g s\n",
abstractLatchCount, concreteLatchCount,
abstractBnvCount, concreteBnvCount,
(double)(mcEndTime-mcStartTime)/1000.0);
}
/* if bad states is no longer reachable, break out */
flag = mdd_lequal(rchStates, invStates, 1, 1);
mdd_free(rchStates);
if (isLastStep || flag) {
if (!isLastStep && refineDirection == 1) {
runMinimization = 1;
refineDirection = 0;
continue;
}else
break;
}
/* Build the new SORs (with backward reachability analysis) */
Fsm_FsmFreeImageInfo(absFsm);
SORs = GrabFsmComputeSynchronousOnionRings(absFsm,
absLatchTable,
absBnvTable,
NIL(array_t),
invStates,
cexType,
verbosity);
sorEndTime = util_cpu_ctime();
sorTime += (sorEndTime - mcEndTime);
} /* End of the Inner Loop */
/* Minimize The Refinement Set of Boolean Network Variables (BNVs)
*/
if (fineGrainFlag==1 && refineMinFlag
&& array_n(addedBnvsAtCurrentLevel)>1) {
miniStartTime = util_cpu_ctime();
GrabMinimizeBnvRefinementSet(network,
coiBnvTable,
absLatchTable,
&absBnvTable,
addedBnvsAtCurrentLevel,
save_SORs,
verbosity);
abstractLatchCount = st_count(absLatchTable);
abstractBnvCount = st_count(absBnvTable);
miniEndTime = util_cpu_ctime();
miniTime += (miniEndTime - miniStartTime);
}
mdd_array_free(save_SORs);
/* Clean-ups
*/
Fsm_FsmSubsystemFree(absFsm);
absFsm = NIL(Fsm_Fsm_t);
array_free(invisibleVarMddIds);
array_free(visibleVarMddIds);
array_free(addedVarsAtCurrentLevel);
array_free(addedBnvsAtCurrentLevel);
addedVarsAtCurrentLevel = NIL(array_t);
addedBnvsAtCurrentLevel = NIL(array_t);
} /* End of the Outer Loop */
endTime = util_cpu_ctime();
totalTime = endTime - startTime;
/* Print out the debugging information */
if (dbgLevel > 0) {
FILE *tmpFile = vis_stdout;
extern FILE *vis_stdpipe;
if (debugFile)
vis_stdpipe = debugFile;
else if (useMore)
vis_stdpipe = popen("more", "w");
else
vis_stdpipe = vis_stdout;
vis_stdout = vis_stdpipe;
if (flag) {
fprintf(vis_stdout, "# %s: formula passed --- ", driverName);
Ctlp_FormulaPrint(vis_stdout, invFormula);
fprintf(vis_stdout, "\n");
}else {
if(dbgLevel != 2)
{
fprintf(vis_stdout, "# %s: formula p%d failed --- ", driverName, i+1);
Ctlp_FormulaPrint(vis_stdout, invFormula);
fprintf(vis_stdout, "\n# %s: calling debugger\n", driverName);
}
flag = !Bmc_AbstractCheckAbstractTraces(network, SORs, coiLatchTable,
1, dbgLevel, printInputs);
}
if (vis_stdout != tmpFile && vis_stdout != debugFile)
(void)pclose(vis_stdpipe);
vis_stdout = tmpFile;
}
if (verbosity >= 2 ) {
fprintf(vis_stdout, "\n-- grab: total cpu time = %5g\n",
(double)totalTime/1000.0);
if (verbosity >= 3) {
fprintf(vis_stdout, "-- grab: mc time = %5.1f\t(%3.1f%%)\n",
(double)mcTime/1000.0, (100.0*mcTime/totalTime));
fprintf(vis_stdout, "-- grab: sor time = %5.1f\t(%3.1f%%)\n",
(double)sorTime/1000.0, (100.0*sorTime/totalTime));
fprintf(vis_stdout, "-- grab: con time = %5.1f\t(%3.1f%%)\n",
(double)conTime/1000.0, (100.0*conTime/totalTime));
fprintf(vis_stdout, "-- grab: ref time = %5.1f\t(%3.1f%%)\n",
(double)refTime/1000.0, (100.0*refTime/totalTime));
fprintf(vis_stdout, "-- grab: min time = %5.1f\t(%3.1f%%)\n",
(double)miniTime/1000.0,(100.0*miniTime/totalTime));
fprintf(vis_stdout, "-- grab: dir time = %5.1f\t(%3.1f%%)\n",
(double)dirTime/1000.0, (100.0*dirTime/totalTime));
}
}
if (verbosity >= 1) {
if (concreteLatchCount > 0) {
fprintf(vis_stdout, "-- grab: abs latch percentage = %d %%\n",
100 * abstractLatchCount/concreteLatchCount );
}
if (verbosity >= 3) {
fprintf(vis_stdout, "-- grab: abs latch = %d\n", abstractLatchCount);
fprintf(vis_stdout, "-- grab: coi latch = %d\n", concreteLatchCount);
}
if (concreteBnvCount > 0) {
fprintf(vis_stdout, "-- grab: abs bnv percentage = %d %%\n",
(100 * abstractBnvCount/concreteBnvCount) );
if (verbosity >= 3) {
fprintf(vis_stdout, "-- grab: abs bnv = %d\n", abstractBnvCount);
fprintf(vis_stdout, "-- grab: coi bnv = %d\n", concreteBnvCount);
}
abstractBnvCount += abstractLatchCount;
concreteBnvCount += concreteLatchCount;
fprintf(vis_stdout, "-- grab: total abs var percentage = %d %%\n",
(100 * abstractBnvCount/concreteBnvCount) );
if (verbosity >= 3) {
fprintf(vis_stdout, "-- grab: abs var = %d\n",
abstractBnvCount);
fprintf(vis_stdout, "-- grab: coi var = %d\n",
concreteBnvCount);
}
}
fprintf(vis_stdout, "-- grab: total refinement iterations = %d\n",
refineIteration);
fprintf(vis_stdout, "-- grab: total image computations %d\n",
Img_GetNumberOfImageComputation(Img_Forward_c));
fprintf(vis_stdout, "-- grab: total preimage computations %d\n",
Img_GetNumberOfImageComputation(Img_Backward_c));
if (verbosity >= 3) {
GrabPrintNodeHashTable("AbstractLatchRankings", absLatchTable);
if (fineGrainFlag)
GrabPrintNodeHashTable("AbstractBnvRankings", absBnvTable);
}
}
/* Clean-up's
*/
st_free_table(coiLatchTable);
st_free_table(absLatchTable);
st_free_table(coiBnvTable);
if (fineGrainFlag) {
st_free_table(absBnvTable);
}
mdd_array_free(invStatesArray);
if (!flag) mdd_array_free(SORs);
Ctlsp_FormulaFree(invFormula_sp);
/* Store the verification results in an array (1--passed, 0--failed) */
array_insert(int, resultArray, i, flag);
}
/* print whether the set of invariants passed or failed
*/
fprintf(vis_stdout, "\n# %s: Summary of invariant pass/fail\n", driverName);
arrayForEachItem(Ctlp_Formula_t *, InvariantFormulaArray, i, invFormula) {
flag = array_fetch(int, resultArray, i);
if (flag) {
(void) fprintf(vis_stdout, "# %s: formula passed --- ", driverName);
Ctlp_FormulaPrint(vis_stdout, (invFormula));
fprintf(vis_stdout, "\n");
} else {
(void) fprintf(vis_stdout, "# %s: formula failed --- ", driverName);
Ctlp_FormulaPrint(vis_stdout, (invFormula));
fprintf(vis_stdout, "\n");
}
}
/* free the current partition and mdd manager if necessary */
if (partitionFlag) {
Ntk_NetworkFreeApplInfo(network, PART_NETWORK_APPL_KEY);
}
if (staticOrderFlag) {
mdd_quit(mddManager);
Ntk_NetworkSetMddManager(network, NIL(mdd_manager));
GrabNtkClearAllMddIds(network);
}
st_free_table(nodeToFaninNumberTable);
array_free(resultArray);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void TimeOutHandle | ( | void | ) | [static] |
Function********************************************************************
Synopsis [Handle function for timeout.]
Description [This function is called when the process receives a signal of type alarm. Since alarm is set with elapsed time, this function checks if the CPU time corresponds to the timeout of the command. If not, it reprograms the alarm to fire later and check if the CPU limit has been reached.]
SideEffects []
Definition at line 1162 of file grab.c.
{
longjmp(timeOutEnv, 1);
}
Here is the caller graph for this function:
Variable Documentation
jmp_buf timeOutEnv [static] |
CFile***********************************************************************
FileName [grab.c]
PackageName [grab]
Synopsis [Abstraction refinement for large scale invariant checking.]
Description [This file contains the functions to check invariant properties by the GRAB abstraction refinement algorithm. GRAB stands for "Generational Refinement of Ariadne's Bundle," in which the automatic refinement is guided by all shortest abstract counter-examples. For more information, please check the ICCAD'03 paper of Wang et al., "Improving Ariadne's Bundle by Following Multiple Counter-Examples in Abstraction Refinement." ]
Author [Chao Wang]
Copyright [Copyright (c) 2004 The Regents of the Univ. of Colorado. All rights reserved.
Permission is hereby granted, without written agreement and without license or royalty fees, to use, copy, modify, and distribute this software and its documentation for any purpose, provided that the above copyright notice and the following two paragraphs appear in all copies of this software.]
