#include "bmcInt.h"
Include dependency graph for bmcBmc.c:
Go to the source code of this file.
Functions | |
| static int | checkIndex (int index, BmcCnfClauses_t *cnfClauses) |
| static int | doAnd (int left, int right) |
| static int | doOr (int left, int right) |
| void | BmcLtlVerifyProp (Ntk_Network_t *network, Ctlsp_Formula_t *ltlFormula, st_table *CoiTable, BmcOption_t *options) |
| int | BmcLtlCheckInductiveInvariant (Ntk_Network_t *network, bAigEdge_t property, BmcOption_t *options, st_table *CoiTable) |
| void | BmcLtlVerifyGp (Ntk_Network_t *network, Ctlsp_Formula_t *ltlFormula, st_table *CoiTable, BmcOption_t *options) |
| void | BmcLtlVerifyFp (Ntk_Network_t *network, Ctlsp_Formula_t *ltlFormula, st_table *CoiTable, BmcOption_t *options) |
| void | BmcLtlVerifyFGp (Ntk_Network_t *network, Ctlsp_Formula_t *ltlFormula, st_table *CoiTable, BmcOption_t *options) |
| void | BmcLtlVerifyUnitDepth (Ntk_Network_t *network, Ctlsp_Formula_t *ltlFormula, st_table *CoiTable, BmcOption_t *options) |
| void | BmcLtlVerifyGeneralLtl (Ntk_Network_t *network, Ctlsp_Formula_t *ltlFormula, st_table *CoiTable, array_t *constraintArray, BmcOption_t *options) |
| int | BmcGenerateCnfForLtl (Ntk_Network_t *network, Ctlsp_Formula_t *ltlFormula, int i, int k, int l, BmcCnfClauses_t *cnfClauses) |
| void | BmcLtlCheckSafety (Ntk_Network_t *network, Ctlsp_Formula_t *ltlFormula, BmcOption_t *options, st_table *CoiTable) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: bmcBmc.c,v 1.72 2005/10/14 04:41:11 awedh Exp $" |
Function Documentation
| int BmcGenerateCnfForLtl | ( | Ntk_Network_t * | network, |
| Ctlsp_Formula_t * | ltlFormula, | ||
| int | i, | ||
| int | k, | ||
| int | l, | ||
| BmcCnfClauses_t * | cnfClauses | ||
| ) |
Function********************************************************************
Synopsis [Generate CNF for an LTL formula]
Description [Generate array of clauses for a trnasition from state i to state k. If l is non-zero, it will also generate the clauses from state l to state i.
if the clause array is empty {}, the propety is always TRUE if the the clause array has one empty clause {{}}, the property is always FALSE. return the clause index number. ]
SideEffects []
SeeAlso []
Definition at line 2028 of file bmcBmc.c.
{
int left, right, cnfIndex;
int andIndex, orIndex;
int j, n;
int leftValue, rightValue, andValue, orValue;
mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
array_t *clause, *tmpclause, *orClause, *rightClause, *leftClause;
BmcCnfStates_t *state;
assert(ltlFormula != NIL(Ctlsp_Formula_t));
right = 0;
rightValue = 0;
if(Ctlsp_isPropositionalFormula(ltlFormula)){
bAigEdge_t property = BmcCreateMaigOfPropFormula(network, manager, ltlFormula);
if (property == bAig_Zero){ /* FALSE */
/* add an empty clause to indicate FALSE property */
BmcAddEmptyClause(cnfClauses);
return 0;
}
if (property == bAig_One){ /* TRUE */
/* Don't generate any clause to indicate TRUE property.*/
return 0;
}
/* Generate the clause of the propositional formula */
/* The state of the input variables is the same as the state of the state variables. */
cnfIndex = BmcGenerateCnfFormulaForAigFunction(manager, property, i, cnfClauses);
return cnfIndex;
}
/*
* Formula is NOT propositional formula
*/
switch(ltlFormula->type) {
case Ctlsp_NOT_c:
/* reach here if formula-left is always not propositional*/
/* NOT must only appears infront of a propositional formula.*/
if (!Ctlsp_isPropositionalFormula(ltlFormula->left)){
fprintf(vis_stderr,"BMC error: the LTL formula is not in NNF\n");
return 0;
}
/*
return -1*BmcGenerateCnfForLtlNoLoop(network, ltlFormula->left, i, k,
cnfIndexTable, clauseArray);
*/
break;
case Ctlsp_AND_c:
/*
c = a * b --> (!a + !b + c) * (a + !c) * (b + !c).
Because a and b must be one, so we need only the last two clauses.
*/
state = BmcCnfClausesFreeze(cnfClauses);
rightValue = 1;
left = BmcGenerateCnfForLtl(network, ltlFormula->left, i, k, l, cnfClauses);
leftValue = checkIndex(left, cnfClauses);
if (leftValue !=0){
right = BmcGenerateCnfForLtl(network, ltlFormula->right, i, k, l, cnfClauses);
rightValue = checkIndex(right, cnfClauses);
}
if ((leftValue == 0) || (rightValue == 0)){
/* restore the information */
BmcCnfClausesRestore(cnfClauses, state);
/* add an empty clause*/
BmcAddEmptyClause(cnfClauses);
FREE(state);
return 0; /* FALSE */
}
if ((leftValue == 1) && (rightValue == 1)){
/* restore the information */
BmcCnfClausesRestore(cnfClauses, state);
FREE(state);
return 0; /* TRUE */
}
BmcCnfClausesUnFreeze(cnfClauses, state);
FREE(state);
/*
tmpclause = array_alloc(int, 3);
array_insert(int, tmpclause, 0, -left);
array_insert(int, tmpclause, 1, -right);
array_insert(int, tmpclause, 2, cnfIndex);
array_insert_last(array_t *, clauseArray, tmpclause);
*/
if (leftValue == 1){
return right;
}
if (rightValue == 1){
return left;
}
cnfIndex = cnfClauses->cnfGlobalIndex++;
tmpclause = array_alloc(int, 2);
array_insert(int, tmpclause, 0, left);
array_insert(int, tmpclause, 1, -cnfIndex);
BmcCnfInsertClause(cnfClauses, tmpclause);
array_insert(int, tmpclause, 0, right);
array_insert(int, tmpclause, 1, -cnfIndex);
BmcCnfInsertClause(cnfClauses, tmpclause);
array_free(tmpclause);
return cnfIndex;
case Ctlsp_OR_c:
/*
c = a + b --> (a + b + !c) * (!a + c) * (!b + c).
Because a and b must be one, so we need only the first clause.
*/
state = BmcCnfClausesFreeze(cnfClauses);
left = BmcGenerateCnfForLtl(network, ltlFormula->left, i, k, l, cnfClauses);
leftValue = checkIndex(left, cnfClauses);
if (leftValue !=1){
right = BmcGenerateCnfForLtl(network, ltlFormula->right, i, k, l, cnfClauses);
rightValue = checkIndex(right, cnfClauses);
}
if ((leftValue == 1) || (rightValue == 1)){
/* restore the information */
BmcCnfClausesRestore(cnfClauses, state);
FREE(state);
return 0; /* TRUE */
}
if ((leftValue == 0) && (rightValue == 0)){
/* restore the information */
BmcCnfClausesRestore(cnfClauses, state);
/* add an empty clause*/
BmcAddEmptyClause(cnfClauses);
FREE(state);
return 0; /* FALSE */
}
BmcCnfClausesUnFreeze(cnfClauses, state);
FREE(state);
/* Either leftValue or rightValue = 0 and the other != 1
At least one clause will be added
*/
if (leftValue == 0){
return right;
}
if (rightValue == 0){
return left;
}
cnfIndex = cnfClauses->cnfGlobalIndex++;
tmpclause = array_alloc(int, 0);
array_insert_last(int, tmpclause, -cnfIndex);
array_insert_last(int, tmpclause, left);
/*
tmpclause = array_alloc(int, 2);
array_insert(int, tmpclause, 0, -left);
array_insert(int, tmpclause, 1, cnfIndex);
array_insert_last(array_t *, clauseArray, tmpclause);
*/
array_insert_last(int, tmpclause, right);
/*
tmpclause = array_alloc(int, 2);
array_insert(int, tmpclause, 0, -right);
array_insert(int, tmpclause, 1, cnfIndex);
array_insert_last(array_t *, clauseArray, tmpclause);
*/
BmcCnfInsertClause(cnfClauses, tmpclause);
array_free(tmpclause);
return cnfIndex;
case Ctlsp_F_c:
if (l >= 0){ /* loop */
i = (l < i)? l: i;
}
cnfIndex = cnfClauses->cnfGlobalIndex++;
clause = array_alloc(int, 0);
for (j=i; j<= k; j++){
left = BmcGenerateCnfForLtl(network, ltlFormula->left, j, k, l, cnfClauses);
leftValue = checkIndex(left, cnfClauses);
if (leftValue != -1){
array_free(clause);
return 0;
}
array_insert_last(int, clause, left);
/*
tmpclause = array_alloc(int, 2);
array_insert(int, tmpclause, 1, cnfIndex);
array_insert(int, tmpclause, 0, -left);
array_insert_last(array_t *, clauseArray, tmpclause);
*/
}
array_insert_last(int, clause, -cnfIndex);
BmcCnfInsertClause(cnfClauses, clause);
array_free(clause);
return cnfIndex;
case Ctlsp_G_c:
if (l < 0){ /* FALSE */
/* add an empty clause */
BmcAddEmptyClause(cnfClauses);
return 0;
} else {
i = (l < i)? l: i;
andIndex = cnfClauses->cnfGlobalIndex++;
for (j=i; j<= k; j++){
left = BmcGenerateCnfForLtl(network, ltlFormula->left, j, k, l, cnfClauses);
leftValue = checkIndex(left, cnfClauses);
if (leftValue != -1){
return 0;
}
tmpclause = array_alloc(int, 2);
array_insert(int, tmpclause, 0, left);
array_insert(int, tmpclause, 1, -andIndex);
BmcCnfInsertClause(cnfClauses, tmpclause);
array_free(tmpclause);
}/* for j loop*/
} /* else */
return andIndex;
case Ctlsp_X_c:
/* X left */
if((l >= 0) && (i == k) ){
i = l;
} else if (i < k){
i = i + 1;
} else { /* FALSE */
/* add an empty clause */
BmcAddEmptyClause(cnfClauses);
return 0;
}
return BmcGenerateCnfForLtl(network, ltlFormula->left, i, k, l, cnfClauses);
case Ctlsp_U_c: /* (left U right) */
state = BmcCnfClausesFreeze(cnfClauses);
leftValue = 1; /* left is TRUE*/
rightValue = 1; /* right is TRUE*/
orIndex = cnfClauses->cnfGlobalIndex++;
orClause = array_alloc(int, 0);
array_insert_last(int, orClause, -orIndex);
orValue = 0;
for (j=i; j<= k; j++){
right = BmcGenerateCnfForLtl(network, ltlFormula->right, j, k, l, cnfClauses);
rightValue = checkIndex(right, cnfClauses);
andIndex = cnfClauses->cnfGlobalIndex++;
if (rightValue == -1){
rightClause = array_alloc(int, 2);
array_insert(int, rightClause, 0, right);
array_insert(int, rightClause, 1, -andIndex);
BmcCnfInsertClause(cnfClauses, rightClause);
array_free(rightClause);
}
andValue = rightValue;
for (n=i; (n <= j-1) && (andValue != 0); n++){
left = BmcGenerateCnfForLtl(network, ltlFormula->left, n, k, l, cnfClauses);
leftValue = checkIndex(left, cnfClauses);
andValue = doAnd(andValue, leftValue);
if (leftValue == -1){
leftClause = array_alloc(int, 2);
array_insert(int, leftClause, 0, left);
array_insert(int, leftClause, 1, -andIndex);
BmcCnfInsertClause(cnfClauses, leftClause);
array_free(leftClause);
}
} /* for n loop */
orValue = doOr(orValue, andValue);
if (orValue == 1){ /* TRUE */
break;
}
if (andValue != 0){
array_insert_last(int, orClause, andIndex);
}
} /* for j loop*/
if ( (l >=0) && (orValue !=1)){ /* loop */
for (j=l; j<= i-1; j++){
right = BmcGenerateCnfForLtl(network, ltlFormula->right, j, k, l, cnfClauses);
rightValue = checkIndex(right, cnfClauses);
andIndex = cnfClauses->cnfGlobalIndex++;
if (rightValue == -1){
rightClause = array_alloc(int, 2);
array_insert(int, rightClause, 0, right);
array_insert(int, rightClause, 1, -andIndex);
BmcCnfInsertClause(cnfClauses, rightClause);
array_free(rightClause);
}
andValue = rightValue;
for (n=i; (n<= k) && (andValue != 0); n++){
left = BmcGenerateCnfForLtl(network, ltlFormula->left, n, k, l, cnfClauses);
leftValue = checkIndex(left, cnfClauses);
andValue = doAnd(andValue, leftValue);
if (leftValue == -1){
leftClause = array_alloc(int, 2);
array_insert(int, leftClause, 0, left);
array_insert(int, leftClause, 1, -andIndex);
BmcCnfInsertClause(cnfClauses, leftClause);
array_free(leftClause);
}
} /* for n loop */
for (n=l; (n<= j-1) && (andValue != 0); n++){
left = BmcGenerateCnfForLtl(network, ltlFormula->left, n, k, l, cnfClauses);
leftValue = checkIndex(left, cnfClauses);
andValue = doAnd(andValue, leftValue);
if (leftValue == -1){
leftClause = array_alloc(int, 2);
array_insert(int, leftClause, 0, left);
array_insert(int, leftClause, 1, -andIndex);
BmcCnfInsertClause(cnfClauses, leftClause);
array_free(leftClause);
}
} /* for n loop */
orValue = doOr(orValue, andValue);
if (orValue == 1){ /* TRUE */
break;
}
if (andValue != 0){
array_insert_last(int, orClause, andIndex);
}
}/* j loop*/
} /* if (l>=0) */
if ((orValue == 1) || (orValue == 0)){
/*restore the infomration back*/
BmcCnfClausesRestore(cnfClauses, state);
FREE(state);
array_free(orClause);
if (orValue == 0){
/* add an empty clause*/
BmcAddEmptyClause(cnfClauses);
}
return 0;
} else {
BmcCnfClausesUnFreeze(cnfClauses, state);
FREE(state);
BmcCnfInsertClause(cnfClauses, orClause);
array_free(orClause);
return orIndex;
}
case Ctlsp_R_c:
/* (left R right) */
state = BmcCnfClausesFreeze(cnfClauses);
orIndex = cnfClauses->cnfGlobalIndex++;
orClause = array_alloc(int, 0);
array_insert_last(int, orClause, -orIndex);
orValue = 0;
if (l >= 0){ /* loop */
andIndex = cnfClauses->cnfGlobalIndex++;
andValue = 1;
for (j=(i<l?i:l); (j<= k) && (andValue != 0); j++){
right = BmcGenerateCnfForLtl(network, ltlFormula->right, j, k, l, cnfClauses);
rightValue = checkIndex(right, cnfClauses);
andValue = doAnd(andValue, rightValue);
if (rightValue == -1){
rightClause = array_alloc(int, 2);
array_insert(int, rightClause, 0, right);
array_insert(int, rightClause, 1, -andIndex);
BmcCnfInsertClause(cnfClauses, rightClause);
array_free(rightClause);
}
} /* for j loop*/
if (andValue == -1){
array_insert_last(int, orClause, andIndex);
}
orValue = doOr(orValue, andValue);
} /* loop */
if(orValue != 1){
for (j=i; j<= k; j++){
left = BmcGenerateCnfForLtl(network, ltlFormula->left,
j, k, l, cnfClauses);
leftValue = checkIndex(left, cnfClauses);
andIndex = cnfClauses->cnfGlobalIndex++;
if (leftValue == -1){
leftClause = array_alloc(int, 2);
array_insert(int, leftClause, 0, left);
array_insert(int, leftClause, 1, -andIndex);
BmcCnfInsertClause(cnfClauses, leftClause);
array_free(leftClause);
}
andValue = leftValue;
for (n=i; (n<= j) && (andValue != 0); n++){
right = BmcGenerateCnfForLtl(network, ltlFormula->right,
n, k, l, cnfClauses);
rightValue = checkIndex(right, cnfClauses);
andValue = doAnd(andValue, rightValue);
if (rightValue == -1){
rightClause = array_alloc(int, 2);
array_insert(int, rightClause, 0, right);
array_insert(int, rightClause, 1, -andIndex);
BmcCnfInsertClause(cnfClauses, rightClause);
array_free(rightClause);
}
} /* for n loop */
orValue = doOr(orValue, andValue);
if (orValue == 1){ /* TRUE */
break;
}
if (andValue != 0){
array_insert_last(int, orClause, andIndex);
}
}/* for j loop*/
if ((l >= 0) && (orValue !=1)) { /* loop */
for (j=l; j<= i-1; j++){
left = BmcGenerateCnfForLtl(network, ltlFormula->left,
j, k, l, cnfClauses);
leftValue = checkIndex(left, cnfClauses);
andIndex = cnfClauses->cnfGlobalIndex++;
if (leftValue == -1){
leftClause = array_alloc(int, 2);
array_insert(int, leftClause, 0, left);
array_insert(int, leftClause, 1, -andIndex);
BmcCnfInsertClause(cnfClauses, leftClause);
array_free(leftClause);
}
andValue = leftValue;
for (n=i; (n<= k) && (andValue != 0); n++){
right = BmcGenerateCnfForLtl(network, ltlFormula->right,
n, k, l, cnfClauses);
rightValue = checkIndex(right, cnfClauses);
andValue = doAnd(andValue, rightValue);
if (rightValue == -1){
rightClause = array_alloc(int, 2);
array_insert(int, rightClause, 0, right);
array_insert(int, rightClause, 1, -andIndex);
BmcCnfInsertClause(cnfClauses, rightClause);
array_free(rightClause);
}
} /* for n loop */
for (n=l; (n<= j) && (andValue != 0); n++){
right = BmcGenerateCnfForLtl(network, ltlFormula->right,
n, k, l, cnfClauses);
rightValue = checkIndex(right, cnfClauses);
andValue = doAnd(andValue, rightValue);
if (rightValue == -1){
rightClause = array_alloc(int, 2);
array_insert(int, rightClause, 0, right);
array_insert(int, rightClause, 1, -andIndex);
BmcCnfInsertClause(cnfClauses, rightClause);
array_free(rightClause);
}
} /* for n loop */
orValue = doOr(orValue, andValue);
if (orValue == 1){ /* TRUE */
break;
}
if (andValue != 0){
array_insert_last(int, orClause, andIndex);
}
} /* for j loop*/
} /* if (l>=0) */
}/* orValue !=1*/
if ((orValue == 1) || (orValue == 0)){
/*restore the infomration back*/
BmcCnfClausesRestore(cnfClauses, state);
FREE(state);
array_free(orClause);
if (orValue == 0){
/* add an empty clause*/
BmcAddEmptyClause(cnfClauses);
}
return 0;
} else {
BmcCnfClausesUnFreeze(cnfClauses, state);
FREE(state);
BmcCnfInsertClause(cnfClauses, orClause);
array_free(orClause);
return orIndex;
}
default:
fail("Unexpected LTL formula type");
break;
}
return -1; /* we should never get here */
}
Here is the call graph for this function:
Here is the caller graph for this function:
| int BmcLtlCheckInductiveInvariant | ( | Ntk_Network_t * | network, |
| bAigEdge_t | property, | ||
| BmcOption_t * | options, | ||
| st_table * | CoiTable | ||
| ) |
Function********************************************************************
Synopsis [Check if the LTL formula in the form G(p) (invariant), where p is a propositional formula, is an Inductive Invariant]
Description [Check if the LTL formula in the form G(p), where p is a propositional formula, is an Inductive Invariant
An LTL formula G(p), where p is a propositional formul, is an inductive invariant if the following two conditions hold:
1- p holds in all the intial states. 2- If p holds in a state s, then it also holds in all states that are reachable from s.
G(p) is an inductive invariant if : SAT( I(0) and !p(0)) return UNSAT and SAT( p(i) and T(i, i+1) and !p(i+1)) returns UNSAT.
Return value: 0 if the property is not an inductive invariant 1 if the property is an inductive invariant -1 error ]
SideEffects []
SeeAlso []
Definition at line 217 of file bmcBmc.c.
{
mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
BmcCnfClauses_t *cnfClauses = NIL(BmcCnfClauses_t);
array_t *unitClause;
int cnfIndex;
array_t *result = NIL(array_t);
FILE *cnfFile;
st_table *nodeToMvfAigTable = NIL(st_table); /* maps each node to its mvfAig */
int savedVerbosityLevel = options->verbosityLevel;
int returnValue = 0; /* the property is not an inductive invariant */
cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
if (cnfFile == NIL(FILE)) {
(void) fprintf(vis_stderr,
"** bmc error: Cannot create CNF output file %s\n",
options->satInFile);
return -1;
}
/*
nodeToMvfAigTable Maps each node to its Multi-function And/Inv graph
*/
nodeToMvfAigTable =
(st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
assert(nodeToMvfAigTable != NIL(st_table));
/*
Clause database
*/
cnfClauses = BmcCnfClausesAlloc();
/*
Check if the property holds in all intial states
*/
/*
Generate CNF clauses for initial states
*/
BmcCnfGenerateClausesForPath(network, 0, 0, BMC_INITIAL_STATES,
cnfClauses, nodeToMvfAigTable, CoiTable);
/*
Generate CNF clauses for the property
*/
cnfIndex = BmcGenerateCnfFormulaForAigFunction(manager, property, 0, cnfClauses);
unitClause = array_alloc(int, 1);
array_insert(int, unitClause, 0, cnfIndex); /* because property is the negation of
the LTL formula*/
BmcCnfInsertClause(cnfClauses, unitClause);
options->verbosityLevel = BmcVerbosityNone_c;
BmcWriteClauses(manager, cnfFile, cnfClauses, options);
(void) fclose(cnfFile);
result = BmcCheckSAT(options);
options->verbosityLevel = (Bmc_VerbosityLevel) savedVerbosityLevel;
BmcCnfClausesFree(cnfClauses);
if (options->satSolverError){
return -1;
}
if (result == NIL(array_t)){ /* the property holds at all initial states */
cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
if (cnfFile == NIL(FILE)) {
(void) fprintf(vis_stderr,
"** bmc error: Cannot create CNF output file %s\n",
options->satInFile);
return -1;
}
/*
Check if the property holds in state i, it also holds in state i+1
*/
cnfClauses = BmcCnfClausesAlloc();
/*
Generate CNF clauses for a transition from state i to state i+1.
*/
BmcCnfGenerateClausesForPath(network, 0, 1, BMC_NO_INITIAL_STATES,
cnfClauses, nodeToMvfAigTable, CoiTable);
cnfIndex = BmcGenerateCnfFormulaForAigFunction(manager, property, 0, cnfClauses);
array_insert(int, unitClause, 0, -cnfIndex); /* because property is the negation of
the LTL formula */
BmcCnfInsertClause(cnfClauses, unitClause);
cnfIndex = BmcGenerateCnfFormulaForAigFunction(manager, property, 1, cnfClauses);
array_insert(int, unitClause, 0, cnfIndex); /* because property is the negation of
the LTL formula */
BmcCnfInsertClause(cnfClauses, unitClause);
options->verbosityLevel = BmcVerbosityNone_c;
BmcWriteClauses(manager, cnfFile, cnfClauses, options);
(void) fclose(cnfFile);
result = BmcCheckSAT(options);
options->verbosityLevel = (Bmc_VerbosityLevel) savedVerbosityLevel;
BmcCnfClausesFree(cnfClauses);
if (options->satSolverError){
returnValue = -1;
}
if (result != NIL(array_t)){
returnValue = 0; /* the property is not an inductive invariant */
} else {
returnValue = 1; /* the property is an inductive invariant */
}
}
array_free(unitClause);
return returnValue;
} /* BmcLtlCheckInductiveInvariant() */
Here is the call graph for this function:
Here is the caller graph for this function:
| void BmcLtlCheckSafety | ( | Ntk_Network_t * | network, |
| Ctlsp_Formula_t * | ltlFormula, | ||
| BmcOption_t * | options, | ||
| st_table * | CoiTable | ||
| ) |
Function********************************************************************
Synopsis [Apply bmc on an abbreviation-free LTL formula that expresses safety propery]
Description [If an LTL formula expresses a safety property, we generate CNF 0 caluse for the part with no loop: [[f]] k ]
SideEffects []
SeeAlso []
Definition at line 2524 of file bmcBmc.c.
{
mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
st_table *nodeToMvfAigTable = NIL(st_table); /* node to mvfAig */
BmcCnfClauses_t *cnfClauses = NIL(BmcCnfClauses_t);
FILE *cnfFile;
int noLoopIndex;
array_t *result = NIL(array_t);
int leftValue = 0;
long startTime, endTime;
int k;
int minK = options->minK;
int maxK = options->maxK;
boolean boundedFormula;
int depth;
array_t *unitClause = array_alloc(int, 1);
array_t *orClause = array_alloc(int, 2);
/* ************** */
/* Initialization */
/* ************** */
startTime = util_cpu_ctime();
/* nodeToMvfAigTable maps each node to its multi-function And/Inv graph */
nodeToMvfAigTable =
(st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
assert(nodeToMvfAigTable != NIL(st_table));
/* For bounded formulae use a tighter upper bound if possible. */
boundedFormula = Ctlsp_LtlFormulaTestIsBounded(ltlFormula, &depth);
if (boundedFormula && depth < maxK && depth >= minK) {
maxK = depth;
}
if (options->verbosityLevel != BmcVerbosityNone_c){
(void) fprintf(vis_stdout, "saftey LTL BMC\n");
if (boundedFormula){
(void) fprintf(vis_stdout, "Bounded formula of depth %d\n", depth);
}
(void) fprintf(vis_stdout, "Apply BMC on counterexample of length >= %d and <= %d (+%d) \n",
minK, maxK, options->step);
}
k= minK;
while( (result == NIL(array_t)) && (k <= maxK)){
if (options->verbosityLevel == BmcVerbosityMax_c) {
(void) fprintf(vis_stdout, "\nGenerate counterexample of length %d\n", k);
}
cnfClauses = BmcCnfClausesAlloc();
cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
if (cnfFile == NIL(FILE)) {
(void)fprintf(vis_stderr,
"** bmc error: Cannot create CNF output file %s\n",
options->satInFile);
return;
}
BmcCnfGenerateClausesForPath(network, 0, k, BMC_INITIAL_STATES,
cnfClauses, nodeToMvfAigTable, CoiTable);
noLoopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, -1, cnfClauses);
leftValue = checkIndex(noLoopIndex, cnfClauses);
if(leftValue == 1){
assert(k==1);
if (options->verbosityLevel != BmcVerbosityNone_c){
(void) fprintf(vis_stdout,"# BMC: formula failed\n");
(void) fprintf(vis_stdout,"# BMC: Empty counterexample because the property is always FALSE\n");
}
break;
} else if(leftValue == 0){
if (options->verbosityLevel != BmcVerbosityNone_c){
(void) fprintf(vis_stdout,"# BMC: the formula is trivially true");
(void) fprintf(vis_stdout," for counterexamples of length %d\n", k);
}
/*
break;
*/
} else {
array_insert(int, unitClause, 0, noLoopIndex);
BmcCnfInsertClause(cnfClauses, unitClause);
BmcWriteClauses(manager, cnfFile, cnfClauses, options);
(void) fclose(cnfFile);
result = BmcCheckSAT(options);
if (options->satSolverError){
break;
}
if(result != NIL(array_t)) {
(void) fprintf(vis_stdout, "# BMC: formula failed\n");
if(options->verbosityLevel != BmcVerbosityNone_c){
(void) fprintf(vis_stdout,
"# BMC: Found a counterexample of length = %d \n", k);
}
if (options->dbgLevel == 1) {
BmcPrintCounterExample(network, nodeToMvfAigTable, cnfClauses,
result, k, CoiTable, options, NIL(array_t));
}
break;
}
}
/* free all used memories */
BmcCnfClausesFree(cnfClauses);
#if 0
/*
Check induction
*/
{
BmcCnfClauses_t *noLoopCnfClauses = BmcCnfClausesAlloc();
array_t *noLoopResult = NIL(array_t);
array_t *unitClause = array_alloc(int, 1);
int i;
printf("Check Induction \n");
cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
if (cnfFile == NIL(FILE)) {
(void)fprintf(vis_stderr,
"** bmc error: Cannot create CNF output file %s\n",
options->satInFile);
return;
}
/*
Generate a loop free path
*/
BmcCnfGenerateClausesForLoopFreePath(network, 0, k+1, BMC_NO_INITIAL_STATES,
noLoopCnfClauses, nodeToMvfAigTable, CoiTable);
/*
The property true at states from 0 to k
*/
unitClause = array_alloc(int, 1);
for(i=0; i<=k; i++){
array_insert(int, unitClause, 0,
-BmcGenerateCnfForLtl(network, ltlFormula, i, k, -1, noLoopCnfClauses));
BmcCnfInsertClause(noLoopCnfClauses, unitClause);
}
/*
The property fails at k +1
*/
array_insert(int, unitClause, 0,
BmcGenerateCnfForLtl(network, ltlFormula, 0, k+1, -1, noLoopCnfClauses));
BmcCnfInsertClause(noLoopCnfClauses, unitClause);
array_free(unitClause);
BmcWriteClauses(manager, cnfFile, noLoopCnfClauses, options);
(void) fclose(cnfFile);
noLoopResult = BmcCheckSAT(options);
if(noLoopResult == NIL(array_t)) {
(void) fprintf(vis_stdout, "# BMC: formula passed\n");
(void) fprintf(vis_stdout,
"# BMC: No more loop free path \n");
break;
}
/*
BmcPrintCounterExample(network, nodeToMvfAigTable, noLoopCnfClauses,
noLoopResult, bound+1, CoiTable, options, NIL(array_t));
*/
BmcCnfClausesFree(noLoopCnfClauses);
} /* Check induction */
#endif
k += options->step;
#if 0
/* Check if reach the depth of the model */
cnfClauses = BmcCnfClausesAlloc();
cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
if (cnfFile == NIL(FILE)) {
(void)fprintf(vis_stderr,
"** bmc error: Cannot create CNF output file %s\n",
options->satInFile);
return;
}
/*
Generate a loop free path
*/
{
BmcCnfGenerateClausesForPath(network, 0, k, BMC_INITIAL_STATES,
cnfClauses, nodeToMvfAigTable, CoiTable);
/*
initIndex = BmcCnfGenerateClausesFromStateToState(network, -1, 0, cnfClauses, nodeToMvfAigTable, CoiTable, -1);
noLoopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, -1, cnfClauses);
array_insert(int, orClause, 0, initIndex);
array_insert(int, orClause, 1, -noLoopIndex);
BmcCnfInsertClause(cnfClauses, orClause);
*/
BmcWriteClauses(manager, cnfFile, cnfClauses, options);
(void) fclose(cnfFile);
result = BmcCheckSAT(options);
if(result == NIL(array_t)) {
(void) fprintf(vis_stdout, "# BMC: formula passed\n");
(void) fprintf(vis_stdout,
"# BMC: No more loop free path \n");
return;
}
/*
BmcPrintCounterExample(network, nodeToMvfAigTable, cnfClauses,
result, k, CoiTable, options, NIL(array_t));
*/
result = NIL(array_t);
}
BmcCnfClausesFree(cnfClauses);
/* Check if reach the depth of the model */
cnfClauses = BmcCnfClausesAlloc();
cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
if (cnfFile == NIL(FILE)) {
(void)fprintf(vis_stderr,
"** bmc error: Cannot create CNF output file %s\n",
options->satInFile);
return;
}
/*
Generate a loop free path
*/
{
BmcCnfGenerateClausesForPath(network, 0, k, BMC_NO_INITIAL_STATES,
cnfClauses, nodeToMvfAigTable, CoiTable);
/*
initIndex = BmcCnfGenerateClausesFromStateToState(network, -1, 0, cnfClauses, nodeToMvfAigTable, CoiTable, -1);
*/
noLoopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, -1, cnfClauses);
array_insert(int, unitClause, 0, noLoopIndex);
BmcCnfInsertClause(cnfClauses, unitClause);
/*
array_insert(int, orClause, 0, initIndex);
array_insert(int, orClause, 1, -noLoopIndex);
BmcCnfInsertClause(cnfClauses, orClause);
*/
BmcWriteClauses(manager, cnfFile, cnfClauses, options);
(void) fclose(cnfFile);
result = BmcCheckSAT(options);
if(result == NIL(array_t)) {
(void) fprintf(vis_stdout, "# BMC: (Bad state) formula passed\n");
(void) fprintf(vis_stdout,
"# BMC: No more loop free path \n");
return;
}
/*
BmcPrintCounterExample(network, nodeToMvfAigTable, cnfClauses,
result, k, CoiTable, options, NIL(array_t));
*/
result = NIL(array_t);
}
BmcCnfClausesFree(cnfClauses);
#endif
} /* while result and k*/
if (options->satSolverError == FALSE){
if ((result == NIL(array_t)) && (k > maxK)){
if (boundedFormula && depth <= options->maxK){
(void) fprintf(vis_stdout,"# BMC: formula passed\n");
} else {
(void) fprintf(vis_stdout,"# BMC: formula undecided\n");
}
if (options->verbosityLevel != BmcVerbosityNone_c){
(void) fprintf(vis_stdout,
"# BMC: no counterexample found of length up to %d \n",
maxK);
}
}
}
/* free all used memories */
if (k == 0){
BmcCnfClausesFree(cnfClauses);
}
if(result != NIL(array_t)){
array_free(result);
}
if (options->verbosityLevel != BmcVerbosityNone_c) {
endTime = util_cpu_ctime();
fprintf(vis_stdout, "-- bmc time = %10g\n",
(double)(endTime - startTime) / 1000.0);
}
array_free(unitClause);
array_free(orClause);
fflush(vis_stdout);
return;
} /* BmcLtlCheckSafety() */
Here is the call graph for this function:
| void BmcLtlVerifyFGp | ( | Ntk_Network_t * | network, |
| Ctlsp_Formula_t * | ltlFormula, | ||
| st_table * | CoiTable, | ||
| BmcOption_t * | options | ||
| ) |
Function********************************************************************
Synopsis [Apply Bounded Model Checking (BMC) on an LTL formula of the form FG(p), where p is propositional.]
Description [Given a model M, an LTL formula f = FGp, and a bound k, we first find a k-loop counterexample of length k at which p false inside the loop. If -r switch of the BMC command is specified, we apply the method in the paper "Proving More Properties with Bounded Model Checking" to check if the property f passes.
Note: Before calling this function, the LTL formula must be negated.
]
SideEffects []
SeeAlso []
Definition at line 945 of file bmcBmc.c.
{
mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
st_table *nodeToMvfAigTable = NIL(st_table); /* node to mvfAig */
BmcCnfClauses_t *cnfClauses = NIL(BmcCnfClauses_t);
FILE *cnfFile;
array_t *orClause, *tmpClause, *loopClause;
int k, l, andIndex, loop;
array_t *result = NIL(array_t);
long startTime, endTime;
int minK = options->minK;
int maxK = options->maxK;
Ctlsp_Formula_t *propFormula;
bAigEdge_t property;
Bmc_PropertyStatus formulaStatus;
int bmcError = FALSE;
int m=-1, n=-1;
int checkLevel = 0;
/*
Refer to Theorem 1 in the paper "Proving More Properties with Bounded Model Checking"
If checkLevel == 0 --> check for beta' only. If UNSAT, m=k and chekLevel = 1
If checkLevel == 1 --> check for beta only. If UNSAT, checkLevel = 2.
If checkLevel == 2 --> check for alpha only. If UNSAT, n=k and checkLevel = 3.
If gama is UNSAT up to (m+n-1) and checkLvel = 3, formula passes.
checkLevel = 4 if (m+n-1) > maxK; */
/*
Remember the LTL property was negated
*/
assert(Ctlsp_LtlFormulaIsGFp(ltlFormula));
/* ************** */
/* Initialization */
/* ************** */
loopClause = NIL(array_t);
startTime = util_cpu_ctime();
/*
nodeToMvfAigTable maps each node to its multi-function And/Inv graph
*/
nodeToMvfAigTable =
(st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
if (nodeToMvfAigTable == NIL(st_table)){
(void) fprintf(vis_stderr,
"** bmc error: you need to build the AIG structure first\n");
return;
}
propFormula = Ctlsp_FormulaReadRightChild(Ctlsp_FormulaReadRightChild(ltlFormula));
property = BmcCreateMaigOfPropFormula(network, manager, propFormula);
if (options->verbosityLevel != BmcVerbosityNone_c){
(void)fprintf(vis_stdout, "LTL formula is of type FG(p)\n");
(void) fprintf(vis_stdout, "Apply BMC on counterexample of length >= %d and <= %d (+%d) \n",
minK, maxK, options->step);
}
tmpClause = array_alloc(int, 2);
k= minK;
formulaStatus = BmcPropertyUndecided_c;
while( (result == NIL(array_t)) && (k <= maxK)){
/*
Search for a k-loop counterexample of length k.
*/
if (options->verbosityLevel == BmcVerbosityMax_c) {
(void) fprintf(vis_stdout, "\nGenerate counterexample of length %d\n", k);
}
/*
Create a clause database
*/
cnfClauses = BmcCnfClausesAlloc();
cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
if (cnfFile == NIL(FILE)) {
(void)fprintf(vis_stderr,
"** bmc error: Cannot create CNF output file %s\n",
options->satInFile);
bmcError = TRUE;
break;
}
/**********************************************
\gama(k)
***********************************************/
/*
Generate an initialized path of length k.
*/
BmcCnfGenerateClausesForPath(network, 0, k, BMC_INITIAL_STATES, cnfClauses, nodeToMvfAigTable, CoiTable);
/*
k-loop
*/
orClause = array_alloc(int, 0);
loopClause = array_alloc(int, k+1);
for(l=0; l<=k; l++){
/*
Use to check if there is a loop from k to l.
*/
loop = cnfClauses->cnfGlobalIndex++;
BmcCnfGenerateClausesFromStateToState(network, k, l, cnfClauses, nodeToMvfAigTable, CoiTable, loop);
array_insert(int, loopClause, l, loop);
andIndex = cnfClauses->cnfGlobalIndex++;
array_insert(int, tmpClause, 0, loop);
array_insert(int, tmpClause, 1, -andIndex);
BmcCnfInsertClause(cnfClauses, tmpClause);
/*
l
If [[F p]] if p true in a state from l to k.
k
*/
array_insert(int, tmpClause, 0,
BmcGenerateCnfForLtl(network, Ctlsp_FormulaCreate(Ctlsp_F_c, propFormula, NIL(Ctlsp_Formula_t)),
l, k, -1, cnfClauses));
BmcCnfInsertClause(cnfClauses, tmpClause);
array_insert_last(int, orClause, andIndex);
} /* for l loop */
BmcCnfInsertClause(cnfClauses, orClause);
array_free(orClause);
BmcWriteClauses(manager, cnfFile, cnfClauses, options);
(void) fclose(cnfFile);
result = BmcCheckSAT(options);
if(options->satSolverError){
break;
}
if(result != NIL(array_t)) {
formulaStatus = BmcPropertyFailed_c;
break;
}
array_free(loopClause);
/* free all used memories */
BmcCnfClausesFree(cnfClauses);
/* ====================================================================
Use termination criteria to prove that the property passes.
==================================================================== */
if((result == NIL(array_t)) &&
(options->inductiveStep !=0) &&
(k % options->inductiveStep == 0)
)
{
array_t *unitClause = array_alloc(int, 0);
array_t *result = NIL(array_t);
int savedVerbosityLevel = options->verbosityLevel;
options->verbosityLevel = BmcVerbosityNone_c;
/* ===========================
Early termination condition
=========================== */
if(options->earlyTermination){
if (savedVerbosityLevel == BmcVerbosityMax_c) {
(void) fprintf(vis_stdout, "\nChecking the early termination at k= %d\n", k);
}
cnfClauses = BmcCnfClausesAlloc();
cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
if (cnfFile == NIL(FILE)) {
(void)fprintf(vis_stderr,
"** abmc error: Cannot create CNF output file %s\n",
options->satInFile);
bmcError = TRUE;
break;
}
/*
Generate an initialized simple path path of length k.
*/
BmcCnfGenerateClausesForLoopFreePath(network, 0, k, BMC_INITIAL_STATES,
cnfClauses, nodeToMvfAigTable, CoiTable);
BmcWriteClauses(manager, cnfFile, cnfClauses, options);
(void) fclose(cnfFile);
BmcCnfClausesFree(cnfClauses);
result = BmcCheckSAT(options);
if(options->satSolverError){
break;
}
if(result == NIL(array_t)) {
formulaStatus = BmcPropertyPassed_c;
if (savedVerbosityLevel == BmcVerbosityMax_c) {
(void) fprintf(vis_stdout, "# BMC: By early termination\n");
}
break;
}
} /* Early termination */
/*
Check \beta''(k)
*/
if(checkLevel == 0){
int i;
cnfClauses = BmcCnfClausesAlloc();
if (savedVerbosityLevel == BmcVerbosityMax_c) {
(void) fprintf(vis_stdout, "# BMC: Check beta'' \n");
}
cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
if (cnfFile == NIL(FILE)) {
(void)fprintf(vis_stderr,
"** bmc error: Cannot create CNF output file %s\n",
options->satInFile);
bmcError = TRUE;
break;
}
/*
Generate a simple path of length k+1.
*/
BmcCnfGenerateClausesForLoopFreePath(network, 0, k+1, BMC_NO_INITIAL_STATES,
cnfClauses, nodeToMvfAigTable, CoiTable);
for(i=1; i<=k+1; i++){
array_insert(int, unitClause, 0,
-BmcGenerateCnfFormulaForAigFunction(manager, property,
i, cnfClauses));
BmcCnfInsertClause(cnfClauses, unitClause);
}
array_insert(int, unitClause, 0,
BmcGenerateCnfFormulaForAigFunction(manager, property,
0, cnfClauses));
BmcCnfInsertClause(cnfClauses, unitClause);
BmcWriteClauses(manager, cnfFile, cnfClauses, options);
(void) fclose(cnfFile);
result = BmcCheckSAT(options);
BmcCnfClausesFree(cnfClauses);
if(options->satSolverError){
break;
}
if(result == NIL(array_t)) {
m = k;
printf("Beta'': Value of m = %d\n", m);
checkLevel = 1;
}
} /* Check for beta'' */
/*
Check \beta'(k)
*/
if(checkLevel == 0){
int i;
cnfClauses = BmcCnfClausesAlloc();
if (savedVerbosityLevel == BmcVerbosityMax_c) {
(void) fprintf(vis_stdout, "# BMC: Check beta' \n");
}
cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
if (cnfFile == NIL(FILE)) {
(void)fprintf(vis_stderr,
"** bmc error: Cannot create CNF output file %s\n",
options->satInFile);
bmcError = TRUE;
break;
}
/*
Generate a simple path of length k+1.
*/
BmcCnfGenerateClausesForLoopFreePath(network, 0, k+1, BMC_NO_INITIAL_STATES,
cnfClauses, nodeToMvfAigTable, CoiTable);
for(i=0; i<=k; i++){
array_insert(int, unitClause, 0,
-BmcGenerateCnfFormulaForAigFunction(manager, property,
i, cnfClauses));
BmcCnfInsertClause(cnfClauses, unitClause);
}
array_insert(int, unitClause, 0,
BmcGenerateCnfFormulaForAigFunction(manager, property,
k+1, cnfClauses));
BmcCnfInsertClause(cnfClauses, unitClause);
BmcWriteClauses(manager, cnfFile, cnfClauses, options);
(void) fclose(cnfFile);
result = BmcCheckSAT(options);
BmcCnfClausesFree(cnfClauses);
if(options->satSolverError){
break;
}
if(result == NIL(array_t)) {
m = k;
printf("Beta': Value of m = %d\n", m);
checkLevel = 1;
}
} /* Check for beta' */
/*
Check for beta
*/
if(checkLevel == 1){
cnfClauses = BmcCnfClausesAlloc();
if (savedVerbosityLevel == BmcVerbosityMax_c) {
(void) fprintf(vis_stdout, "# BMC: Check beta\n");
}
cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
if (cnfFile == NIL(FILE)) {
(void)fprintf(vis_stderr,
"** bmc error: Cannot create CNF output file %s\n",
options->satInFile);
bmcError = TRUE;
break;
}
/*
Generate a simple path of length k+1.
*/
BmcCnfGenerateClausesForLoopFreePath(network, 0, k+1, BMC_NO_INITIAL_STATES,
cnfClauses, nodeToMvfAigTable, CoiTable);
array_insert(int, unitClause, 0,
-BmcGenerateCnfFormulaForAigFunction(manager, property,
k, cnfClauses));
BmcCnfInsertClause(cnfClauses, unitClause);
array_insert(int, unitClause, 0,
BmcGenerateCnfFormulaForAigFunction(manager, property,
k+1, cnfClauses));
BmcCnfInsertClause(cnfClauses, unitClause);
BmcWriteClauses(manager, cnfFile, cnfClauses, options);
(void) fclose(cnfFile);
result = BmcCheckSAT(options);
BmcCnfClausesFree(cnfClauses);
if(options->satSolverError){
break;
}
if(result == NIL(array_t)) {
checkLevel = 2;
}
} /* Check beta */
if(checkLevel == 2){ /* we check \alpha if \beta UNSAT */
if (savedVerbosityLevel == BmcVerbosityMax_c) {
(void) fprintf(vis_stdout, "# BMC: Check alpha \n");
}
/*
\alpha(k)
*/
cnfClauses = BmcCnfClausesAlloc();
cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
if (cnfFile == NIL(FILE)) {
(void)fprintf(vis_stderr,
"** bmc error: Cannot create CNF output file %s\n",
options->satInFile);
bmcError = TRUE;
break;
}
/*
Generate an initialized path of length k.
*/
BmcCnfGenerateClausesForLoopFreePath(network, 0, k, BMC_INITIAL_STATES,
cnfClauses, nodeToMvfAigTable, CoiTable);
array_insert(int, unitClause, 0,
BmcGenerateCnfFormulaForAigFunction(manager, property,
k, cnfClauses));
BmcCnfInsertClause(cnfClauses, unitClause);
BmcWriteClauses(manager, cnfFile, cnfClauses, options);
(void) fclose(cnfFile);
result = BmcCheckSAT(options);
BmcCnfClausesFree(cnfClauses);
if(options->satSolverError){
break;
}
if(result == NIL(array_t)) {
n = k;
checkLevel = 3;
printf("m=%d n=%d\n",m,n);
if ((m+n-1) <= maxK){
maxK = m+n-1;
} else {
checkLevel = 4;
}
}
}/* Check alpha */
array_free(unitClause);
options->verbosityLevel = (Bmc_VerbosityLevel) savedVerbosityLevel;
} /* Prove the property passes*/
k += options->step;
} /* while result and k*/
if (bmcError == FALSE){
if(options->satSolverError){
(void) fprintf(vis_stdout,"# BMC: Error in calling SAT solver\n");
} else {
if(checkLevel == 3){
(void) fprintf(vis_stdout, "# BMC: (m+n-1) Complete the theorem\n");
formulaStatus = BmcPropertyPassed_c;
}
if(formulaStatus == BmcPropertyFailed_c) {
(void) fprintf(vis_stdout, "# BMC: formula failed\n");
if(options->verbosityLevel != BmcVerbosityNone_c){
(void) fprintf(vis_stdout,
"# BMC: Found a counterexample of length = %d \n", k);
}
if (options->dbgLevel == 1) {
BmcPrintCounterExample(network, nodeToMvfAigTable, cnfClauses,
result, k, CoiTable, options, loopClause);
BmcCnfClausesFree(cnfClauses);
array_free(loopClause);
}
} else if(formulaStatus == BmcPropertyPassed_c) {
(void) fprintf(vis_stdout, "# BMC: formula Passed\n");
} else if(formulaStatus == BmcPropertyUndecided_c) {
(void) fprintf(vis_stdout,"# BMC: formula undecided\n");
if (options->verbosityLevel != BmcVerbosityNone_c){
(void) fprintf(vis_stdout,
"# BMC: no counterexample found of length up to %d \n",
maxK);
}
}
}
}
/*
free all used memories
*/
array_free(tmpClause);
if(result != NIL(array_t)){
array_free(result);
}
if (options->verbosityLevel != BmcVerbosityNone_c) {
endTime = util_cpu_ctime();
fprintf(vis_stdout, "-- abmc time = %10g\n",
(double)(endTime - startTime) / 1000.0);
}
fflush(vis_stdout);
return;
} /* BmcLtlVerifyGFp() */
Here is the call graph for this function:
Here is the caller graph for this function:
| void BmcLtlVerifyFp | ( | Ntk_Network_t * | network, |
| Ctlsp_Formula_t * | ltlFormula, | ||
| st_table * | CoiTable, | ||
| BmcOption_t * | options | ||
| ) |
Function********************************************************************
Synopsis [Apply Bounded Model Checking (BMC) on an LTL formula of the form F(p), where p is propositional.]
Description [Given a model M, an LTL formula f = Fp, and a bound k, we first find a k-loop counterexample of length k at which all states violate p. If -r switch of the BMC command is specified, we apply the method in the paper "Proving More Properties with Bounded Model Checking" to check if the property f passes.
Note: Before calling this function, the LTL formula must be negated.
] SideEffects []
SeeAlso []
Definition at line 688 of file bmcBmc.c.
{
mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
st_table *nodeToMvfAigTable = NIL(st_table); /* maps each node to its mvfAig */
BmcCnfClauses_t *cnfClauses = NIL(BmcCnfClauses_t);
FILE *cnfFile;
array_t *unitClause= array_alloc(int, 1), *outClause;
int outIndex;
int k;
array_t *result = NIL(array_t);
long startTime, endTime;
bAigEdge_t property;
int bound;
int bmcError = FALSE;
Bmc_PropertyStatus formulaStatus = BmcPropertyUndecided_c;
assert(Ctlsp_LtlFormulaIsGp(ltlFormula));
startTime = util_cpu_ctime();
if (options->verbosityLevel != BmcVerbosityNone_c){
(void)fprintf(vis_stdout, "LTL formula is of type F(p)\n");
}
property = BmcCreateMaigOfPropFormula(network, manager, ltlFormula->right);
if (property == mAig_NULL){
return;
}
if (property == bAig_One){
(void) fprintf(vis_stdout, "# BMC: formula failed\n");
(void) fprintf(vis_stdout, " Empty counterexample because the property is always FALSE\n");
if (options->verbosityLevel != BmcVerbosityNone_c) {
endTime = util_cpu_ctime();
fprintf(vis_stdout, "-- bmc time = %10g\n",
(double)(endTime - startTime) / 1000.0);
}
return;
} else if (property == bAig_Zero){
(void) fprintf(vis_stdout,"# BMC: The property is always TRUE\n");
formulaStatus = BmcPropertyPassed_c;
(void) fprintf(vis_stdout,"# BMC: formula passed\n");
if (options->verbosityLevel != BmcVerbosityNone_c) {
endTime = util_cpu_ctime();
fprintf(vis_stdout, "-- bmc time = %10g\n",
(double)(endTime - startTime) / 1000.0);
}
return;
}
if (options->verbosityLevel != BmcVerbosityNone_c){
(void)fprintf(vis_stdout, "Apply BMC on counterexample of length >= %d and <= %d (+%d) \n",
options->minK, options->maxK, options->step);
}
/*
nodeToMvfAigTable Maps each node to its Multi-function AIG graph
*/
nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
assert(nodeToMvfAigTable != NIL(st_table));
outClause = NIL(array_t);
bound = options->minK;
BmcGetCoiForLtlFormula(network, ltlFormula, CoiTable);
while( (result == NIL(array_t)) && (bound <= options->maxK)){
if (options->verbosityLevel == BmcVerbosityMax_c) {
(void) fprintf(vis_stdout,
"\nBMC: Generate counterexample of length %d\n", bound);
}
cnfClauses = BmcCnfClausesAlloc();
cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
if (cnfFile == NIL(FILE)) {
(void)fprintf(vis_stderr,
"** bmc error: Cannot create CNF output file %s\n",
options->satInFile);
bmcError = TRUE;
break;
}
/*
Generate clauses for an initialized path of length "bound".
*/
BmcCnfGenerateClausesForPath(network, 0, bound, BMC_INITIAL_STATES,
cnfClauses, nodeToMvfAigTable, CoiTable);
/*
Generate CNF for the property. Property fails at all states
*/
for(k=0; k <= bound; k++){
array_insert(int, unitClause, 0,
BmcGenerateCnfFormulaForAigFunction(manager, property,
k, cnfClauses));
BmcCnfInsertClause(cnfClauses, unitClause);
}
/* Generate CNF for a loop-back (loop from the last state to any
state) path.
(Sk -> S0) + (Sk -> S1) + ..... + (Sk-> Sk-1) + (Sk-> Sk)
Each transition consisits of one or more latches. We
AND the transiton relation of these latches. For multi-valued
latches, we OR the equivalence of each value of the latch. To
do the AND we use the CNF equivalent of the AND. a = b*c => (b
+ !a) * (c + !a)
*/
outClause = array_alloc(int, bound);
for (k=0; k <= bound; k++){
/*
Create new var for the output of the AND node.
*/
outIndex = cnfClauses->cnfGlobalIndex++;
BmcCnfGenerateClausesFromStateToState(network, bound, k, cnfClauses,
nodeToMvfAigTable, CoiTable, outIndex);
array_insert(int, outClause, k, outIndex);
} /* for k state loop */
BmcCnfInsertClause(cnfClauses, outClause);
BmcWriteClauses(manager, cnfFile, cnfClauses, options);
(void) fclose(cnfFile);
result = BmcCheckSAT(options);
if (options->satSolverError){
break;
}
if(result != NIL(array_t)){
formulaStatus = BmcPropertyFailed_c;
break;
}
BmcCnfClausesFree(cnfClauses);
array_free(outClause);
if((result == NIL(array_t)) &&
(options->inductiveStep !=0) &&
(bound % options->inductiveStep == 0)
)
{
int savedVerbosityLevel = options->verbosityLevel;
long startTime = util_cpu_ctime();
array_t *result = NIL(array_t);
if (options->verbosityLevel == BmcVerbosityMax_c) {
(void) fprintf(vis_stdout,
"\nBMC: Check if the property passes\n");
}
cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
if (cnfFile == NIL(FILE)) {
(void)fprintf(vis_stderr,
"** bmc error: Cannot create CNF output file %s\n",
options->satInFile);
bmcError = TRUE;
break;
}
cnfClauses = BmcCnfClausesAlloc();
/*
CNF for an initialized simple path.
*/
BmcCnfGenerateClausesForLoopFreePath(network, 0, bound, BMC_INITIAL_STATES,
cnfClauses, nodeToMvfAigTable, CoiTable);
/*
Generate CNF for the property. Property fails at all states
*/
for(k=0; k <= bound; k++){
array_insert(int, unitClause, 0,
BmcGenerateCnfFormulaForAigFunction(manager, property,
k, cnfClauses));
BmcCnfInsertClause(cnfClauses, unitClause);
}
BmcWriteClauses(manager, cnfFile, cnfClauses, options);
BmcCnfClausesFree(cnfClauses);
(void) fclose(cnfFile);
/*
Do not print any detail information when checking the clauses
*/
options->verbosityLevel = BmcVerbosityNone_c;
result = BmcCheckSAT(options);
options->verbosityLevel = (Bmc_VerbosityLevel) savedVerbosityLevel;
if (options->satSolverError){
break;
}
if (options->verbosityLevel != BmcVerbosityNone_c){
endTime = util_cpu_ctime();
fprintf(vis_stdout, "-- checking time = %10g\n",
(double)(endTime - startTime) / 1000.0);
}
if (result == NIL(array_t)){ /* UNSAT */
formulaStatus = BmcPropertyPassed_c;
break; /* formula is satisfiable */
}
array_free(result);
} /* Check induction */
/* free all used memories
BmcCnfClausesFree(cnfClauses); */
bound += options->step;
} /* while result and bound */
if (bmcError == FALSE){
if(!options->satSolverError){
if(formulaStatus == BmcPropertyFailed_c) {
(void) fprintf(vis_stdout, "# BMC: formula failed\n");
if(options->verbosityLevel != BmcVerbosityNone_c){
(void) fprintf(vis_stdout,
"# BMC: Found a counterexample of length = %d \n", bound);
}
if (options->dbgLevel == 1) {
BmcPrintCounterExample(network, nodeToMvfAigTable, cnfClauses,
result, bound, CoiTable, options, outClause);
}
array_free(result);
BmcCnfClausesFree(cnfClauses);
array_free(outClause);
} else if(formulaStatus == BmcPropertyPassed_c) {
(void) fprintf(vis_stdout, "# BMC: formula Passed\n");
} else if(formulaStatus == BmcPropertyUndecided_c) {
(void) fprintf(vis_stdout,"# BMC: formula undecided\n");
if (options->verbosityLevel != BmcVerbosityNone_c){
(void) fprintf(vis_stdout,
"# BMC: no counterexample found of length up to %d \n",
options->maxK);
}
}
} else {
(void) fprintf(vis_stdout,"# BMC: Error in calling SAT solver\n");
}
}
if (options->verbosityLevel != BmcVerbosityNone_c) {
endTime = util_cpu_ctime();
fprintf(vis_stdout, "-- bmc time = %10g\n",
(double)(endTime - startTime) / 1000.0);
}
if(unitClause != NIL(array_t)) {
array_free(unitClause);
}
fflush(vis_stdout);
return;
} /* BmcLtlVerifyFp() */
Here is the call graph for this function:
Here is the caller graph for this function:
| void BmcLtlVerifyGeneralLtl | ( | Ntk_Network_t * | network, |
| Ctlsp_Formula_t * | ltlFormula, | ||
| st_table * | CoiTable, | ||
| array_t * | constraintArray, | ||
| BmcOption_t * | options | ||
| ) |
Function********************************************************************
Synopsis [Use BMC to verify a general LTL formulae]
Description [Implements the Bounded Model Checking technique as in the paper "Symbolic Model Checking without BDDs". We also have implemented some of the improvements in the BMC encoding described in the paper "Improving the Encoding of LTL Model Checking into SAT" ]
SideEffects []
SeeAlso []
Definition at line 1680 of file bmcBmc.c.
{
mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
st_table *nodeToMvfAigTable = NIL(st_table); /* node to mvfAig */
BmcCnfClauses_t *cnfClauses = NIL(BmcCnfClauses_t);
FILE *cnfFile;
array_t *orClause = NIL(array_t);
array_t *loopClause, *tmpclause;
int l, loopIndex, andIndex, loop;
int noLoopIndex;
array_t *result = NIL(array_t);
array_t *fairnessArray = NIL(array_t);
int leftValue = 0;
int rightValue = 0;
long startTime, endTime;
int k;
int minK = options->minK;
int maxK = options->maxK;
boolean boundedFormula;
int depth;
/* Store the index of loop from k to all sate from 0 to k */
array_t *ltlConstraintArray; /* constraints converted to LTL */
int f;
boolean fairness = (constraintArray != NIL(array_t));
BmcCheckForTermination_t *terminationStatus = 0;
Bmc_PropertyStatus formulaStatus;
int bmcStatus=0; /* Holds the status of running BMC
= -1 if there is an error */
/* ************** */
/* Initialization */
/* ************** */
startTime = util_cpu_ctime();
/*
nodeToMvfAigTable maps each node to its multi-function And/Inv graph
*/
nodeToMvfAigTable =
(st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
assert(nodeToMvfAigTable != NIL(st_table));
loopClause = NIL(array_t);
noLoopIndex = 0;
ltlConstraintArray = NIL(array_t);
if(fairness){
Ctlsp_Formula_t *formula;
int i;
/*
All formulae in constraintArray are propositional, propositional
constraint.
*/
ltlConstraintArray = array_alloc(Ctlsp_Formula_t *, 0);
arrayForEachItem(Ctlsp_Formula_t *, constraintArray, i, formula) {
/*
To help making propositional constraint easy to encode.
*/
formula = Ctlsp_FormulaCreate(Ctlsp_F_c, formula, NIL(Ctlsp_Formula_t));
array_insert(Ctlsp_Formula_t *, ltlConstraintArray, i, formula);
BmcGetCoiForLtlFormula(network, formula, CoiTable);
}
}
/*
For bounded formulae use a tighter upper bound if possible.
*/
boundedFormula = Ctlsp_LtlFormulaTestIsBounded(ltlFormula, &depth);
if (boundedFormula && depth < maxK && depth >= minK) {
maxK = depth;
} else {
if(options->inductiveStep !=0){
/*
Use the termination criteria to prove the property passes.
*/
terminationStatus = BmcAutTerminationAlloc(network,
Ctlsp_LtllFormulaNegate(ltlFormula),
constraintArray);
assert(terminationStatus);
}
}
if (options->verbosityLevel != BmcVerbosityNone_c){
(void) fprintf(vis_stdout, "General LTL BMC\n");
if (boundedFormula){
(void) fprintf(vis_stdout, "Bounded formula of depth %d\n", depth);
}
(void) fprintf(vis_stdout, "Apply BMC on counterexample of length >= %d and <= %d (+%d) \n",
minK, maxK, options->step);
}
k= minK;
formulaStatus = BmcPropertyUndecided_c;
while( (result == NIL(array_t)) && (k <= maxK)){
if (options->verbosityLevel == BmcVerbosityMax_c) {
(void) fprintf(vis_stdout, "\nGenerate counterexample of length %d\n", k);
}
cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
if (cnfFile == NIL(FILE)) {
(void)fprintf(vis_stderr,
"** bmc error: Cannot create CNF output file %s\n",
options->satInFile);
bmcStatus = -1;
break;
}
/*
Create a clause database
*/
cnfClauses = BmcCnfClausesAlloc();
/*
Gnerate clauses for an initialized path of length k
*/
BmcCnfGenerateClausesForPath(network, 0, k, BMC_INITIAL_STATES,
cnfClauses, nodeToMvfAigTable, CoiTable);
if(!fairness){ /* No fairness constraint */
noLoopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, -1, cnfClauses);
leftValue = checkIndex(noLoopIndex, cnfClauses);
} else {
leftValue = 0; /* the path must have a loop*/
}
if (leftValue != 1) {
orClause = array_alloc(int, 0);
/*
No need to check for !Lk in the basic encoding
*/
if (leftValue == -1){
array_insert_last(int, orClause, noLoopIndex);
}
loopClause = array_alloc(int, k+1);
for(l=0; l<=k; l++){
loopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, l, cnfClauses);
rightValue = checkIndex(loopIndex, cnfClauses);
if (rightValue == 0){
break;
}
if(fairness){
Ctlsp_Formula_t *formula;
int i;
fairnessArray = array_alloc(int, 0);
arrayForEachItem(Ctlsp_Formula_t *, ltlConstraintArray, i, formula) {
array_insert_last(int, fairnessArray,
BmcGenerateCnfForLtl(network, formula, l, k, -1, cnfClauses));
}
}
if (rightValue !=0){
loop = cnfClauses->cnfGlobalIndex++;
BmcCnfGenerateClausesFromStateToState(network, k, l, cnfClauses,
nodeToMvfAigTable, CoiTable, loop);
array_insert(int, loopClause, l, loop);
if(rightValue == -1){
andIndex = cnfClauses->cnfGlobalIndex++;
tmpclause = array_alloc(int, 2);
array_insert(int, tmpclause, 0, loop);
array_insert(int, tmpclause, 1, -andIndex);
BmcCnfInsertClause(cnfClauses, tmpclause);
array_insert(int, tmpclause, 0, loopIndex);
array_insert(int, tmpclause, 1, -andIndex);
BmcCnfInsertClause(cnfClauses, tmpclause);
if(fairness){
for(f=0; f < array_n(fairnessArray); f++){
array_insert(int, tmpclause, 0, array_fetch(int, fairnessArray, f));
array_insert(int, tmpclause, 1, -andIndex);
BmcCnfInsertClause(cnfClauses, tmpclause);
}
}
array_free(tmpclause);
array_insert_last(int, orClause, andIndex);
} else {
array_insert_last(int, orClause, loop);
}
}
if(fairness){
array_free(fairnessArray);
}
} /* for l loop */
}
if((leftValue == 1) || (rightValue == 1)){
assert(k==1);
if (options->verbosityLevel != BmcVerbosityNone_c){
formulaStatus = BmcPropertyFailed_c;
(void) fprintf(vis_stdout,"# BMC: Empty counterexample because the property is always FALSE\n");
}
break;
} else if((leftValue == 0) && (rightValue == 0)){
if (options->verbosityLevel != BmcVerbosityNone_c){
(void) fprintf(vis_stdout,"# BMC: the formula is trivially true");
(void) fprintf(vis_stdout," for counterexamples of length %d\n", k);
}
} else {
/*
BmcCnfInsertClause(cnfClauses, loopClause);
*/
BmcCnfInsertClause(cnfClauses, orClause);
/*
array_free(loopClause);
*/
array_free(orClause);
BmcWriteClauses(manager, cnfFile, cnfClauses, options);
(void) fclose(cnfFile);
result = BmcCheckSAT(options);
if(options->satSolverError){
break;
}
if(result != NIL(array_t)) {
/*
formula failed\n"
*/
formulaStatus = BmcPropertyFailed_c;
break;
}
array_free(loopClause);
}
/* free all used memories */
BmcCnfClausesFree(cnfClauses);
cnfClauses = NIL(BmcCnfClauses_t);
/*
Use the termination check if the the LTL formula is not bounded
*/
if(terminationStatus && (formulaStatus == BmcPropertyUndecided_c) && (bmcStatus != 1)){
if((options->inductiveStep !=0) &&
(k % options->inductiveStep == 0)
)
{
/*
Check for termination for the current value of k.
*/
terminationStatus->k = k;
bmcStatus = BmcAutLtlCheckForTermination(network,
constraintArray, terminationStatus,
nodeToMvfAigTable, CoiTable, options);
if(bmcStatus == 1){
maxK = terminationStatus->k;
}
if(bmcStatus == 3){
formulaStatus = BmcPropertyPassed_c;
break;
}
if(bmcStatus == -1){
break;
}
}
} /* terminationStatus */
k += options->step;
} /* while result and k*/
/*
If no error.
*/
if(bmcStatus != -1){
/*
if(result == NIL(array_t)){
*/
if(formulaStatus == BmcPropertyUndecided_c){
if(bmcStatus == 1){
(void) fprintf(vis_stdout,
"# BMC: no counterexample found of length up to %d \n", maxK);
(void) fprintf(vis_stdout, "# BMC: By termination criterion (m+n-1)\n");
formulaStatus = BmcPropertyPassed_c;
}
if (boundedFormula && depth <= options->maxK){
(void) fprintf(vis_stdout,
"# BMC: no counterexample found of length up to %d \n", depth);
formulaStatus = BmcPropertyPassed_c;
}
}
if(options->satSolverError){
(void) fprintf(vis_stdout,"# BMC: Error in calling SAT solver\n");
} else {
if(formulaStatus == BmcPropertyFailed_c) {
(void) fprintf(vis_stdout, "# BMC: formula failed\n");
if(options->verbosityLevel != BmcVerbosityNone_c){
(void) fprintf(vis_stdout,
"# BMC: Found a counterexample of length = %d \n", k);
}
if ((options->dbgLevel == 1) && (result != NIL(array_t))) {
BmcPrintCounterExample(network, nodeToMvfAigTable, cnfClauses,
result, k, CoiTable, options, loopClause);
}
/*BmcCnfClausesFree(cnfClauses);*/
array_free(loopClause);
} else if(formulaStatus == BmcPropertyPassed_c) {
(void) fprintf(vis_stdout, "# BMC: formula Passed\n");
(void) fprintf(vis_stdout, "# Termination depth = %d\n", maxK);
} else if(formulaStatus == BmcPropertyUndecided_c) {
(void) fprintf(vis_stdout,"# BMC: formula undecided\n");
if (options->verbosityLevel != BmcVerbosityNone_c){
(void) fprintf(vis_stdout,
"# BMC: no counterexample found of length up to %d \n",
maxK);
}
}
}
}
if (options->verbosityLevel != BmcVerbosityNone_c) {
endTime = util_cpu_ctime();
fprintf(vis_stdout, "-- bmc time = %10g\n",
(double)(endTime - startTime) / 1000.0);
}
/*
free all used memories
*/
if(terminationStatus){
BmcAutTerminationFree(terminationStatus);
}
if(result != NIL(array_t)){
array_free(result);
}
if(cnfClauses != NIL(BmcCnfClauses_t)){
BmcCnfClausesFree(cnfClauses);
}
if(fairness){
/*Ctlsp_FormulaArrayFree(ltlConstraintArray);*/
}
fflush(vis_stdout);
return;
} /* BmcLtlVerifyGeneralLtl() */
Here is the call graph for this function:
Here is the caller graph for this function:
| void BmcLtlVerifyGp | ( | Ntk_Network_t * | network, |
| Ctlsp_Formula_t * | ltlFormula, | ||
| st_table * | CoiTable, | ||
| BmcOption_t * | options | ||
| ) |
Function********************************************************************
Synopsis [Apply Bounded Model Checking (BMC) on an LTL formula of the form G(p), where p is a propositional formula.]
Description [Given a model M, an LTL formula f = Gp, and a bound k, we first find a counterexample of length k to a state that violates p. If -r switch of the BMC command is specified, we apply the induction proof to check if the property f passes. The property f passes if there is no simple path in M that leads to a state that violates p, or no simple path in M starting at an initial state.
Note: Before calling this function, the LTL formula must be negated.
]
SideEffects []
SeeAlso []
Definition at line 347 of file bmcBmc.c.
{
mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
st_table *nodeToMvfAigTable = NIL(st_table); /* maps each node to its mvfAig */
BmcCnfClauses_t *cnfClauses = NIL(BmcCnfClauses_t);
BmcCnfStates_t *state;
FILE *cnfFile;
array_t *Pclause = array_alloc(int, 0);
int k, bound, initK, propK;
array_t *result = NIL(array_t);
long startTime, endTime;
bAigEdge_t property;
int minK = options->minK;
int maxK = options->maxK;
int i, initState = BMC_INITIAL_STATES;
array_t *unitClause;
int bmcError = FALSE;
Bmc_PropertyStatus formulaStatus;
assert(Ctlsp_LtlFormulaIsFp(ltlFormula));
startTime = util_cpu_ctime();
if (options->verbosityLevel != BmcVerbosityNone_c){
(void)fprintf(vis_stdout, "LTL formula is of type G(p)\n");
}
property = BmcCreateMaigOfPropFormula(network, manager, ltlFormula->right);
if (property == mAig_NULL){
return;
}
if (property == bAig_One){
(void) fprintf(vis_stdout,"# BMC: Empty counterexample because the property is always FALSE\n");
(void) fprintf(vis_stdout,"# BMC: formula failed\n");
if (options->verbosityLevel != BmcVerbosityNone_c){
fprintf(vis_stdout, "-- bmc time = %10g\n",
(double)(util_cpu_ctime() - startTime) / 1000.0);
}
return;
} else if (property == bAig_Zero){
(void) fprintf(vis_stdout,"# BMC: The property is always TRUE\n");
(void) fprintf(vis_stdout,"# BMC: formula passed\n");
if (options->verbosityLevel != BmcVerbosityNone_c){
fprintf(vis_stdout, "-- bmc time = %10g\n",
(double)(util_cpu_ctime() - startTime) / 1000.0);
}
return;
}
#if 0
if (options->verbosityLevel == BmcVerbosityMax_c){
(void) fprintf(vis_stdout, "\nBMC: Check if the property is an inductive invariant\n");
}
checkInductiveInvariant = BmcLtlCheckInductiveInvariant(network, property, options, CoiTable);
if(checkInductiveInvariant == -1){
return;
}
if (checkInductiveInvariant == 1){
(void) fprintf(vis_stdout,"# BMC: The property is an inductive invariant\n");
(void) fprintf(vis_stdout,"# BMC: formula passed\n");
if (options->verbosityLevel != BmcVerbosityNone_c){
fprintf(vis_stdout, "-- bmc time = %10g\n",
(double)(util_cpu_ctime() - startTime) / 1000.0);
}
return;
}
#endif
if (options->verbosityLevel != BmcVerbosityNone_c){
(void)fprintf(vis_stdout, "Apply BMC on counterexample of length >= %d and <= %d (+%d)\n",
minK, maxK, options->step);
}
initK = 0;
propK = 0;
formulaStatus = BmcPropertyUndecided_c;
/* nodeToMvfAigTable Maps each node to its Multi-function And/Inv graph */
nodeToMvfAigTable =
(st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
assert(nodeToMvfAigTable != NIL(st_table));
/*
Create clauses database
*/
cnfClauses = BmcCnfClausesAlloc();
/*
init = BmcCreateMaigOfInitialStates(network, nodeToMvfAigTable, CoiTable);
*/
for(bound = minK; bound <= maxK; bound += options->step){
if (options->verbosityLevel == BmcVerbosityMax_c) {
(void) fprintf(vis_stdout,
"\nBMC: Generate counterexample of length %d\n",
bound);
}
cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
if (cnfFile == NIL(FILE)) {
(void) fprintf(vis_stderr,
"** bmc error: Cannot create CNF output file %s\n",
options->satInFile);
bmcError = TRUE;
break;
}
BmcCnfGenerateClausesForPath(network, initK, bound, initState, cnfClauses, nodeToMvfAigTable, CoiTable);
initState = BMC_NO_INITIAL_STATES;
/* Generate CNF for the property */
Pclause = array_alloc(int, 0);
/*
state = BmcCnfClausesFreeze(cnfClauses);
*/
for(k=propK; k <= bound; k++){
array_insert_last(
int, Pclause, BmcGenerateCnfFormulaForAigFunction(manager, property,
k, cnfClauses));
}
state = BmcCnfClausesFreeze(cnfClauses);
BmcCnfInsertClause(cnfClauses, Pclause);
BmcWriteClauses(manager, cnfFile, cnfClauses, options);
(void) fclose(cnfFile);
BmcCnfClausesRestore(cnfClauses, state);
result = BmcCheckSAT(options);
if (options->satSolverError){
array_free(Pclause);
break;
}
if (result != NIL(array_t)){
bound++;
array_free(Pclause);
/*
formula failed\n"
*/
formulaStatus = BmcPropertyFailed_c;
break;
}
unitClause = array_alloc(int, 1);
for(i=0; i<array_n(Pclause); i++){
array_insert(int, unitClause, 0, -array_fetch(int, Pclause, i));
BmcCnfInsertClause(cnfClauses, unitClause);
}
array_free(unitClause);
array_free(Pclause);
FREE(state);
initK = bound;
propK = bound+1;
/*
Prove if the property passes using the induction proof of SSS0.
*/
if((result == NIL(array_t)) &&
(options->inductiveStep !=0) &&
(bound % options->inductiveStep == 0)){
BmcCnfClauses_t *cnfClauses;
array_t *result = NIL(array_t);
array_t *unitClause = array_alloc(int, 1);
int savedVerbosityLevel = options->verbosityLevel;
long startTime = util_cpu_ctime();
if (options->verbosityLevel == BmcVerbosityMax_c) {
(void) fprintf(vis_stdout, "\nBMC: Check for induction\n");
}
options->verbosityLevel = BmcVerbosityNone_c;
if(options->earlyTermination){
/*
Early termination condition
Check if there is no simple path of length 'bound' starts from
initial states
*/
cnfClauses = BmcCnfClausesAlloc();
cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
if (cnfFile == NIL(FILE)) {
(void)fprintf(vis_stderr,
"** bmc error: Cannot create CNF output file %s\n",
options->satInFile);
bmcError = TRUE;
break;
}
/*
Generate an initialized simple path path of length bound.
*/
BmcCnfGenerateClausesForLoopFreePath(network, 0, bound, BMC_INITIAL_STATES,
cnfClauses, nodeToMvfAigTable, CoiTable);
BmcWriteClauses(manager, cnfFile, cnfClauses, options);
(void) fclose(cnfFile);
BmcCnfClausesFree(cnfClauses);
result = BmcCheckSAT(options);
if(options->satSolverError){
break;
}
if(result == NIL(array_t)){
if (savedVerbosityLevel == BmcVerbosityMax_c) {
(void) fprintf(vis_stdout,
"# BMC: No simple path starting at an initial state\n");
}
formulaStatus = BmcPropertyPassed_c;
} else {
array_free(result);
}
} /* Early termination */
if(formulaStatus != BmcPropertyPassed_c){
cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
if (cnfFile == NIL(FILE)) {
(void)fprintf(vis_stderr,
"** bmc error: Cannot create CNF output file %s\n",
options->satInFile);
bmcError = TRUE;
break;
}
cnfClauses = BmcCnfClausesAlloc();
/*
Generate a simple path of length k+1
*/
BmcCnfGenerateClausesForLoopFreePath(network, 0, bound+1, BMC_NO_INITIAL_STATES,
cnfClauses, nodeToMvfAigTable, CoiTable);
/*
All the states to bound satisfy the property.
*/
unitClause = array_alloc(int, 1);
for(k=0; k <= bound; k++){
array_insert(
int, unitClause, 0, -BmcGenerateCnfFormulaForAigFunction(manager, property,
k, cnfClauses));
BmcCnfInsertClause(cnfClauses, unitClause);
}
/*
The property fails at bound +1
*/
array_insert(int, unitClause, 0,
BmcGenerateCnfFormulaForAigFunction(manager, property,
bound+1, cnfClauses));
BmcCnfInsertClause(cnfClauses, unitClause);
array_free(unitClause);
BmcWriteClauses(manager, cnfFile, cnfClauses, options);
BmcCnfClausesFree(cnfClauses);
(void) fclose(cnfFile);
result = BmcCheckSAT(options);
if (options->satSolverError){
break;
}
if(result == NIL(array_t)) {
if (savedVerbosityLevel == BmcVerbosityMax_c) {
(void) fprintf(vis_stdout,
"# BMC: No simple path leading to a bad state\n");
}
formulaStatus = BmcPropertyPassed_c;
}
}
options->verbosityLevel = (Bmc_VerbosityLevel) savedVerbosityLevel;
if (options->verbosityLevel != BmcVerbosityNone_c){
endTime = util_cpu_ctime();
fprintf(vis_stdout, "-- check for induction time = %10g\n",
(double)(endTime - startTime) / 1000.0);
}
} /* Check induction */
if(formulaStatus != BmcPropertyUndecided_c){
break;
}
} /* for bound loop */
if( bmcError == FALSE){
if (options->satSolverError){
(void) fprintf(vis_stdout,"# BMC: Error in calling SAT solver\n");
} else {
if(formulaStatus == BmcPropertyUndecided_c){
if (options->verbosityLevel != BmcVerbosityNone_c){
(void) fprintf(vis_stdout,
"# BMC: no counterexample found of length up to %d \n",
options->maxK);
}
}
if(formulaStatus == BmcPropertyFailed_c) {
(void) fprintf(vis_stdout, "# BMC: formula failed\n");
if(options->verbosityLevel != BmcVerbosityNone_c){
(void) fprintf(vis_stdout,
"# BMC: Found a counterexample of length = %d \n", bound-1);
}
if (options->dbgLevel == 1) {
BmcPrintCounterExample(network, nodeToMvfAigTable, cnfClauses,
result, bound-1, CoiTable, options, NIL(array_t));
}
} else if(formulaStatus == BmcPropertyPassed_c) {
(void) fprintf(vis_stdout, "# BMC: formula Passed\n");
} else if(formulaStatus == BmcPropertyUndecided_c) {
(void) fprintf(vis_stdout,"# BMC: formula undecided\n");
}
}
}
/* free all used memories */
if(cnfClauses != NIL(BmcCnfClauses_t)){
BmcCnfClausesFree(cnfClauses);
}
if(result != NIL(array_t)) {
array_free(result);
}
/*
array_free(Pclause);
*/
if (options->verbosityLevel != BmcVerbosityNone_c){
endTime = util_cpu_ctime();
fprintf(vis_stdout, "-- bmc time = %10g\n",
(double)(endTime - startTime) / 1000.0);
}
fflush(vis_stdout);
return;
} /* BmcLtlVerifyGp() */
Here is the call graph for this function:
Here is the caller graph for this function:
| void BmcLtlVerifyProp | ( | Ntk_Network_t * | network, |
| Ctlsp_Formula_t * | ltlFormula, | ||
| st_table * | CoiTable, | ||
| BmcOption_t * | options | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Apply Bounded Model Checking (BMC) on a propositional formula.]
Description [If the property dos not hold in any initial state, the property holds.
Note: Before calling this function, the LTL formula must be negated.
]
SideEffects []
SeeAlso []
Definition at line 74 of file bmcBmc.c.
{
mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
st_table *nodeToMvfAigTable = NIL(st_table); /* maps each node to its mvfAig */
BmcCnfClauses_t *cnfClauses = NIL(BmcCnfClauses_t);
FILE *cnfFile;
array_t *result = NIL(array_t);
long startTime, endTime;
bAigEdge_t property;
array_t *unitClause;
assert(Ctlsp_isPropositionalFormula(ltlFormula));
startTime = util_cpu_ctime();
if (options->verbosityLevel != BmcVerbosityNone_c){
(void) fprintf(vis_stdout, "LTL formula is propositional\n");
}
property = BmcCreateMaigOfPropFormula(network, manager, ltlFormula);
if (property == mAig_NULL){
return;
}
if (property == bAig_One){
(void) fprintf(vis_stdout,"# BMC: Empty counterexample because the property is always FALSE\n");
(void) fprintf(vis_stdout,"# BMC: formula failed\n");
if (options->verbosityLevel != BmcVerbosityNone_c){
fprintf(vis_stdout, "-- bmc time = %10g\n",
(double)(util_cpu_ctime() - startTime) / 1000.0);
}
return;
} else if (property == bAig_Zero){
(void) fprintf(vis_stdout,"# BMC: The property is always TRUE\n");
(void) fprintf(vis_stdout,"# BMC: formula passed\n");
if (options->verbosityLevel != BmcVerbosityNone_c){
fprintf(vis_stdout, "-- bmc time = %10g\n",
(double)(util_cpu_ctime() - startTime) / 1000.0);
}
return;
}
cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
if (cnfFile == NIL(FILE)) {
(void) fprintf(vis_stderr,
"** bmc error: Cannot create CNF output file %s\n",
options->satInFile);
return;
}
/* nodeToMvfAigTable Maps each node to its Multi-function And/Inv graph */
nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(network,
MVFAIG_NETWORK_APPL_KEY);
assert(nodeToMvfAigTable != NIL(st_table));
/*
Create clauses database
*/
cnfClauses = BmcCnfClausesAlloc();
unitClause = array_alloc(int, 1);
/*
Create an initialized path of length 0
*/
BmcCnfGenerateClausesForPath(network, 0, 0, BMC_INITIAL_STATES, cnfClauses, nodeToMvfAigTable, CoiTable);
/* Generate CNF for the property */
array_insert(int, unitClause, 0,
BmcGenerateCnfFormulaForAigFunction(manager, property, 0, cnfClauses));
BmcCnfInsertClause(cnfClauses, unitClause);
BmcWriteClauses(manager, cnfFile, cnfClauses, options);
(void) fclose(cnfFile);
result = BmcCheckSAT(options);
if (options->satSolverError){
(void) fprintf(vis_stdout,"# BMC: Error in calling SAT solver\n");
} else {
if (result != NIL(array_t)){
(void) fprintf(vis_stdout, "# BMC: formula failed\n");
if(options->verbosityLevel != BmcVerbosityNone_c){
(void) fprintf(vis_stdout,
"# BMC: Found a counterexample of length = 0 \n");
}
if (options->dbgLevel == 1) {
BmcPrintCounterExample(network, nodeToMvfAigTable, cnfClauses,
result, 0, CoiTable, options, NIL(array_t));
}
array_free(result);
} else {
if(options->verbosityLevel != BmcVerbosityNone_c){
fprintf(vis_stdout,"# BMC: no counterexample found of length up to 0\n");
}
(void) fprintf(vis_stdout, "# BMC: formula Passed\n");
}
}
array_free(unitClause);
BmcCnfClausesFree(cnfClauses);
if (options->verbosityLevel != BmcVerbosityNone_c){
endTime = util_cpu_ctime();
fprintf(vis_stdout, "-- bmc time = %10g\n",
(double)(endTime - startTime) / 1000.0);
}
fflush(vis_stdout);
return;
} /* BmcLtlVerifyProp */
Here is the call graph for this function:
Here is the caller graph for this function:
| void BmcLtlVerifyUnitDepth | ( | Ntk_Network_t * | network, |
| Ctlsp_Formula_t * | ltlFormula, | ||
| st_table * | CoiTable, | ||
| BmcOption_t * | options | ||
| ) |
Function********************************************************************
Synopsis [Apply Bounded Model Checking (BMC) on an LTL formula of depth = 1]
Description [The depth of the LTL formula f is the maximum level of nesting of temporal operators in f. If the depth of the LTL formula = 1, the translation of the formula in case of loop is independent of the loop.
Note: Before calling this function, the LTL formula must be negated.
]
SideEffects []
SeeAlso []
Definition at line 1400 of file bmcBmc.c.
{
mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
st_table *nodeToMvfAigTable = NIL(st_table); /* node to mvfAig */
BmcCnfClauses_t *cnfClauses = NIL(BmcCnfClauses_t);
FILE *cnfFile;
array_t *orClause =NIL(array_t);
array_t *loopClause, *tmpclause;
int l, loopIndex, andIndex, loop;
int noLoopIndex;
array_t *result = NIL(array_t);
int leftValue = 0;
int rightValue = 0;
long startTime, endTime;
int k;
int minK = options->minK;
int maxK = options->maxK;
/* Store the index of a loop from k to all sate from 0 to k */
Bmc_PropertyStatus formulaStatus;
BmcCheckForTermination_t *terminationStatus = 0;
int bmcStatus=0; /* Holds the status of running BMC
= -1 if there is an error */
assert(Ctlsp_LtlFormulaDepth(ltlFormula) == 1);
/* ************** */
/* Initialization */
/* ************** */
startTime = util_cpu_ctime();
/*
nodeToMvfAigTable maps each node to its multi-function AIG graph
*/
nodeToMvfAigTable =
(st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
assert(nodeToMvfAigTable != NIL(st_table));
loopClause = NIL(array_t);
if (options->verbosityLevel != BmcVerbosityNone_c){
(void) fprintf(vis_stdout, "Unit depth LTL formula\n");
(void) fprintf(vis_stdout, "Apply BMC on counterexample of length >= %d and <= %d (+%d) \n",
minK, maxK, options->step);
}
if(options->inductiveStep !=0){
/*
Use the termination criteria to prove the property passes.
*/
terminationStatus = BmcAutTerminationAlloc(network,
Ctlsp_LtllFormulaNegate(ltlFormula),
NIL(array_t));
assert(terminationStatus);
}
k = minK;
formulaStatus = BmcPropertyUndecided_c;
while( (result == NIL(array_t)) && (k <= maxK)){
if (options->verbosityLevel == BmcVerbosityMax_c) {
(void) fprintf(vis_stdout, "\nGenerate counterexample of length %d\n", k);
}
/*
Create clause database
*/
cnfClauses = BmcCnfClausesAlloc();
cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
if (cnfFile == NIL(FILE)) {
(void)fprintf(vis_stderr,
"** bmc error: Cannot create CNF output file %s\n",
options->satInFile);
bmcStatus = -1;
break;
}
/*
Generate clauses represent an initialized path of length k
*/
BmcCnfGenerateClausesForPath(network, 0, k, BMC_INITIAL_STATES,
cnfClauses, nodeToMvfAigTable, CoiTable);
/*
Generate clauses represent paths which satisfy the LTL formula if
there is no loop.
*/
noLoopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, -1, cnfClauses);
leftValue = checkIndex(noLoopIndex, cnfClauses);
if (leftValue != 1) { /* no loop part of the basic encoding is not TRUE */
orClause = array_alloc(int, 0);
/*
No need to check for !Lk in the basic encoding
*/
if (leftValue == -1){ /* no loop part of the basic encoding is not FALSE */
array_insert_last(int, orClause, noLoopIndex);
}
/*
Generate clauses represent paths which satisfy the LTL formula if
there is a loop.
*/
loopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, 0, cnfClauses);
rightValue = checkIndex(loopIndex, cnfClauses);
if (rightValue == 0){ /* loop part of the basic encoding is FALSE */
break;
}
/*
rightValue can be 1 or -1
leftValue can be 0 or -1
*/
if (noLoopIndex == loopIndex){ /* do not check for the existence of a loop*/
break;
}
/*
Clauses for loop-back path.
*/
loopClause = array_alloc(int, k+2);
for(l=0; l<=k; l++){
loop = cnfClauses->cnfGlobalIndex++;
BmcCnfGenerateClausesFromStateToState(network, k, l, cnfClauses,
nodeToMvfAigTable, CoiTable, loop);
array_insert(int, loopClause, l, loop);
} /* for l loop */
loop = cnfClauses->cnfGlobalIndex++;
array_insert(int, loopClause, k+1, -loop);
BmcCnfInsertClause(cnfClauses, loopClause);
if(rightValue == -1){
andIndex = cnfClauses->cnfGlobalIndex++;
tmpclause = array_alloc(int, 2);
array_insert(int, tmpclause, 0, loop);
array_insert(int, tmpclause, 1, -andIndex);
BmcCnfInsertClause(cnfClauses, tmpclause);
array_insert(int, tmpclause, 0, loopIndex);
array_insert(int, tmpclause, 1, -andIndex);
BmcCnfInsertClause(cnfClauses, tmpclause);
array_free(tmpclause);
array_insert_last(int, orClause, andIndex);
} else {
array_insert_last(int, orClause, loop);
}
}
/* if((leftValue == 1) || (rightValue == 1)){ */
if(leftValue == 1){
assert(k==1);
/*
formula failed
*/
formulaStatus = BmcPropertyFailed_c;
if (options->verbosityLevel != BmcVerbosityNone_c){
(void) fprintf(vis_stdout,"# BMC: Empty counterexample because the property is always FALSE\n");
}
break;
} else if((leftValue == 0) && (rightValue == 0)){
if (options->verbosityLevel != BmcVerbosityNone_c){
(void) fprintf(vis_stdout,"# BMC: the formula is trivially true");
(void) fprintf(vis_stdout," for counterexamples of length %d\n", k);
}
} else {
BmcCnfInsertClause(cnfClauses, orClause);
array_free(orClause);
BmcWriteClauses(manager, cnfFile, cnfClauses, options);
(void) fclose(cnfFile);
result = BmcCheckSAT(options);
if(options->satSolverError){
break;
}
if(result != NIL(array_t)) {
/*
formula failed
*/
formulaStatus = BmcPropertyFailed_c;
} else {
/* free some used memories */
BmcCnfClausesFree(cnfClauses);
array_free(loopClause);
/*
Use the termination check
*/
if(terminationStatus && (formulaStatus == BmcPropertyUndecided_c) && (bmcStatus != 1)){
if((options->inductiveStep !=0) &&
(k % options->inductiveStep == 0)
)
{
/*
Check for termination for the current value of k.
*/
terminationStatus->k = k;
bmcStatus = BmcAutLtlCheckForTermination(network,
NIL(array_t), terminationStatus,
nodeToMvfAigTable, CoiTable, options);
if(bmcStatus == 1){
maxK = options->maxK;
}
if(bmcStatus == 3){
formulaStatus = BmcPropertyPassed_c;
break;
}
if(bmcStatus == -1){
break;
}
}
} /* terminationStatus */
}
}
k += options->step;
} /* while result and k*/
/*
If no error.
*/
if(bmcStatus != -1){
if(bmcStatus == 1){
(void) fprintf(vis_stdout,
"# BMC: no counterexample found of length up to %d \n", options->maxK);
(void) fprintf(vis_stdout, "# BMC: By termination criterion (m+n-1)\n");
formulaStatus = BmcPropertyPassed_c;
}
if(options->satSolverError){
(void) fprintf(vis_stdout,"# BMC: Error in calling SAT solver\n");
} else {
if(formulaStatus == BmcPropertyFailed_c) {
(void) fprintf(vis_stdout, "# BMC: formula failed\n");
if(options->verbosityLevel != BmcVerbosityNone_c){
(void) fprintf(vis_stdout,
"# BMC: Found a counterexample of length = %d \n", k);
}
if ((options->dbgLevel == 1) && (result != NIL(array_t))) {
BmcPrintCounterExample(network, nodeToMvfAigTable, cnfClauses,
result, k, CoiTable, options, loopClause);
}
/* free some used memories */
BmcCnfClausesFree(cnfClauses);
array_free(loopClause);
array_free(result);
} else if(formulaStatus == BmcPropertyPassed_c) {
(void) fprintf(vis_stdout, "# BMC: formula Passed\n");
(void) fprintf(vis_stdout, "# Termination depth = %d\n", maxK);
} else if(formulaStatus == BmcPropertyUndecided_c) {
(void) fprintf(vis_stdout,"# BMC: formula undecided\n");
if (options->verbosityLevel != BmcVerbosityNone_c){
(void) fprintf(vis_stdout,
"# BMC: no counterexample found of length up to %d \n",
maxK);
}
}
}
}
if (options->verbosityLevel != BmcVerbosityNone_c) {
endTime = util_cpu_ctime();
fprintf(vis_stdout, "-- bmc time = %10g\n",
(double)(endTime - startTime) / 1000.0);
}
if(terminationStatus){
BmcAutTerminationFree(terminationStatus);
}
fflush(vis_stdout);
return;
} /* Bmc_VerifyUnitDepth() */
Here is the call graph for this function:
| static int checkIndex | ( | int | index, |
| BmcCnfClauses_t * | cnfClauses | ||
| ) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [Check if the index of the varaible in CNF is TURE, FALSE, or none]
Description []
SideEffects []
Definition at line 2834 of file bmcBmc.c.
{
int rtnValue = -1; /* it is not TRUE or FALSE*/
if (index == 0){ /* TRUE or FALSE*/
if (cnfClauses->emptyClause){ /* last added clause was empty = FALSE*/
rtnValue = 0; /* FALSE */
} else {
/*
if (cnfClauses->noOfClauses == 0)
rtnValue = 1;
}
*/
rtnValue = 1; /* TRUE */
}
}
return rtnValue;
}
Here is the caller graph for this function:
| static int doAnd | ( | int | left, |
| int | right | ||
| ) | [static] |
Function********************************************************************
Synopsis []
Description [ 0 1 -1 ---------- 0 0 0 0 1 0 1 -1 -1 0 -1 -1
]
SideEffects []
Definition at line 2872 of file bmcBmc.c.
{
if ((left == -1) && (right == -1)){
return -1;
}
return (left * right);
} /* doAnd */
Here is the caller graph for this function:
| static int doOr | ( | int | left, |
| int | right | ||
| ) | [static] |
Function********************************************************************
Synopsis []
Description [ 0 1 -1 ----------- 0 0 1 -1 1 1 1 -1 -1 -1 -1 -1
]
SideEffects []
Definition at line 2900 of file bmcBmc.c.
{
if ((left == -1) || (right == -1)){
return -1;
}
if ((left == 1) || (right == 1)){
return 1;
}
return 0;
} /* doOr */
Here is the caller graph for this function:
Variable Documentation
char rcsid [] UNUSED = "$Id: bmcBmc.c,v 1.72 2005/10/14 04:41:11 awedh Exp $" [static] |
CFile***********************************************************************
FileName [bmcBmc.c]
PackageName [bmc]
Synopsis [SAT-based ltl model checker.]
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.]
