#include "bmcInt.h"
Include dependency graph for bmcCmd.c:
Go to the source code of this file.
Functions | |
| static BmcOption_t * | ParseBmcOptions (int argc, char **argv) |
| static int | CommandBmc (Hrc_Manager_t **hmgr, int argc, char **argv) |
| static void | TimeOutHandle (void) |
| static void | DispatchBmcCommand (Ntk_Network_t *network, Ctlsp_Formula_t *ltlFormula, array_t *constraintArray, BmcOption_t *options) |
| static int | CommandCnfSat (Hrc_Manager_t **hmgr, int argc, char **argv) |
| void | Bmc_Init (void) |
| void | Bmc_End (void) |
| BmcOption_t * | BmcOptionAlloc (void) |
| void | BmcOptionFree (BmcOption_t *result) |
| char * | BmcCreateTmpFile (void) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: bmcCmd.c,v 1.83 2010/04/09 23:50:57 fabio Exp $" |
| static jmp_buf | timeOutEnv |
| static int | bmcTimeOut |
| static long | alarmLapTime |
Function Documentation
| void Bmc_End | ( | void | ) |
| void Bmc_Init | ( | void | ) |
AutomaticEnd Function********************************************************************
Synopsis [Initializes the BMC package.]
SideEffects []
SeeAlso [Bmc_End]
Definition at line 71 of file bmcCmd.c.
{
Cmd_CommandAdd("bounded_model_check", CommandBmc, /* doesn't change network */ 0);
Cmd_CommandAdd("cnf_sat", CommandCnfSat, /* doesn't change network */ 0);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| char* BmcCreateTmpFile | ( | void | ) |
Function********************************************************************
Synopsis [Create a temporary file]
Description []
SideEffects []
Definition at line 419 of file bmcCmd.c.
{
#if HAVE_MKSTEMP && HAVE_CLOSE
char cnfFileName[] = "/tmp/vis.XXXXXX";
int fd;
#else
char *cnfFileName;
char buffer[512];
#endif
#if HAVE_MKSTEMP && HAVE_CLOSE
fd = mkstemp(cnfFileName);
if (fd == -1){
#else
cnfFileName = util_strsav(tmpnam(buffer));
if (cnfFileName == NIL(char)){
#endif
(void)fprintf(vis_stderr,"** bmc error: Can not create temporary file. ");
(void)fprintf(vis_stderr,"Clean up /tmp and try again.\n");
return NIL(char);
}
#if HAVE_MKSTEMP && HAVE_CLOSE
close(fd);
#endif
return util_strsav(cnfFileName);
} /* createTmpFile() */
Here is the caller graph for this function:
| BmcOption_t* BmcOptionAlloc | ( | void | ) |
Function********************************************************************
Synopsis [Alloc Memory for BmcOption_t.]
SideEffects []
SeeAlso []
Definition at line 348 of file bmcCmd.c.
{
BmcOption_t *result = ALLOC(BmcOption_t, 1);
if (!result){
return result;
}
result->ltlFile = NIL(FILE);
result->fairFile = NIL(FILE);
result->cnfFileName = NIL(char);
result->minK = 0;
result->maxK = 1;
result->step = 1;
result->timeOutPeriod = 0;
result->startTime = 0;
result->verbosityLevel = BmcVerbosityNone_c;
result->dbgLevel = 0;
result->inductiveStep = 0;
result->printInputs = FALSE;
result->satSolverError = FALSE;
result->satInFile = NIL(char);
result->satOutFile = NIL(char);
result->incremental = 0;
result->earlyTermination = 0;
result->satSolver = CirCUs; /* default is 0 */
result->clauses = 0; /* default is 0 */
result->encoding = 0; /* default is 0 */
return result;
}
Here is the caller graph for this function:
| void BmcOptionFree | ( | BmcOption_t * | result | ) |
Function********************************************************************
Synopsis [Free BmcOption_t, and close files.]
SideEffects []
SeeAlso []
Definition at line 387 of file bmcCmd.c.
{
if (result->ltlFile != NIL(FILE)){
fclose(result->ltlFile);
}
if (result->cnfFileName != NIL(char)){
FREE(result->cnfFileName);
} else if (result->satInFile != NIL(char)) {
unlink(result->satInFile);
FREE(result->satInFile);
}
if (result->fairFile != NIL(FILE)){
fclose(result->fairFile);
}
if (result->satOutFile != NIL(char)) {
unlink(result->satOutFile);
FREE(result->satOutFile);
}
FREE(result);
}
Here is the caller graph for this function:
| static int CommandBmc | ( | Hrc_Manager_t ** | hmgr, |
| int | argc, | ||
| char ** | argv | ||
| ) | [static] |
Function********************************************************************
Synopsis [Implements the bounded_model_check command]
CommandName [bounded_model_check]
CommandSynopsis [Performs a SAT-based LTL model checking on a flattened network]
CommandArguments [\[-h\] \[-v <verbosity_level>\] \[-m <minimum_length>\] \[-k <maximum_length>\] \[-s <step_value>\] \[-r <termination_check_step>\] \[-e\] \[-F <fairness_file>\] \[-S <sat_solver>\] \[-E <encoding>\] \[-C <clause_type>\] \[-I <inc_level>\] \[-d <dbg_level>\] \[-t <timeOutPeriod>\] \[-o <cnf_file>\] \[-i\] \[-O <debug_file>\] <ltl_file> ]
CommandDescription [Performs a SAT-based LTL bounded model checking (BMC) on a flattened network. This command looks for a counterexample of length k ( minimum_length k maximum_length). If -r is specified, this command performs check for termination after each termination_check_step . If no counterexample is found, this command increases k by step_value (specifies by the -s option) until a counterexample is found, the search becomes intractable (timed out), or k reaches a bound (determine by the check for termination), and then we conclude that the LTL property passes.
This command implements the basic encoding of Bounded Model Checking (BMC) as descibed in the paper "Symbolic Model Checking without BDDs". However, the -E option can be used to select other encoding scheme. We also applied some of the improvements in the BMC encoding described in the paper "Improving the Encoding of LTL Model Checking into SAT".
To prove that an LTL property passes, we implement the termination methods that are descirebed in the papers "Checking Safety Properties Using Induction and a SAT-Solver" and "Proving More Properties with Bounded Model Checking".
Before calling this command, the user should have initialized the design by calling the command flatten_hierarchy. If the user uses the -r option and the LTL property is a general LTL property, the command build_partition_maigs must be called. The aig graph must be built by calling the command build_partition_mdds
Command options:
- -h
Print the command usage.
- -m
<minimum_length> Minimum length of counterexample to be checked (default is 0).
- -k
<maximum_length> Maximum length of counterexample to be checked (default is 1).
- -s
<step_value> Incrementing value of counterexample length (default is 1).
- -r
<termination_check_step> Check for termination for each termination_check_step (default is 0). 0 means don't check for termination.
- -e
Activate early termination check. Check if there is no simple path starts from an initial state. Valid only for general LTL and safety properties. Must be used with -r option.
- -S
<sat_solver> Specify SAT solver
sat_solvermust be one of the following:0: CirCUs (Default)1: zChaff- -E
<encoding> Specify encoding scheme
encodingmust be one of the following:0: The original BMC encoding (Default)1: SNF encoding2: Fixpoint encoding- -C
<clause_type> Specify clause type
encodingmust be one of the following:0: Apply CirCUs SAT solver on circuit (Default)1: Apply SAT solver on CNF generated form circuit2: Apply SAT solver on CNF- -I
<inc_level> Specify increment sat solver type
encodingmust be one of the following:1: Trace Objective (Default)2: Distill3: Trace Objective + Distill- -F
<fairness_file> Read fairness constraints from
<fairness_file>. Each formula in the file is a condition that must hold infinitely often on a fair path.- -o
<cnf_file>Save CNF formula in<cnf_file> - -O
<debug_file>Save counterexample to<debug_file> - -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.- -d
<dbg_level> Specify the amount of debugging performed when the BMC models check the LTL formula.
dbg_levelmust be one of the following:0: No debugging performed.dbg_level=0is the default.1: Debugging with minimal output: generate counter-example if the LTL formula fails and the counterexample length.- -i
Print input values causing transitions between states during debugging.
<ltl_file>File containing LTL formulae to be checked.
]
SideEffects []
SeeAlso [Ntk_NetworkAddApplInfo]
Definition at line 602 of file bmcCmd.c.
{
Ntk_Network_t *network;
BmcOption_t *options;
int i;
array_t *formulaArray;
array_t *LTLformulaArray;
bAig_Manager_t *manager;
array_t *constraintArray = NIL(array_t);
/*
* Parse command line options.
*/
if ((options = ParseBmcOptions(argc, argv)) == NIL(BmcOption_t)) {
return 1;
}
/*
* Read the network
*/
network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
if (network == NIL(Ntk_Network_t)) {
(void) fprintf(vis_stdout, "** bmc error: No network\n");
BmcOptionFree(options);
return 1;
}
manager = Ntk_NetworkReadMAigManager(network);
if (manager == NIL(mAig_Manager_t)) {
(void) fprintf(vis_stdout, "** bmc error: run build_partition_maigs command first\n");
BmcOptionFree(options);
return 1;
}
/*
We need the bdd when building the transition relation of the automaton
*/
if(options->inductiveStep !=0){
Fsm_Fsm_t *designFsm = NIL(Fsm_Fsm_t);
designFsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
if (designFsm == NIL(Fsm_Fsm_t)) {
return 1;
}
}
/* time out */
if (options->timeOutPeriod > 0) {
/* Set the static variables used by the signal handler. */
bmcTimeOut = options->timeOutPeriod;
alarmLapTime = options->startTime = util_cpu_ctime();
(void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
(void) alarm(options->timeOutPeriod);
if (setjmp(timeOutEnv) > 0) {
(void) fprintf(vis_stdout,
"\n# BMC: timeout occurred after %d seconds.\n",
options->timeOutPeriod);
(void) fprintf(vis_stdout, "# BMC: data may be corrupted.\n");
BmcOptionFree(options);
alarm(0);
return 1;
}
}
formulaArray = Ctlsp_FileParseFormulaArray(options->ltlFile);
if (formulaArray == NIL(array_t)) {
(void) fprintf(vis_stderr,
"** bmc error: error in parsing CTL* Fromula from file\n");
BmcOptionFree(options);
return 1;
}
if (array_n(formulaArray) == 0) {
(void) fprintf(vis_stderr, "** bmc error: No formula in file\n");
BmcOptionFree(options);
Ctlsp_FormulaArrayFree(formulaArray);
return 1;
}
LTLformulaArray = Ctlsp_FormulaArrayConvertToLTL(formulaArray);
Ctlsp_FormulaArrayFree(formulaArray);
if (LTLformulaArray == NIL(array_t)){
(void) fprintf(vis_stdout, "** bmc error: Invalid LTL formula\n");
BmcOptionFree(options);
return 1;
}
if (options->fairFile != NIL(FILE)) {
constraintArray = BmcReadFairnessConstraints(options->fairFile);
if(constraintArray == NIL(array_t)){
Ctlsp_FormulaArrayFree(LTLformulaArray);
BmcOptionFree(options);
return 1;
}
if(!Ctlsp_LtlFormulaArrayIsPropositional(constraintArray)){
Ctlsp_FormulaArrayAddLtlFairnessConstraints(LTLformulaArray,
constraintArray);
Ctlsp_FormulaArrayFree(constraintArray);
constraintArray = NIL(array_t);
}
}
/*
Call a proper BMC function based on LTL formula.
*/
for (i = 0; i < array_n(LTLformulaArray); i++) {
Ctlsp_Formula_t *ltlFormula = array_fetch(Ctlsp_Formula_t *,
LTLformulaArray, i);
DispatchBmcCommand(network, ltlFormula, constraintArray, options);
}
/*
Free used memeory
*/
if (constraintArray != NIL(array_t)){
Ctlsp_FormulaArrayFree(constraintArray);
}
Ctlsp_FormulaArrayFree(LTLformulaArray);
BmcOptionFree(options);
fflush(vis_stdout);
fflush(vis_stderr);
alarm(0);
return 0;
}/* CommandBmc() */
Here is the call graph for this function:
Here is the caller graph for this function:
| static int CommandCnfSat | ( | Hrc_Manager_t ** | hmgr, |
| int | argc, | ||
| char ** | argv | ||
| ) | [static] |
Function********************************************************************
Synopsis [cnf_sat]
Description []
CommandName [cnf_sat]
CommandSynopsis [Perform SAT solving with CNF input]
CommandArguments [\[-h\] \[-a <assgined_filename>\] \[-f <output_filename>\] \[-t <timeout>\] \[-v <verbose>\] \[-b\] <cnf_filename> ]
CommandDescription [Perform SAT solving with CirCUs after reading CNF file
-b
If the given CNF has small number of variables and clause then the BDD is built from the CNF clauses. If the monolithic BDD is built then we can conclude SAT or UNSAT, otherwise the normal SAT algorithm is invoked.
-t <timeOutPeriod>
Specify the time out period (in seconds) after which the command aborts. By default this option is set to infinity.
-f <output_filename> Specify the output filename to save the satisfying assignments and the statistics of SAT solving.
]
SideEffects []
SeeAlso []
Definition at line 977 of file bmcCmd.c.
{
satOption_t *option;
char *filename, c;
char *forcedAssignFilename;
int timeOutPeriod, i;
option = sat_InitOption();
timeOutPeriod = -1;
forcedAssignFilename = 0;
util_getopt_reset();
while ((c = util_getopt(argc, argv, "a:bf:ht:v:c:")) != EOF) {
switch(c) {
case 'h':
goto usage;
case 'b' :
option->BDDMonolithic = 1;
break;
case 'f' :
option->outFilename = strdup(util_optarg);
break;
case 'a' :
forcedAssignFilename = strdup(util_optarg);
break;
case 't' :
timeOutPeriod = atoi(util_optarg);
break;
case 'v':
for (i = 0; i < (int)(strlen(util_optarg)); i++) {
if (!isdigit((int)util_optarg[i])) {
goto usage;
}
}
option->verbose = (Bmc_VerbosityLevel) atoi(util_optarg);
break;
//Bing: for unsat core
case 'c':
option->coreGeneration = 1;
option->unsatCoreFileName = strdup(util_optarg);
option->minimizeConflictClause = 0;
option->clauseDeletionHeuristic = 0;
break;
default:
goto usage;
}
}
if (argc - util_optind == 0) {
(void) fprintf(vis_stderr, "** ERROR : file containing cnf file not provided\n");
goto usage;
}
else if (argc - util_optind > 1) {
(void) fprintf(vis_stderr, "** ERROR : too many arguments\n");
goto usage;
}
filename = util_strsav(argv[util_optind]);
if(forcedAssignFilename)
option->forcedAssignArr = sat_ReadForcedAssignment(forcedAssignFilename);
if (timeOutPeriod > 0) {
bmcTimeOut = timeOutPeriod;
alarmLapTime = util_cpu_ctime();
(void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
(void) alarm(timeOutPeriod);
if (setjmp(timeOutEnv) > 0) {
(void) fprintf(vis_stderr,
"** ERROR : timeout occurred after %d seconds.\n", timeOutPeriod);
alarm(0);
return 1;
}
}
sat_CNFMain(option, filename);
return 0;
usage:
(void) fprintf(vis_stderr, "usage: cnf_sat [-h] [-v verboseLevel] [-t timeout] <cnf_file>\n");
(void) fprintf(vis_stderr, " -h \tprint the command usage\n");
(void) fprintf(vis_stderr, " -a <filename> \tto make forced assignment\n");
(void) fprintf(vis_stderr, " -f <filename> \twrite log to the file\n");
(void) fprintf(vis_stderr, " -b \tuse BDD based method\n");
(void) fprintf(vis_stderr, " -v <verbosity_level>\n");
(void) fprintf(vis_stderr, " -t <period> time out period\n");
(void) fprintf(vis_stderr, " -c <filename> UNSAT core generation\n");
(void) fprintf(vis_stderr, " <cnf_file> CNF file to be checked.\n");
return 1;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void DispatchBmcCommand | ( | Ntk_Network_t * | network, |
| Ctlsp_Formula_t * | ltlFormula, | ||
| array_t * | constraintArray, | ||
| BmcOption_t * | options | ||
| ) | [static] |
Function********************************************************************
Synopsis [Dispatch BMC]
Description [Call a proper BMC routine.
The -E for BMC encoding scheme -C clause generation -S SAT solver 0 CirCUs 1 zChaff
]
SideEffects []
Definition at line 766 of file bmcCmd.c.
{
Ctlsp_Formula_t *negLtlFormula = Ctlsp_LtllFormulaNegate(ltlFormula);
st_table *CoiTable = st_init_table(st_ptrcmp, st_ptrhash);
assert(ltlFormula != NIL(Ctlsp_Formula_t));
assert(network != NIL(Ntk_Network_t));
/*
print out the given LTL formula
*/
fprintf(vis_stdout, "Formula: ");
Ctlsp_FormulaPrint(vis_stdout, ltlFormula);
fprintf(vis_stdout, "\n");
if (options->verbosityLevel >= BmcVerbosityMax_c){
fprintf(vis_stdout, "Negated formula: ");
Ctlsp_FormulaPrint(vis_stdout, negLtlFormula);
fprintf(vis_stdout, "\n");
}
/*
Compute the cone of influence of the LTL formula
*/
BmcGetCoiForLtlFormula(network, negLtlFormula, CoiTable);
if(options->clauses == 2){
/*
Generate clauses for each time frame. This is the old way of generating
clauses in BMC.
*/
if (constraintArray != NIL(array_t)){
BmcLtlVerifyGeneralLtl(network, negLtlFormula, CoiTable,
constraintArray, options);
} else /*
If the LTL formula is propositional.
*/
if(Ctlsp_isPropositionalFormula(negLtlFormula)){
BmcLtlVerifyProp(network, negLtlFormula, CoiTable, options);
} else /*
If the LTL formula is of type G(p) (its negation is
of type F(q)), where p and q are propositional.
*/
if(Ctlsp_LtlFormulaIsFp(negLtlFormula)){
BmcLtlVerifyGp(network, negLtlFormula, CoiTable, options);
} else /*
If the LTL formula is of type F(p) (its negation is
of type G(q)), where p and q are propositional.
*/
if (Ctlsp_LtlFormulaIsGp(negLtlFormula)){
BmcLtlVerifyFp(network, negLtlFormula, CoiTable, options);
} else /*
If the depth of the LTL formula (the maximum level
of nesting temporal operators) = 1
*/
/*
if (Ctlsp_LtlFormulaDepth(negLtlFormula) == 1){
BmcLtlVerifyUnitDepth(network, negLtlFormula, CoiTable, options);
} else
*/
/*
If the LTL formula is of type FG(p) (its negation is
of type GF(q)), where p and q are propositional.
*/
if(Ctlsp_LtlFormulaIsGFp(negLtlFormula)){
BmcLtlVerifyFGp(network, negLtlFormula, CoiTable, options);
} else
/*
All other LTL formulae
*/
BmcLtlVerifyGeneralLtl(network, negLtlFormula, CoiTable,
NIL(array_t), options);
} else {
/*
Build AIG for each time frame.
*/
if (constraintArray != NIL(array_t)){
if(options->encoding == 0){
BmcCirCUsLtlVerifyGeneralLtl(network, negLtlFormula,
CoiTable,
constraintArray, options, 0);
} else
if(options->encoding == 1){
BmcCirCUsLtlVerifyGeneralLtl(network, negLtlFormula,
CoiTable,
constraintArray, options, 1);
} else
if(options->encoding == 2){
BmcCirCUsLtlVerifyGeneralLtlFixPoint(network, negLtlFormula,
CoiTable,
constraintArray, options);
}
} else
/*
If the LTL formula is propositional.
*/
if(Ctlsp_isPropositionalFormula(negLtlFormula)){
BmcCirCUsLtlVerifyProp(network, negLtlFormula, CoiTable, options);
} else
/*
If the LTL formula is of type G(p) (its negation is
of type F(q)), where p and q are propositional.
*/
if(Ctlsp_LtlFormulaIsFp(negLtlFormula)){
BmcCirCUsLtlVerifyGp(network, negLtlFormula, CoiTable, options);
} else
/*
If the LTL formula is of type F(p) (its negation is
of type G(q)), where p and q are propositional.
*/
if (Ctlsp_LtlFormulaIsGp(negLtlFormula)){
BmcCirCUsLtlVerifyFp(network, negLtlFormula, CoiTable, options);
} else
/*
If the depth of the LTL formula (the maximum level
of nesting temporal operators) = 1
if (Ctlsp_LtlFormulaDepth(negLtlFormula) == 1){
BmcLtlVerifyUnitDepth(network, negLtlFormula, CoiTable, options);
} else
If the LTL formula is of type FG(p) (its negation is
of type GF(q)), where p and q are propositional.
*/
if(Ctlsp_LtlFormulaIsGFp(negLtlFormula)){
BmcCirCUsLtlVerifyFGp(network, negLtlFormula, CoiTable, options);
} else
if(Ctlsp_LtlFormulaTestIsSyntacticallyCoSafe(negLtlFormula) ||
(Ltl_AutomatonGetStrength(BmcAutLtlToAutomaton(network,ltlFormula)) == 0))
{
BmcCirCUsLtlCheckSafety(network, negLtlFormula, options, CoiTable);
}
else {
/*
All other LTL formulae
*/
if(options->encoding == 0){
BmcCirCUsLtlVerifyGeneralLtl(network, negLtlFormula,
CoiTable,
NIL(array_t), options, 0);
} else
if(options->encoding == 1){
BmcCirCUsLtlVerifyGeneralLtl(network, negLtlFormula,
CoiTable,
NIL(array_t), options, 1);
} else
if(options->encoding == 2){
BmcCirCUsLtlVerifyGeneralLtlFixPoint(network, negLtlFormula,
CoiTable,
NIL(array_t), options);
}
}
}
st_free_table(CoiTable);
Ctlsp_FormulaFree(negLtlFormula);
} /* DispatchBmcCommand() */
Here is the call graph for this function:
Here is the caller graph for this function:
| static BmcOption_t * ParseBmcOptions | ( | int | argc, |
| char ** | argv | ||
| ) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [Parse the user input for command "bmc".]
Description []
SideEffects []
Definition at line 107 of file bmcCmd.c.
{
BmcOption_t *options = BmcOptionAlloc();
char *ltlFileName = NIL(char);
unsigned int i;
int c;
if (!options){
return NIL(BmcOption_t);
}
options->dbgOut = 0;
/*
* Parse command line options.
*/
util_getopt_reset();
while ((c = util_getopt(argc, argv, "E:C:S:F:O::I:hiv:m:k:s:o:t:d:r:e")) != EOF) {
switch(c) {
case 'F':
options->fairFile = Cmd_FileOpen(util_optarg, "r", NIL(char *), 0);
if (options->fairFile == NIL(FILE)) {
(void) fprintf(vis_stdout,
"** bmc error: Cannot open the file %s\n",
util_optarg);
BmcOptionFree(options);
return NIL(BmcOption_t);
}
break;
case 'O':
options->dbgOut = Cmd_FileOpen(util_optarg, "w", NIL(char *), 0);
if(options->dbgOut == NIL(FILE)) {
(void) fprintf(vis_stdout, "**bmc error: Cannot open %s for debug information.\n", util_optarg);
BmcOptionFree(options);
return NIL(BmcOption_t);
}
break;
case 'm':
for (i = 0; i < strlen(util_optarg); i++) {
if (!isdigit((int)util_optarg[i])) {
goto usage;
}
}
options->minK = atoi(util_optarg);
break;
case 'k':
for (i = 0; i < strlen(util_optarg); i++) {
if (!isdigit((int)util_optarg[i])) {
goto usage;
}
}
options->maxK = atoi(util_optarg);
break;
case 's':
for (i = 0; i < strlen(util_optarg); i++) {
if (!isdigit((int)util_optarg[i])) {
goto usage;
}
}
options->step = atoi(util_optarg);
break;
case 'r':
for (i = 0; i < strlen(util_optarg); i++) {
if (!isdigit((int)util_optarg[i])) {
goto usage;
}
}
options->inductiveStep = atoi(util_optarg);
break;
case 'e':
options->earlyTermination = TRUE;
break;
case 'd':
for (i = 0; i < strlen(util_optarg); i++) {
if (!isdigit((int)util_optarg[i])) {
goto usage;
}
}
options->dbgLevel = atoi(util_optarg);
break;
case 't' :
options->timeOutPeriod = atoi(util_optarg);
break;
case 'i':
options->printInputs = TRUE;
break;
case 'h':
goto usage;
case 'v':
for (i = 0; i < strlen(util_optarg); i++) {
if (!isdigit((int)util_optarg[i])) {
goto usage;
}
}
options->verbosityLevel = (Bmc_VerbosityLevel) atoi(util_optarg);
break;
case 'o':
options->cnfFileName = util_strsav(util_optarg);
break;
case 'I' :
options->incremental = atoi(util_optarg);
break;
case 'E':
for (i = 0; i < strlen(util_optarg); i++) {
if (!isdigit((int)util_optarg[i])) {
goto usage;
}
}
options->encoding = atoi(util_optarg);
if((options->encoding < 0) || (options->encoding > 2)){
goto usage;
}
break;
case 'S':
for (i = 0; i < strlen(util_optarg); i++) {
if (!isdigit((int)util_optarg[i])) {
goto usage;
}
}
options->satSolver = atoi(util_optarg);
if((options->satSolver < 0) || (options->satSolver > 1)){
goto usage;
}
break;
case 'C':
for (i = 0; i < strlen(util_optarg); i++) {
if (!isdigit((int)util_optarg[i])) {
goto usage;
}
}
options->clauses = atoi(util_optarg);
if((options->clauses < 0) || (options->clauses > 2)){
goto usage;
}
break;
default:
goto usage;
}
}
if (options->minK > options->maxK){
(void) fprintf(vis_stderr, "** bmc error: value for -m option must not be greater than vlaue for -k option\n");
goto usage;
}
/*
* Open the ltl file.
*/
if (argc - util_optind == 0) {
(void) fprintf(vis_stderr, "** bmc error: file containing ltl formulae not provided\n");
goto usage;
}
else if (argc - util_optind > 1) {
(void) fprintf(vis_stderr, "** bmc error: too many arguments\n");
goto usage;
}
ltlFileName = util_strsav(argv[util_optind]);
/* Read LTL Formulae */
if (!ltlFileName)
goto usage;
options->ltlFile = Cmd_FileOpen(ltlFileName, "r", NIL(char *), 0);
if (options->ltlFile == NIL(FILE)) {
(void) fprintf(vis_stdout,"** bmc error: Cannot open the file %s\n", ltlFileName);
FREE(ltlFileName);
BmcOptionFree(options);
return NIL(BmcOption_t);
}
FREE(ltlFileName);
/* create SAT Solver input file */
if (options->cnfFileName == NIL(char)) {
options->satInFile = BmcCreateTmpFile();
if (options->satInFile == NIL(char)){
BmcOptionFree(options);
return NIL(BmcOption_t);
}
} else {
options->satInFile = options->cnfFileName;
}
/* create SAT Solver output file */
options->satOutFile = BmcCreateTmpFile();
if (options->satOutFile == NIL(char)){
BmcOptionFree(options);
return NIL(BmcOption_t);
}
return options;
usage:
(void) fprintf(vis_stderr, "usage: bmc [-h][-m minimum_length][-k maximum_length][-s step][-r inductive_step][-e][-F <fairness_file>][-d debug_level][-E <encoding>][-C <clauses>][-S <sat_solver>][-O <debug_file>][-I <level>][-v verbosity_level][-t period][-o <cnf_file>] <ltl_file>\n");
(void) fprintf(vis_stderr, " -h \tprint the command usage\n");
(void) fprintf(vis_stderr, " -m \tminimum length of counterexample to be checked (default is 0)\n");
(void) fprintf(vis_stderr, " -k \tmaximum length of counterexample to be checked (default is 1)\n");
(void) fprintf(vis_stderr, " -s \tincrementing value of counterexample length (default is 1)\n");
(void) fprintf(vis_stderr, " -r \tUse check for termination at each inductive_step to check if the property passes (default is 0).\n");
(void) fprintf(vis_stderr, " -e \tUse early termination to check if the property passes. Valid only with -r \n");
(void) fprintf(vis_stderr, " -F <fairness_file>\n");
(void) fprintf(vis_stderr, " -d <debug_level>\n");
(void) fprintf(vis_stderr, " debug_level = 0 => No debugging performed (Default)\n");
(void) fprintf(vis_stderr, " debug_level = 1 => Debugging with minimal output: generate counter-example if the LTL formula fails.\n");
(void) fprintf(vis_stderr, " debug_level = 2 => Debugging with full output in Aiger format: generate counter-example if the LTL formula fails.\n");
(void) fprintf(vis_stderr, " -O <debug_file>\n");
(void) fprintf(vis_stderr, " -i \tPrint input values in debug traces.\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, " -t <period> time out period\n");
(void) fprintf(vis_stderr, " -E <encoding>\n");
(void) fprintf(vis_stderr, " encoding = 0 => Original BMC encoding (Default)\n");
(void) fprintf(vis_stderr, " encoding = 1 => SNF encoding\n");
(void) fprintf(vis_stderr, " encoding = 2 => Fixpoint encoding\n");
/*
(void) fprintf(vis_stderr, " encoding = 3 => FNF encoding\n");
*/
(void) fprintf(vis_stderr, " -S <sat_solver>\n");
(void) fprintf(vis_stderr, " sat_solver = 0 => CirCUs (Default)\n");
(void) fprintf(vis_stderr, " sat_solver = 1 => cusp\n");
(void) fprintf(vis_stderr, " -C <clauses>\n");
(void) fprintf(vis_stderr, " clauses = 0 => Apply CirCUs on circuit (Default)\n");
(void) fprintf(vis_stderr, " clauses = 1 => Apply SAT solver on CNF (new)\n");
(void) fprintf(vis_stderr, " clauses = 2 => Apply SAT solver on CNF (old)\n");
(void) fprintf(vis_stderr, " -I <level>\n");
(void) fprintf(vis_stderr, " level = 1 => Trace Objective\n");
(void) fprintf(vis_stderr, " level = 2 => Distill\n");
(void) fprintf(vis_stderr, " level = 3 => Trace Objective + Distill\n");
(void) fprintf(vis_stderr, " -o <cnf_file> contains CNF of the counterexample\n");
(void) fprintf(vis_stderr, " <ltl_file> The input file containing LTL formulae to be checked.\n");
BmcOptionFree(options);
return NIL(BmcOption_t);
}
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 time out occurs. Since alarm is set with an elapsed time, this function checks if the CPU time corresponds to the timeout of the command. If not, it reprograms the alarm to fire again later.]
SideEffects []
Definition at line 735 of file bmcCmd.c.
{
int seconds = (int) ((util_cpu_ctime() - alarmLapTime) / 1000);
if (seconds < bmcTimeOut) {
unsigned slack = (unsigned) (bmcTimeOut - seconds);
(void) signal(SIGALRM, (void(*)(int)) TimeOutHandle);
(void) alarm(slack);
} else {
longjmp(timeOutEnv, 1);
}
} /* TimeOutHandle */
Here is the caller graph for this function:
Variable Documentation
long alarmLapTime [static] |
int bmcTimeOut [static] |
jmp_buf timeOutEnv [static] |
char rcsid [] UNUSED = "$Id: bmcCmd.c,v 1.83 2010/04/09 23:50:57 fabio Exp $" [static] |
CFile***********************************************************************
FileName [bmcCmd.c]
PackageName [bmc]
Synopsis [Command interface for bounded model checking (bmc)]
Author [Mohammad Awedh]
Copyright [This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.]
