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:
<refine_algorithm>
refine_algorithm must be one of the following:
GRAB: the GRAB refinement method (Default).
<cex_type>
cex_type must be one of the following:
0: minterm state counter-example.
1: cube state counter-example.
2: synchronous onion rings (Default).
<dbg_level>
dbg_level must be one of the following:
0: No debugging performed.
dbg_level=0 is the default.
1: Generate a counter-example (a path to a fair cycle).
<finegrain_flag>
finegrain_flag must be one of the following:
0: disable fine-grain abstraction.
1: enable fine-grain abstraction (Default).
<refinemin_flag>
refinemin_flag must be one of the following:
0: disable greedy refinement minimization.
1: enable greedy refinement minimization (Default).
<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.
<dbg_out>
See also commands : model_check, check_invariant ]
SideEffects []
******************************************************************************/
static int
CommandGrab(
Hrc_Manager_t ** hmgr,
int argc,
char ** argv)
{
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]