#include "bmcInt.h"#include "sat.h"#include "baig.h"
Include dependency graph for bmcCirCUs.c:
Go to the source code of this file.
Functions | |
| static int | printSatValue (bAig_Manager_t *manager, st_table *nodeToMvfAigTable, st_table *li2index, bAigEdge_t **baigArr, array_t *nodeArr, int bound, int *prevValue) |
| static int | printSatValueAiger (bAig_Manager_t *manager, st_table *nodeToMvfAigTable, st_table *li2index, bAigEdge_t **baigArr, array_t *nodeArr, int bound, int *prevValue) |
| static int | StringCheckIsInteger (char *string, int *value) |
| static int | verifyIfConstant (bAigEdge_t property) |
| void | BmcCirCUsLtlVerifyProp (Ntk_Network_t *network, Ctlsp_Formula_t *ltl, st_table *coiTable, BmcOption_t *options) |
| int | BmcCirCUsLtlCheckInductiveInvariant (Ntk_Network_t *network, Ctlsp_Formula_t *ltl, BmcOption_t *options, st_table *CoiTable) |
| void | BmcCirCUsLtlVerifyGp (Ntk_Network_t *network, Ctlsp_Formula_t *ltl, st_table *coiTable, BmcOption_t *options) |
| void | BmcCirCUsLtlVerifyFp (Ntk_Network_t *network, Ctlsp_Formula_t *ltl, st_table *coiTable, BmcOption_t *options) |
| bAigEdge_t | BmcCirCUsGenerateLogicForLtl (Ntk_Network_t *network, Ctlsp_Formula_t *ltl, int from, int to, int loop) |
| bAigEdge_t | BmcCirCUsGenerateLogicForLtlSNF (Ntk_Network_t *network, array_t *formulaArray, int fromState, int toState, int loop) |
| bAigEdge_t | BmcCirCUsGenerateLogicForLtlFixPoint (Ntk_Network_t *network, Ctlsp_Formula_t *ltl, int from, int to, array_t *loopArray) |
| bAigEdge_t | BmcCirCUsGenerateLogicForLtlFixPointRecursive (Ntk_Network_t *network, Ctlsp_Formula_t *ltl, int from, int to, int translation, array_t *loopArray, st_table *ltl2AigTable) |
| void | BmcCirCUsLtlVerifyFGp (Ntk_Network_t *network, Ctlsp_Formula_t *ltlFormula, st_table *coiTable, BmcOption_t *options) |
| void | BmcCirCUsLtlVerifyGeneralLtl (Ntk_Network_t *network, Ctlsp_Formula_t *ltl, st_table *coiTable, array_t *constraintArray, BmcOption_t *options, int snf) |
| void | BmcCirCUsLtlVerifyGeneralLtlFixPoint (Ntk_Network_t *network, Ctlsp_Formula_t *ltl, st_table *coiTable, array_t *constraintArray, BmcOption_t *options) |
| void | BmcCirCUsLtlCheckSafety (Ntk_Network_t *network, Ctlsp_Formula_t *ltl, BmcOption_t *options, st_table *coiTable) |
| bAigEdge_t | BmcCirCUsConnectFromStateToState (Ntk_Network_t *network, int from, int to, st_table *nodeToMvfAigTable, st_table *coiIndexTable, int withInitialState) |
| bAigEdge_t | BmcCirCUsSimlePathConstraint (Ntk_Network_t *network, int fromState, int toState, st_table *nodeToMvfAigTable, st_table *coiIndexTable, int withInitialState) |
| bAigEdge_t | BmcCirCUsGenerateSimplePath (Ntk_Network_t *network, int from, int to, st_table *nodeToMvfAigTable, st_table *coiIndexTable, int withInitialState) |
| void | BmcCirCUsPrintCounterExample (Ntk_Network_t *network, st_table *nodeToMvfAigTable, st_table *coiTable, int length, array_t *loop_arr, BmcOption_t *options, int withInitialState) |
| void | BmcCirCUsPrintCounterExampleAiger (Ntk_Network_t *network, st_table *nodeToMvfAigTable, st_table *coiTable, int length, array_t *loop_arr, BmcOption_t *options, int withInitialState) |
| bAigEdge_t | BmcCirCUsCreatebAigOfPropFormula (Ntk_Network_t *network, bAig_Manager_t *manager, int bound, Ctlsp_Formula_t *ltl, int withInitialState) |
| bAigEdge_t | BmcCirCUsCreatebAigOfPropFormulaOriginal (Ntk_Network_t *network, bAig_Manager_t *manager, Ctlsp_Formula_t *ltl) |
| satInterface_t * | BmcCirCUsInterface (bAig_Manager_t *manager, Ntk_Network_t *network, bAigEdge_t object, array_t *auxObjectArray, BmcOption_t *bmcOption, satInterface_t *interface) |
| satInterface_t * | BmcCirCUsInterfaceWithObjArr (bAig_Manager_t *manager, Ntk_Network_t *network, array_t *objectArray, array_t *auxObjectArray, BmcOption_t *bmcOption, satInterface_t *interface) |
| satManager_t * | BmcCirCUsCreateManager (Ntk_Network_t *network) |
| st_table * | BmcCirCUsGetCoiIndexTable (Ntk_Network_t *network, st_table *coiTable) |
| void | BmcRestoreAssertion (bAig_Manager_t *manager, satManager_t *cm) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: bmcCirCUs.c,v 1.56 2010/04/09 23:50:57 fabio Exp $" |
Function Documentation
| bAigEdge_t BmcCirCUsConnectFromStateToState | ( | Ntk_Network_t * | network, |
| int | from, | ||
| int | to, | ||
| st_table * | nodeToMvfAigTable, | ||
| st_table * | coiIndexTable, | ||
| int | withInitialState | ||
| ) |
Function********************************************************************
Synopsis [Build AIG for a transition from state "from" to state "to"]
Description [The state next to "from" equal to "to". (from+1) == to]
SideEffects []
SeeAlso []
Definition at line 2358 of file bmcCirCUs.c.
{
bAigEdge_t *fli, *tli;
bAigEdge_t loop, tv;
int l, index, nLatches;
bAigTimeFrame_t *timeframe;
mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
if(withInitialState) timeframe = manager->timeframe;
else timeframe = manager->timeframeWOI;
fli = timeframe->latchInputs[from+1];
tli = timeframe->latchInputs[to];
loop = bAig_One;
nLatches = timeframe->nLatches;
for(l=0; l<nLatches; l++) {
if(!st_lookup_int(coiIndexTable, (char *)(long)l, &index)) continue;
tv = bAig_Eq(manager, fli[l], tli[l]);
loop = bAig_And(manager, tv, loop);
if(loop == bAig_Zero) break;
}
return(loop);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| bAigEdge_t BmcCirCUsCreatebAigOfPropFormula | ( | Ntk_Network_t * | network, |
| bAig_Manager_t * | manager, | ||
| int | bound, | ||
| Ctlsp_Formula_t * | ltl, | ||
| int | withInitialState | ||
| ) |
Function********************************************************************
Synopsis [Builds AND/INVERTER graph (aig) for a propsitional formula at time frame bound]
Description [Builds AND/INVERTER graph for a propsitional formula at time frame bound. Returns bAig ID of the function that is quivalent to the propositional fomula]
SideEffects []
SeeAlso []
case Ctlsp_NOT_c: result = mAig_Not(left); break;
Definition at line 2923 of file bmcCirCUs.c.
{
int index;
bAigEdge_t result, left, right, *li;
bAigTimeFrame_t *timeframe;
if (ltl == NIL(Ctlsp_Formula_t)) return mAig_NULL;
if (ltl->type == Ctlsp_TRUE_c) return mAig_One;
if (ltl->type == Ctlsp_FALSE_c) return mAig_Zero;
assert(Ctlsp_isPropositionalFormula(ltl));
if(withInitialState) timeframe = manager->timeframe;
else timeframe = manager->timeframeWOI;
if (ltl->type == Ctlsp_ID_c){
char *nodeNameString = Ctlsp_FormulaReadVariableName(ltl);
char *nodeValueString = Ctlsp_FormulaReadValueName(ltl);
Ntk_Node_t *node = Ntk_NetworkFindNodeByName(network, nodeNameString);
Var_Variable_t *nodeVar;
int nodeValue;
MvfAig_Function_t *tmpMvfAig;
st_table *nodeToMvfAigTable; /* maps each node to its mvfAig */
if (node == NIL(Ntk_Node_t)) {
char *nameKey;
char tmpName[100];
sprintf(tmpName, "%s_%d", nodeNameString, bound);
nameKey = util_strsav(tmpName);
result = bAig_FindNodeByName(manager, nameKey);
if(result == bAig_NULL){
result = bAig_CreateVarNode(manager, nameKey);
} else {
FREE(nameKey);
}
return result;
}
nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
assert(nodeToMvfAigTable != NIL(st_table));
tmpMvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
if (tmpMvfAig == NIL(MvfAig_Function_t)){
tmpMvfAig = Bmc_NodeBuildMVF(network, node);
array_free(tmpMvfAig);
tmpMvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
}
nodeVar = Ntk_NodeReadVariable(node);
if (Var_VariableTestIsSymbolic(nodeVar)) {
nodeValue = Var_VariableReadIndexFromSymbolicValue(nodeVar, nodeValueString);
if ( nodeValue == -1 ) {
(void) fprintf(vis_stderr, "Value specified in RHS is not in domain of variable\n");
(void) fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString);
return mAig_NULL;
}
}
else {
int check;
check = StringCheckIsInteger(nodeValueString, &nodeValue);
if( check == 0 ) {
(void) fprintf(vis_stderr,"Illegal value in the RHS\n");
(void) fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString);
return mAig_NULL;
}
if( check == 1 ) {
(void) fprintf(vis_stderr,"Value in the RHS is out of range of int\n");
(void) fprintf(vis_stderr,"%s = %s", nodeNameString, nodeValueString);
return mAig_NULL;
}
if ( !(Var_VariableTestIsValueInRange(nodeVar, nodeValue))) {
(void) fprintf(vis_stderr,"Value specified in RHS is not in domain of variable\n");
(void) fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString);
return mAig_NULL;
}
}
result = MvfAig_FunctionReadComponent(tmpMvfAig, nodeValue);
result = bAig_GetCanonical(manager, result);
if(st_lookup_int(timeframe->li2index, (char *)result, &index)) {
li = timeframe->latchInputs[bound];
result = bAig_GetCanonical(manager, li[index]);
}
else if(st_lookup_int(timeframe->o2index, (char *)result, &index)) {
li = timeframe->outputs[bound];
result = bAig_GetCanonical(manager, li[index]);
}
else if(st_lookup_int(timeframe->i2index, (char *)result, &index)) {
li = timeframe->internals[bound];
result = bAig_GetCanonical(manager, li[index]);
}
return result;
}
left = BmcCirCUsCreatebAigOfPropFormula(network, manager, bound, ltl->left, withInitialState);
if (left == mAig_NULL){
return mAig_NULL;
}
right = BmcCirCUsCreatebAigOfPropFormula(network, manager, bound, ltl->right, withInitialState);
if (right == mAig_NULL && ltl->type ==Ctlsp_NOT_c ){
return mAig_Not(left);
}
else if(right == mAig_NULL) {
return mAig_NULL;
}
switch(ltl->type) {
case Ctlsp_OR_c:
result = mAig_Or(manager, left, right);
break;
case Ctlsp_AND_c:
result = mAig_And(manager, left, right);
break;
case Ctlsp_THEN_c:
result = mAig_Then(manager, left, right);
break;
case Ctlsp_EQ_c:
result = mAig_Eq(manager, left, right);
break;
case Ctlsp_XOR_c:
result = mAig_Xor(manager, left, right);
break;
default:
fail("Unexpected type");
}
return result;
} /* BmcCirCUsCreatebAigOfPropFormula */
Here is the call graph for this function:
Here is the caller graph for this function:
| bAigEdge_t BmcCirCUsCreatebAigOfPropFormulaOriginal | ( | Ntk_Network_t * | network, |
| bAig_Manager_t * | manager, | ||
| Ctlsp_Formula_t * | ltl | ||
| ) |
Function********************************************************************
Synopsis [Builds AND/INVERTER graph (aig) for a propsitional formula]
Description [Builds AND/INVERTER graph for a propsitional formula. Returns bAig ID of the function that is quivalent to the propositional fomula]
SideEffects []
SeeAlso []
case Ctlsp_NOT_c: result = mAig_Not(left); break;
Definition at line 3083 of file bmcCirCUs.c.
{
bAigEdge_t result, left, right;
if (ltl == NIL(Ctlsp_Formula_t)) return mAig_NULL;
if (ltl->type == Ctlsp_TRUE_c) return mAig_One;
if (ltl->type == Ctlsp_FALSE_c) return mAig_Zero;
assert(Ctlsp_isPropositionalFormula(ltl));
if (ltl->type == Ctlsp_ID_c){
char *nodeNameString = Ctlsp_FormulaReadVariableName(ltl);
char *nodeValueString = Ctlsp_FormulaReadValueName(ltl);
Ntk_Node_t *node = Ntk_NetworkFindNodeByName(network, nodeNameString);
Var_Variable_t *nodeVar;
int nodeValue;
MvfAig_Function_t *tmpMvfAig;
st_table *nodeToMvfAigTable; /* maps each node to its mvfAig */
if (node == NIL(Ntk_Node_t)) {
(void) fprintf(vis_stderr, "bmc error: Could not find node corresponding to the name\t %s\n", nodeNameString);
return mAig_NULL;
}
nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
if (nodeToMvfAigTable == NIL(st_table)){
(void) fprintf(vis_stderr, "bmc error: please run build_partiton_maigs first");
return mAig_NULL;
}
tmpMvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
if (tmpMvfAig == NIL(MvfAig_Function_t)){
tmpMvfAig = Bmc_NodeBuildMVF(network, node);
array_free(tmpMvfAig);
tmpMvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
}
nodeVar = Ntk_NodeReadVariable(node);
if (Var_VariableTestIsSymbolic(nodeVar)) {
nodeValue = Var_VariableReadIndexFromSymbolicValue(nodeVar, nodeValueString);
if ( nodeValue == -1 ) {
(void) fprintf(vis_stderr, "Value specified in RHS is not in domain of variable\n");
(void) fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString);
return mAig_NULL;
}
}
else {
int check;
check = StringCheckIsInteger(nodeValueString, &nodeValue);
if( check == 0 ) {
(void) fprintf(vis_stderr,"Illegal value in the RHS\n");
(void) fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString);
return mAig_NULL;
}
if( check == 1 ) {
(void) fprintf(vis_stderr,"Value in the RHS is out of range of int\n");
(void) fprintf(vis_stderr,"%s = %s", nodeNameString, nodeValueString);
return mAig_NULL;
}
if ( !(Var_VariableTestIsValueInRange(nodeVar, nodeValue))) {
(void) fprintf(vis_stderr,"Value specified in RHS is not in domain of variable\n");
(void) fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString);
return mAig_NULL;
}
}
result = bAig_GetCanonical(manager,
MvfAig_FunctionReadComponent(tmpMvfAig, nodeValue));
return result;
}
left = BmcCirCUsCreatebAigOfPropFormulaOriginal(network, manager, ltl->left);
if (left == mAig_NULL){
return mAig_NULL;
}
right = BmcCirCUsCreatebAigOfPropFormulaOriginal(network, manager, ltl->right);
if (right == mAig_NULL && ltl->type ==Ctlsp_NOT_c ){
return mAig_Not(left);
}
else if(right == mAig_NULL) {
return mAig_NULL;
}
switch(ltl->type) {
case Ctlsp_OR_c:
result = mAig_Or(manager, left, right);
break;
case Ctlsp_AND_c:
result = mAig_And(manager, left, right);
break;
case Ctlsp_THEN_c:
result = mAig_Then(manager, left, right);
break;
case Ctlsp_EQ_c:
result = mAig_Eq(manager, left, right);
break;
case Ctlsp_XOR_c:
result = mAig_Xor(manager, left, right);
break;
default:
fail("Unexpected LTL type");
}
return result;
} /* BmcCirCUsCreatebAigOfPropFormulaOriginal */
Here is the call graph for this function:
Here is the caller graph for this function:
| satManager_t* BmcCirCUsCreateManager | ( | Ntk_Network_t * | network | ) |
Function********************************************************************
Synopsis [ Create Manager for debug purpose.]
Description [ Create Manager for debug purpose.]
SideEffects []
SeeAlso []
Definition at line 3600 of file bmcCirCUs.c.
{
satManager_t *cm;
bAig_Manager_t *manager;
satOption_t *option;
manager = Ntk_NetworkReadMAigManager(network);
/* allocate sat manager*/
cm = sat_InitManager(0);
cm->nodesArraySize = manager->nodesArraySize;
cm->initNodesArraySize = manager->nodesArraySize;
cm->maxNodesArraySize = manager->maxNodesArraySize;
cm->nodesArray = manager->NodesArray;
cm->HashTable = manager->HashTable;
cm->literals = manager->literals;
cm->initNumVariables = (manager->nodesArraySize/bAigNodeSize);
cm->initNumClauses = 0;
cm->initNumLiterals = 0;
cm->comment = ALLOC(char, 2);
cm->comment[0] = ' ';
cm->comment[1] = '\0';
cm->stdErr = vis_stderr;
cm->stdOut = vis_stdout;
cm->status = 0;
cm->orderedVariableArray = 0;
cm->unitLits = sat_ArrayAlloc(16);
cm->pureLits = sat_ArrayAlloc(16);
cm->option = 0;
cm->each = 0;
cm->decisionHead = 0;
cm->variableArray = 0;
cm->queue = 0;
cm->BDDQueue = 0;
cm->unusedAigQueue = 0;
if(cm->status == 0) {
/* initialize option*/
option = sat_InitOption();
/*option->verbose = bmcOption->verbosityLevel;*/
option->verbose = 0;
cm->option = option;
cm->each = sat_InitStatistics();
BmcRestoreAssertion(manager, cm);
/* value reset..*/
sat_CleanDatabase(cm);
/* set cone of influence*/
sat_SetConeOfInfluence(cm);
sat_AllocLiteralsDB(cm);
/*sat_ReportStatistics(cm, cm->each);*/
}
sat_CombineStatistics(cm);
/*
For the case that the input contains CNF clauese;
*/
if(cm->literals)
cm->literals->last = cm->literals->initialSize;
return(cm);
}
Here is the call graph for this function:
| bAigEdge_t BmcCirCUsGenerateLogicForLtl | ( | Ntk_Network_t * | network, |
| Ctlsp_Formula_t * | ltl, | ||
| int | from, | ||
| int | to, | ||
| int | loop | ||
| ) |
Function********************************************************************
Synopsis [Build AIG graph of BMC encoding for a path]
Description [Build AIG graph of BMC encoding for a path. If loop = -1, then the BMC encoding is for no loop path. Otherwise, it is for (to, loop)-loop path]
SideEffects []
SeeAlso []
Definition at line 724 of file bmcCirCUs.c.
{
bAigEdge_t property, temp;
bAigEdge_t left, right, result;
int j, k;
mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
if(Ctlsp_isPropositionalFormula(ltl)){
property = BmcCirCUsCreatebAigOfPropFormula(network, manager, from, ltl, BMC_INITIAL_STATES);
return(property);
}
switch(ltl->type) {
case Ctlsp_NOT_c:
if (!Ctlsp_isPropositionalFormula(ltl->left)){
fprintf(vis_stderr,"BMC error: the LTL formula is not in NNF\n");
return 0;
}
case Ctlsp_AND_c:
left = BmcCirCUsGenerateLogicForLtl(network, ltl->left, from, to, loop);
if(left == bAig_Zero) return(bAig_Zero);
right = BmcCirCUsGenerateLogicForLtl(network, ltl->right, from, to, loop);
return(bAig_And(manager, left, right));
case Ctlsp_OR_c:
left = BmcCirCUsGenerateLogicForLtl(network, ltl->left, from, to, loop);
if(left == bAig_One) return(bAig_One);
right = BmcCirCUsGenerateLogicForLtl(network, ltl->right, from, to, loop);
return(bAig_Or(manager, left, right));
case Ctlsp_F_c:
if(loop >= 0) from = (loop<from) ? loop : from;
result = bAig_Zero;
for(j=from; j<=to; j++) {
left = BmcCirCUsGenerateLogicForLtl(network, ltl->left, j, to, loop);
if(left == bAig_One) return(left);
result = bAig_Or(manager, left, result);
}
return(result);
case Ctlsp_G_c:
if(loop < 0) return(bAig_Zero);
from = (loop < from) ? loop : from;
result = bAig_One;
for(j=from; j<=to; j++) {
left = BmcCirCUsGenerateLogicForLtl(network, ltl->left, j, to, loop);
result = bAig_And(manager, result, left);
if(result == bAig_Zero) break;
}
return(result);
case Ctlsp_X_c:
if(loop>=0 && from == to) from = loop;
else if(from < to) from = from + 1;
else return(bAig_Zero);
left = BmcCirCUsGenerateLogicForLtl(network, ltl->left, from, to, loop);
return(left);
case Ctlsp_U_c:
result = bAig_Zero;
for(j=from; j<=to; j++) {
right = BmcCirCUsGenerateLogicForLtl(network, ltl->right, j, to, loop);
temp = right;
for(k=from; (k<=j-1); k++) {
left = BmcCirCUsGenerateLogicForLtl(network, ltl->left, k, to, loop);
temp = bAig_And(manager, temp, left);
if(temp == bAig_Zero) break;
}
result = bAig_Or(manager, result, temp);
if(result == bAig_One) break;
}
if(loop>=0 && result != bAig_One) {
for(j=loop; j<=from-1; j++) {
right = BmcCirCUsGenerateLogicForLtl(network, ltl->right, j, to, loop);
temp = right;
for(k=from; k<=to; k++) {
left = BmcCirCUsGenerateLogicForLtl(network, ltl->left, k, to, loop);
temp = bAig_And(manager, temp, left);
if(temp == bAig_Zero) break;
}
for(k=loop; k<=j-1; k++) {
left = BmcCirCUsGenerateLogicForLtl(network, ltl->left, k, to, loop);
temp = bAig_And(manager, temp, left);
if(temp == bAig_Zero) break;
}
result = bAig_Or(manager, result, temp);
if(result == bAig_One) break;
}
}
return(result);
case Ctlsp_R_c:
result = bAig_Zero;
if(loop >= 0) {
temp = bAig_One;
for(j=(from<loop ? from : loop); j<=to; j++) {
right = BmcCirCUsGenerateLogicForLtl(network, ltl->right, j, to, loop);
temp = bAig_And(manager, temp, right);
if(temp == bAig_Zero) break;
}
result = bAig_Or(manager, result, temp);
}
if(result != bAig_One) {
for(j=from; j<=to; j++) {
left = BmcCirCUsGenerateLogicForLtl(network, ltl->left, j, to, loop);
temp = left;
for(k=from; k<=j; k++) {
right = BmcCirCUsGenerateLogicForLtl(network, ltl->right, k, to, loop);
temp = bAig_And(manager, temp, right);
if(temp == bAig_Zero) break;
}
result = bAig_Or(manager, temp, result);
if(result == bAig_One) break;
}
if(loop >= 0 && result != bAig_One) {
for(j=loop; j<=from-1; j++) {
left = BmcCirCUsGenerateLogicForLtl(network, ltl->left, j, to, loop);
temp = left;
for(k=from; k<=to; k++) {
right = BmcCirCUsGenerateLogicForLtl(network, ltl->right, k, to, loop);
temp = bAig_And(manager, temp, right);
if(temp == bAig_Zero) break;
}
for(k=loop; k<=j; k++) {
right = BmcCirCUsGenerateLogicForLtl(network, ltl->right, k, to, loop);
temp = bAig_And(manager, temp, right);
if(temp == bAig_Zero) break;
}
result = bAig_Or(manager, result, temp);
if(result == bAig_One) break;
}
}
}
return(result);
default:
fail("Unexpected LTL formula type");
break;
}
assert(0);
return(-1);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| bAigEdge_t BmcCirCUsGenerateLogicForLtlFixPoint | ( | Ntk_Network_t * | network, |
| Ctlsp_Formula_t * | ltl, | ||
| int | from, | ||
| int | to, | ||
| array_t * | loopArray | ||
| ) |
Function********************************************************************
Synopsis [Build AIG graph of BMC encoding for LTL formulae based on fixpoint characteristics of LTL formulae.]
Description [We use BMC encoding based on FMCAD'04 paper: Simple Bounded LTL Model Checking.
This function can only be applied to abbreviation-free LTL formulae. The formula must be in Negation Normal Form. For LTL formula of the form Fp, where p is propositional, this function build AIG for auxiliary translation.]
SideEffects []
SeeAlso []
Definition at line 944 of file bmcCirCUs.c.
{
bAigEdge_t result;
st_table *ltl2AigTable;
assert(ltl != NIL(Ctlsp_Formula_t));
ltl2AigTable = st_init_table(strcmp, st_strhash);
result = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl,
from, to, 0, loopArray, ltl2AigTable);
st_free_table(ltl2AigTable);
return result;
} /* BmcCirCUsGenerateLogicForLtlFixPoint */
Here is the call graph for this function:
Here is the caller graph for this function:
| bAigEdge_t BmcCirCUsGenerateLogicForLtlFixPointRecursive | ( | Ntk_Network_t * | network, |
| Ctlsp_Formula_t * | ltl, | ||
| int | from, | ||
| int | to, | ||
| int | translation, | ||
| array_t * | loopArray, | ||
| st_table * | ltl2AigTable | ||
| ) |
Function********************************************************************
Synopsis [The recursive function of BmcCirCUsGenerateLogicForLtlFixPoint]
Description []
SideEffects []
SeeAlso []
Definition at line 976 of file bmcCirCUs.c.
{
mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
bAigEdge_t property, temp;
bAigEdge_t left, right, result;
int j;
char *nameKey;
char tmpName[100];
/*
Check if AIG was built for this LTL formula at a given time
*/
sprintf(tmpName, "%ld_%d%d", (long)ltl, from, translation);
nameKey = util_strsav(tmpName);
if(st_lookup(ltl2AigTable, nameKey, &result)){
FREE(nameKey);
return result;
}
FREE(nameKey);
if(Ctlsp_isPropositionalFormula(ltl)){
property = BmcCirCUsCreatebAigOfPropFormula(network, manager,
from, ltl, BMC_INITIAL_STATES);
sprintf(tmpName, "%ld_%d%d", (long)ltl, from, 1);
nameKey = util_strsav(tmpName);
st_insert(ltl2AigTable, nameKey, (char*) (long) property);
return(property);
}
switch(ltl->type) {
case Ctlsp_NOT_c:
if (!Ctlsp_isPropositionalFormula(ltl->left)){
fprintf(vis_stderr,"BMC error: the LTL formula is not in NNF\n");
return 0;
}
case Ctlsp_AND_c:
left = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->left, from, to,
translation, loopArray, ltl2AigTable);
if(left == bAig_Zero){
return(bAig_Zero);
}
right = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->right, from, to,
translation, loopArray, ltl2AigTable);
return(bAig_And(manager, left, right));
case Ctlsp_OR_c:
left = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->left, from, to,
translation, loopArray, ltl2AigTable);
if(left == bAig_One){
return(bAig_One);
}
right = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->right, from, to,
translation, loopArray, ltl2AigTable);
return(bAig_Or(manager, left, right));
case Ctlsp_X_c:
if(from < to){
result = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->left, from+1, to,
1, loopArray, ltl2AigTable);
} else {
result = bAig_Zero;
for(j=1; j<=to; j++) {
left = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->left, j, to,
1, loopArray, ltl2AigTable);
temp = bAig_And(manager, array_fetch(bAigEdge_t, loopArray, j), left);
result = bAig_Or(manager, result, temp);
}
}
sprintf(tmpName, "%ld_%d%d", (long) ltl, from, 1);
nameKey = util_strsav(tmpName);
st_insert(ltl2AigTable, nameKey, (char*) (long) result);
return result;
case Ctlsp_U_c:
sprintf(tmpName, "%ld_%d%d", (long) ltl, to, 0); /* 0 for auxiliary translation*/
nameKey = util_strsav(tmpName);
right = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->right, to, to, 1, loopArray, ltl2AigTable);
st_insert(ltl2AigTable, nameKey, (char*) (long) right);
/*
Compute the auxiliary translation.
*/
for(j=to-1; j>=from; j--) {
result = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl, j+1, to, 0, loopArray, ltl2AigTable);
right = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->right, j, to, 1, loopArray, ltl2AigTable);
left = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->left, j, to, 1, loopArray, ltl2AigTable);
result = bAig_And(manager,left, result);
result = bAig_Or(manager,right, result);
sprintf(tmpName, "%ld_%d%d", (long)ltl, j, 0); /* 0 for auxiliary translation*/
nameKey = util_strsav(tmpName);
st_insert(ltl2AigTable, nameKey, (char*) (long) result);
}
/*
Compute the final translation at k.
*/
result = bAig_Zero;
for(j=1; j<=to; j++) {
temp = bAig_And(manager, array_fetch(bAigEdge_t, loopArray, j),
BmcCirCUsGenerateLogicForLtlFixPointRecursive(
network, ltl, j, to, 0, loopArray, ltl2AigTable));
result = bAig_Or(manager, result, temp);
}
right = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->right, to, to, 1, loopArray, ltl2AigTable);
left = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->left,
to, to, 1, loopArray,
ltl2AigTable);
result = bAig_And(manager,left, result);
result = bAig_Or(manager,right, result);
sprintf(tmpName, "%ld_%d%d", (long)ltl, to, 1); /* 1 for final translation*/
nameKey = util_strsav(tmpName);
st_insert(ltl2AigTable, nameKey, (char*) (long) result);
/*
Compute the final translation.
*/
for(j=to-1; j>=from; j--) {
result = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl, j+1, to, 1, loopArray, ltl2AigTable);
right = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->right, j, to, 1, loopArray, ltl2AigTable);
left = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->left, j, to, 1, loopArray, ltl2AigTable);
result = bAig_And(manager,left, result);
result = bAig_Or(manager,right, result);
sprintf(tmpName, "%ld_%d%d", (long)ltl, j, 1);
nameKey = util_strsav(tmpName);
st_insert(ltl2AigTable, nameKey, (char*) (long) result);
}
return(result);
case Ctlsp_R_c:
sprintf(tmpName, "%ld_%d%d", (long)ltl, to, 0); /* 0 for auxiliary translation*/
right = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->right, to, to, 1, loopArray, ltl2AigTable);
nameKey = util_strsav(tmpName);
st_insert(ltl2AigTable, nameKey, (char*) (long) right);
/*
Compute the auxiliary translation.
*/
for(j=to-1; j>=from; j--) {
result = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl, j+1, to, 0, loopArray, ltl2AigTable);
right = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->right, j, to, 1, loopArray, ltl2AigTable);
left = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->left, j, to, 1, loopArray, ltl2AigTable);
result = bAig_Or(manager,left, result);
result = bAig_And(manager,right, result);
sprintf(tmpName, "%ld_%d%d", (long) ltl, j, 0); /* 0 for auxiliary translation*/
nameKey = util_strsav(tmpName);
st_insert(ltl2AigTable, nameKey, (char*) (long) result);
}
/*
Compute the final translation at k.
*/
result = bAig_Zero;
for(j=1; j<=to; j++) {
temp = bAig_And(manager, array_fetch(bAigEdge_t, loopArray, j),
BmcCirCUsGenerateLogicForLtlFixPointRecursive(
network, ltl, j, to, 0, loopArray, ltl2AigTable));
result = bAig_Or(manager, result, temp);
}
right = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->right,
to, to, 1, loopArray,
ltl2AigTable);
left = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->left,
to, to, 1, loopArray,
ltl2AigTable);
result = bAig_Or(manager,left, result);
result = bAig_And(manager,right, result);
sprintf(tmpName, "%ld_%d%d", (long) ltl, to+1, 1); /* 1 for final translation*/
nameKey = util_strsav(tmpName);
st_insert(ltl2AigTable, nameKey, (char*) (long) result);
/*
Compute the final translation.
*/
for(j=to-1; j>=from; j--) {
result = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl, j+1, to, 1, loopArray, ltl2AigTable);
right = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->right, j, to, 1, loopArray, ltl2AigTable);
left = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->left, j, to, 1, loopArray, ltl2AigTable);
result = bAig_Or(manager,left, result);
result = bAig_And(manager,right, result);
sprintf(tmpName, "%ld_%d%d", (long)ltl, j, 1);
nameKey = util_strsav(tmpName);
st_insert(ltl2AigTable, nameKey, (char*) (long) result);
}
return(result);
case Ctlsp_F_c:
/*
Compute only the auxiliary translation.
*/
sprintf(tmpName, "%ld_%d%d", (long)ltl, to, 0); /* 0 for auxiliary translation*/
nameKey = util_strsav(tmpName);
left = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->left,
to, to, 1, loopArray,
ltl2AigTable);
st_insert(ltl2AigTable, nameKey, (char*) (long) left);
for(j=to-1; j>=from; j--) {
result = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl,
j+1, to, 0,
loopArray,
ltl2AigTable);
left = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->left,
j, to, 1, loopArray,
ltl2AigTable);
result = bAig_Or(manager,left, result);
sprintf(tmpName, "%ld_%d%d", (long)ltl, j, 0); /* 0 for auxiliary translation*/
nameKey = util_strsav(tmpName);
st_insert(ltl2AigTable, nameKey, (char*) (long) result);
}
result = bAig_Zero;
for(j=1; j<=to; j++) {
temp = bAig_And(manager, array_fetch(bAigEdge_t, loopArray, j),
BmcCirCUsGenerateLogicForLtlFixPointRecursive(
network, ltl, j, to, 0, loopArray, ltl2AigTable));
result = bAig_Or(manager, result, temp);
}
return(result);
default:
fail("Unexpected LTL formula type");
break;
}
assert(0);
return(-1);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| bAigEdge_t BmcCirCUsGenerateLogicForLtlSNF | ( | Ntk_Network_t * | network, |
| array_t * | formulaArray, | ||
| int | fromState, | ||
| int | toState, | ||
| int | loop | ||
| ) |
Function********************************************************************
Synopsis [Build AIG graph for BMC encoding using Separated Normal Form (SNF)]
Description []
SideEffects []
SeeAlso []
Definition at line 882 of file bmcCirCUs.c.
{
mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
Ctlsp_Formula_t *formula;
bAigEdge_t property = bAig_One;
bAigEdge_t left, right, result;
int i, k;
Ctlsp_Formula_t *leftChild, *rightChild;
for (i = 0; i < array_n(formulaArray); i++) {
formula = array_fetch(Ctlsp_Formula_t *, formulaArray, i);
leftChild = Ctlsp_FormulaReadLeftChild(formula);
rightChild = Ctlsp_FormulaReadRightChild(formula);
if(!strcmp(Ctlsp_FormulaReadVariableName(leftChild), " SNFstart")){
result = BmcCirCUsGenerateLogicForLtl(network, rightChild,
0, toState, loop);
} else
if(!strcmp(Ctlsp_FormulaReadVariableName(leftChild), " SNFbound")){
result = BmcCirCUsGenerateLogicForLtl(network, rightChild,
toState, toState, loop);
} else {
result = bAig_One;
for(k=fromState; k<= toState; k++){
left = BmcCirCUsGenerateLogicForLtl(network, leftChild,
k, toState, loop);
right = BmcCirCUsGenerateLogicForLtl(network, rightChild,
k, toState, loop);
result = bAig_And(manager, result,
bAig_Then(manager, left, right));
}
}
property = bAig_And(manager, property, result);
}
return property;
} /* BmcCirCUsGenerateLogicForLtlSNF */
Here is the call graph for this function:
Here is the caller graph for this function:
| bAigEdge_t BmcCirCUsGenerateSimplePath | ( | Ntk_Network_t * | network, |
| int | from, | ||
| int | to, | ||
| st_table * | nodeToMvfAigTable, | ||
| st_table * | coiIndexTable, | ||
| int | withInitialState | ||
| ) |
Function********************************************************************
Synopsis [Build an AIG graph for a simple path]
Description []
SideEffects []
SeeAlso []
Definition at line 2446 of file bmcCirCUs.c.
{
int i, j;
bAigEdge_t loop, nloop;
mAig_Manager_t *manager;
manager = Ntk_NetworkReadMAigManager(network);
bAig_ExpandTimeFrame(network, manager, to, withInitialState);
nloop = bAig_One;
for(i=from+1; i<=to; i++) {
for(j=from; j<i; j++) {
loop = BmcCirCUsConnectFromStateToState(
network, i-1, j, nodeToMvfAigTable, coiIndexTable, withInitialState);
nloop = bAig_And(manager, nloop, bAig_Not(loop));
}
}
return(nloop);
}
Here is the call graph for this function:
| st_table* BmcCirCUsGetCoiIndexTable | ( | Ntk_Network_t * | network, |
| st_table * | coiTable | ||
| ) |
Function********************************************************************
Synopsis [Return a list of AIG in the initialized timeframe corrsponding to the input of all lateches in COI table]
Description []
SideEffects []
SeeAlso []
Definition at line 3678 of file bmcCirCUs.c.
{
mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
Ntk_Node_t *node;
st_generator *gen;
int tmp;
st_table *node2MvfAigTable =
(st_table *)Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
int mvfSize, index, i;
bAigEdge_t v;
MvfAig_Function_t *mvfAig;
st_table *li2index, *coiIndexTable;
assert(manager->timeframe != 0);
/*
Mohammad Says:
This may solve the problem of calling expandTimeframe before calling this
function. Check with HoonSang.
if(timeframe == 0)
timeframe = bAig_InitTimeFrame(network, manager, 1);
*/
/*
li2index stores AIG id for inputs of all latches
*/
li2index = manager->timeframe->li2index;
coiIndexTable = st_init_table(st_numcmp, st_numhash);
st_foreach_item_int(coiTable, gen, &node, &tmp) {
if(!Ntk_NodeTestIsLatch(node)) continue;
st_lookup(node2MvfAigTable, node, &mvfAig);
mvfSize = array_n(mvfAig);
for(i=0; i< mvfSize; i++){
v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
if(st_lookup_int(li2index, (char *)v, &index))
st_insert(coiIndexTable, (char *)(long)index, (char *)(long)index);
}
}
return(coiIndexTable);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| satInterface_t* BmcCirCUsInterface | ( | bAig_Manager_t * | manager, |
| Ntk_Network_t * | network, | ||
| bAigEdge_t | object, | ||
| array_t * | auxObjectArray, | ||
| BmcOption_t * | bmcOption, | ||
| satInterface_t * | interface | ||
| ) |
Function********************************************************************
Synopsis [ CirCUs interface for bounded model checking.]
Description [ CirCUs interface for bounded model checking. ]
SideEffects []
SeeAlso []
Definition at line 3241 of file bmcCirCUs.c.
{
satManager_t *cm;
satOption_t *option;
satLevel_t *d;
int i, size;
bAigEdge_t tv;
/* allocate sat manager */
cm = sat_InitManager(interface);
cm->nodesArraySize = manager->nodesArraySize;
cm->initNodesArraySize = manager->nodesArraySize;
cm->maxNodesArraySize = manager->maxNodesArraySize;
cm->nodesArray = manager->NodesArray;
cm->HashTable = manager->HashTable;
cm->literals = manager->literals;
cm->initNumVariables = (manager->nodesArraySize/bAigNodeSize);
cm->initNumClauses = 0;
cm->initNumLiterals = 0;
cm->comment = ALLOC(char, 2);
cm->comment[0] = ' ';
cm->comment[1] = '\0';
cm->stdErr = vis_stderr;
cm->stdOut = vis_stdout;
cm->status = 0;
cm->orderedVariableArray = 0;
cm->unitLits = sat_ArrayAlloc(16);
cm->pureLits = sat_ArrayAlloc(16);
cm->option = 0;
cm->each = 0;
cm->decisionHead = 0;
cm->variableArray = 0;
cm->queue = 0;
cm->BDDQueue = 0;
cm->unusedAigQueue = 0;
if(interface)
cm->nonobjUnitLitArray = interface->nonobjUnitLitArray;
if(auxObjectArray) {
cm->auxObj = sat_ArrayAlloc(auxObjectArray->num+1);
size = auxObjectArray->num;
for(i=0; i<size; i++) {
tv = array_fetch(bAigEdge_t, auxObjectArray, i);
if(tv == 1) continue;
else if(tv == 0) {
cm->status = SAT_UNSAT;
break;
}
sat_ArrayInsert(cm->auxObj, tv);
}
}
if(object == 0) cm->status = SAT_UNSAT;
else if(object == 1) cm->status = SAT_SAT;
if(cm->status == 0) {
cm->obj = sat_ArrayAlloc(1);
sat_ArrayInsert(cm->obj, object);
/* initialize option */
option = sat_InitOption();
option->cnfPrefix = bmcOption->cnfPrefix;
/*option->verbose = bmcOption->verbosityLevel; */
option->verbose = 0;
option->timeoutLimit = bmcOption->timeOutPeriod;
sat_SetIncrementalOption(option, bmcOption->incremental);
cm->option = option;
cm->each = sat_InitStatistics();
BmcRestoreAssertion(manager, cm);
/* value reset.. */
sat_CleanDatabase(cm);
/* set cone of influence */
sat_SetConeOfInfluence(cm);
sat_AllocLiteralsDB(cm);
if(bmcOption->cnfFileName != NIL(char)) {
sat_WriteCNF(cm, bmcOption->cnfFileName);
}
if(bmcOption->clauses == 0){ /* CirCUs circuit*/
if (bmcOption->verbosityLevel == BmcVerbosityMax_c) {
fprintf(vis_stdout,
"Number of Variables = %d Number of Clauses = %d\n",
sat_GetNumberOfInitialVariables(cm), sat_GetNumberOfInitialClauses(cm));
}
if (bmcOption->verbosityLevel >= BmcVerbosityMax_c) {
(void)fprintf(vis_stdout,"Calling SAT solver (CirCUs) ...");
(void) fflush(vis_stdout);
}
sat_Main(cm);
if (bmcOption->verbosityLevel >= BmcVerbosityMax_c) {
(void) fprintf(vis_stdout," done ");
(void) fprintf(vis_stdout, "(%g s)\n", cm->each->satTime);
}
} else if(bmcOption->clauses == 1) { /* CirCUs CNF */
satArray_t *result;
char *fileName = NIL(char);
sat_WriteCNF(cm, bmcOption->satInFile);
if(bmcOption->satSolver == cusp){
fileName = BmcCirCUsCallCusp(bmcOption);
}
if(bmcOption->satSolver == CirCUs){
fileName = BmcCirCUsCallCirCUs(bmcOption);
}
if(fileName != NIL(char)){
result = sat_ReadForcedAssignment(fileName);
d = sat_AllocLevel(cm);
sat_PutAssignmentValueMain(cm, d, result);
sat_ArrayFree(result);
}
}
}
sat_CombineStatistics(cm);
if(interface == 0)
interface = ALLOC(satInterface_t, 1);
interface->total = cm->total;
interface->nonobjUnitLitArray = cm->nonobjUnitLitArray;
interface->objUnitLitArray = 0;
interface->savedConflictClauses = cm->savedConflictClauses;
interface->trieArray = cm->trieArray;
interface->status = cm->status;
cm->total = 0;
cm->nonobjUnitLitArray = 0;
cm->savedConflictClauses = 0;
if(cm->maxNodesArraySize > manager->maxNodesArraySize) {
manager->maxNodesArraySize = cm->maxNodesArraySize;
manager->nameList = REALLOC(char *, manager->nameList , manager->maxNodesArraySize/bAigNodeSize);
manager->bddIdArray = REALLOC(int , manager->bddIdArray , manager->maxNodesArraySize/bAigNodeSize);
manager->bddArray = REALLOC(bdd_t *, manager->bddArray , manager->maxNodesArraySize/bAigNodeSize);
}
manager->NodesArray = cm->nodesArray;
manager->literals = cm->literals;
/* For the case that the input contains CNF clauese; */
if(cm->literals)
cm->literals->last = cm->literals->initialSize;
cm->nodesArray = 0;
cm->HashTable = 0;
cm->timeframe = 0;
cm->timeframeWOI = 0;
cm->literals = 0;
sat_FreeManager(cm);
return(interface);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| satInterface_t* BmcCirCUsInterfaceWithObjArr | ( | bAig_Manager_t * | manager, |
| Ntk_Network_t * | network, | ||
| array_t * | objectArray, | ||
| array_t * | auxObjectArray, | ||
| BmcOption_t * | bmcOption, | ||
| satInterface_t * | interface | ||
| ) |
Function********************************************************************
Synopsis [ CirCUs interface for bounded model checking.]
Description [ CirCUs interface for bounded model checking. ]
SideEffects []
SeeAlso []
Definition at line 3413 of file bmcCirCUs.c.
{
satManager_t *cm;
satOption_t *option;
int i, size;
bAigEdge_t tv;
/* allocate sat manager */
cm = sat_InitManager(interface);
cm->nodesArraySize = manager->nodesArraySize;
cm->initNodesArraySize = manager->nodesArraySize;
cm->maxNodesArraySize = manager->maxNodesArraySize;
cm->nodesArray = manager->NodesArray;
cm->HashTable = manager->HashTable;
cm->literals = manager->literals;
cm->initNumVariables = (manager->nodesArraySize/bAigNodeSize);
cm->initNumClauses = 0;
cm->initNumLiterals = 0;
cm->comment = ALLOC(char, 2);
cm->comment[0] = ' ';
cm->comment[1] = '\0';
cm->stdErr = vis_stderr;
cm->stdOut = vis_stdout;
cm->status = 0;
cm->orderedVariableArray = 0;
cm->unitLits = sat_ArrayAlloc(16);
cm->pureLits = sat_ArrayAlloc(16);
cm->option = 0;
cm->each = 0;
cm->decisionHead = 0;
cm->variableArray = 0;
cm->queue = 0;
cm->BDDQueue = 0;
cm->unusedAigQueue = 0;
if(interface)
cm->nonobjUnitLitArray = interface->nonobjUnitLitArray;
if(auxObjectArray) {
cm->auxObj = sat_ArrayAlloc(auxObjectArray->num+1);
size = auxObjectArray->num;
for(i=0; i<size; i++) {
tv = array_fetch(bAigEdge_t, auxObjectArray, i);
if(tv == 1) continue;
else if(tv == 0) {
cm->status = SAT_UNSAT;
break;
}
sat_ArrayInsert(cm->auxObj, tv);
}
}
if(objectArray) {
cm->obj = sat_ArrayAlloc(objectArray->num+1);
size = objectArray->num;
for(i=0; i<size; i++) {
tv = array_fetch(bAigEdge_t, objectArray, i);
if(tv == 1) continue;
else if(tv == 0) {
cm->status = SAT_UNSAT;
break;
}
sat_ArrayInsert(cm->obj, tv);
}
}
if(cm->status == 0) {
/* initialize option */
option = sat_InitOption();
option->cnfPrefix = bmcOption->cnfPrefix;
/*option->verbose = bmcOption->verbosityLevel; */
option->verbose = 0;
option->timeoutLimit = bmcOption->timeOutPeriod;
sat_SetIncrementalOption(option, bmcOption->incremental);
cm->option = option;
cm->each = sat_InitStatistics();
BmcRestoreAssertion(manager, cm);
/* value reset.. */
sat_CleanDatabase(cm);
/* set cone of influence */
sat_SetConeOfInfluence(cm);
sat_AllocLiteralsDB(cm);
if(bmcOption->cnfFileName != NIL(char)) {
sat_WriteCNF(cm, bmcOption->cnfFileName);
}
if(bmcOption->clauses == 0){ /* CirCUs circuit*/
if (bmcOption->verbosityLevel == BmcVerbosityMax_c) {
fprintf(vis_stdout,
"Number of Variables = %d Number of Clauses = %d\n",
sat_GetNumberOfInitialVariables(cm), sat_GetNumberOfInitialClauses(cm));
}
if (bmcOption->verbosityLevel >= BmcVerbosityMax_c) {
(void)fprintf(vis_stdout,"Calling SAT solver (CirCUs) ...");
(void) fflush(vis_stdout);
}
sat_Main(cm);
if (bmcOption->verbosityLevel >= BmcVerbosityMax_c) {
(void) fprintf(vis_stdout," done ");
(void) fprintf(vis_stdout, "(%g s)\n", cm->each->satTime);
}
}else if(bmcOption->clauses == 1) { /* CirCUs CNF */
satArray_t *result;
char *fileName = NIL(char);
sat_WriteCNF(cm, bmcOption->satInFile);
if(bmcOption->satSolver == cusp){
fileName = BmcCirCUsCallCusp(bmcOption);
} else{
if(bmcOption->satSolver == CirCUs){
fileName = BmcCirCUsCallCirCUs(bmcOption);
}
}
if(fileName != NIL(char)){
satLevel_t *d;
cm->status = SAT_SAT;
result = sat_ReadForcedAssignment(fileName);
d = sat_AllocLevel(cm);
sat_PutAssignmentValueMain(cm, d, result);
sat_ArrayFree(result);
} else {
cm->status = SAT_UNSAT;
}
}
/*sat_ReportStatistics(cm, cm->each);*/
}
sat_CombineStatistics(cm);
if(interface == 0){
interface = ALLOC(satInterface_t, 1);
}
interface->total = cm->total;
interface->nonobjUnitLitArray = cm->nonobjUnitLitArray;
interface->objUnitLitArray = 0;
interface->savedConflictClauses = cm->savedConflictClauses;
interface->trieArray = cm->trieArray;
interface->status = cm->status;
cm->total = 0;
cm->nonobjUnitLitArray = 0;
cm->savedConflictClauses = 0;
if(cm->maxNodesArraySize > manager->maxNodesArraySize) {
manager->maxNodesArraySize = cm->maxNodesArraySize;
manager->nameList = REALLOC(char *, manager->nameList , manager->maxNodesArraySize/bAigNodeSize);
manager->bddIdArray = REALLOC(int , manager->bddIdArray , manager->maxNodesArraySize/bAigNodeSize);
manager->bddArray = REALLOC(bdd_t *, manager->bddArray , manager->maxNodesArraySize/bAigNodeSize);
}
manager->NodesArray = cm->nodesArray;
manager->literals = cm->literals;
/*
For the case that the input contains CNF clauses;
*/
if(cm->literals)
cm->literals->last = cm->literals->initialSize;
cm->nodesArray = 0;
cm->HashTable = 0;
cm->timeframe = 0;
cm->timeframeWOI = 0;
cm->literals = 0;
sat_FreeManager(cm);
return(interface);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| int BmcCirCUsLtlCheckInductiveInvariant | ( | Ntk_Network_t * | network, |
| Ctlsp_Formula_t * | ltl, | ||
| BmcOption_t * | options, | ||
| st_table * | CoiTable | ||
| ) |
Function********************************************************************
Synopsis [Check if the LTL formula in the form G(p) (invariant), p is a propositional formula, is an Inductive Invariant using SAT]
Description [Check if the LTL formula in the form G(p), p is a propositional formula, is an Inductive Invariant
An LTL formula G(p), where p is a propositional formula, is an inductive invariant if the following two conditions hold:
1- p holds in all 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 ]
SideEffects []
SeeAlso []
Definition at line 189 of file bmcCirCUs.c.
{
mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
bAigEdge_t property, result;
int satFlag;
satInterface_t *interface;
array_t *objArray = array_alloc(bAigEdge_t, 1);
int returnValue = 0; /* the property is not an inductive
invariant */
/*
Check if the property holds in all initial states.
*/
interface = 0;
bAig_ExpandTimeFrame(network, manager, 1, BMC_INITIAL_STATES);
property = BmcCirCUsCreatebAigOfPropFormula(network, manager, 0, ltl->right, BMC_INITIAL_STATES);
array_insert(bAigEdge_t, objArray, 0, property);
options->cnfPrefix = 0;
interface = BmcCirCUsInterfaceWithObjArr(manager, network, objArray,
NIL(array_t), options, interface);
satFlag = interface->status;
sat_FreeInterface(interface);
if(satFlag == SAT_UNSAT) {
/*
Check the induction step.
*/
interface = 0;
bAig_ExpandTimeFrame(network, manager, 2, BMC_NO_INITIAL_STATES);
property = BmcCirCUsCreatebAigOfPropFormula(network, manager, 0, ltl->right, BMC_NO_INITIAL_STATES);
/*
The property is true at state 0. Remember that the passing property is
the negation of the original property.
*/
result = bAig_Not(property);
property = BmcCirCUsCreatebAigOfPropFormula(network, manager, 1, ltl->right, BMC_NO_INITIAL_STATES);
/*
The property is false at state 1
*/
result = bAig_And(manager, result, property);
array_insert(bAigEdge_t, objArray, 0, result);
options->cnfPrefix = 1;
interface = BmcCirCUsInterfaceWithObjArr(manager, network, objArray,
NIL(array_t), options, interface);
satFlag = interface->status;
sat_FreeInterface(interface);
if(satFlag == SAT_UNSAT) {
returnValue = 1; /* the property is an inductive invariant */
}
}
array_free(objArray);
return returnValue;
} /* BmcCirCUsLtlCheckInductiveInvariant */
Here is the call graph for this function:
Here is the caller graph for this function:
| void BmcCirCUsLtlCheckSafety | ( | Ntk_Network_t * | network, |
| Ctlsp_Formula_t * | ltl, | ||
| BmcOption_t * | options, | ||
| st_table * | coiTable | ||
| ) |
Function********************************************************************
Synopsis [Apply BMC on a safety properties]
Description []
SideEffects []
SeeAlso []
Definition at line 2177 of file bmcCirCUs.c.
{
mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
st_table *nodeToMvfAigTable = NIL(st_table);
long startTime, endTime;
bAigEdge_t noLoop;
int depth, satFlag, bound;
int minK = options->minK;
int maxK = options->maxK;
int boundedFormula;
array_t *previousResultArray;
satInterface_t *interface;
array_t *objArray;
BmcCheckForTermination_t *terminationStatus = 0;
Bmc_PropertyStatus formulaStatus;
st_table *coiIndexTable;
assert(Ctlsp_LtlFormulaTestIsSyntacticallyCoSafe(ltl));
startTime = util_cpu_ctime();
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(ltl, &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(ltl),
NIL(array_t));
assert(Ltl_AutomatonGetStrength(terminationStatus->automaton) == 0); /* Terminal Automaton*/
assert(terminationStatus);
}
}
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);
}
satFlag = SAT_UNSAT;
bAig_ExpandTimeFrame(network, manager, 0, BMC_INITIAL_STATES);
coiIndexTable = BmcCirCUsGetCoiIndexTable(network, coiTable);
interface = 0;
formulaStatus = BmcPropertyUndecided_c;
/*
Hold objects
*/
objArray = array_alloc(bAigEdge_t, 1);
previousResultArray = array_alloc(bAigEdge_t, 0);
bound=minK;
while(bound<=maxK) {
if(options->verbosityLevel == BmcVerbosityMax_c)
fprintf(vis_stdout, "\nGenerate counterexample of length %d\n", bound);
fflush(vis_stdout);
bAig_ExpandTimeFrame(network, manager, bound+1, BMC_INITIAL_STATES);
/*
A counterexample to a safety property is finite path at which the
safety property does not hold.
*/
noLoop = BmcCirCUsGenerateLogicForLtl(network, ltl, 0, bound, -1);
array_insert(bAigEdge_t, objArray, 0, noLoop);
options->cnfPrefix = bound;
interface = BmcCirCUsInterfaceWithObjArr(manager, network,
objArray,
previousResultArray,
options,
interface);
satFlag = interface->status;
if(satFlag == SAT_SAT) {
formulaStatus = BmcPropertyFailed_c;
break;
}
array_insert_last(bAigEdge_t, previousResultArray, bAig_Not(noLoop));
/*
Use the termination check if the the LTL formula is not bounded
*/
if(!boundedFormula &&
(options->inductiveStep !=0) &&
(bound % options->inductiveStep == 0))
{
terminationStatus->k = bound;
BmcCirCUsAutLtlCheckTerminalAutomaton(network, manager,
nodeToMvfAigTable,
terminationStatus,
coiIndexTable, options);
if(terminationStatus->action == 1){
formulaStatus = BmcPropertyPassed_c;
maxK = bound;
break;
}
}
bound += options->step;
}
array_free(objArray);
array_free(previousResultArray);
sat_FreeInterface(interface);
if ((formulaStatus != BmcPropertyFailed_c) && boundedFormula && depth <= options->maxK){
/*
No counterexample of length up to the bounded depth of the LTL formula is
found. Formula passes
*/
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", bound);
}
if (options->dbgLevel == 1) {
BmcCirCUsPrintCounterExample(network, nodeToMvfAigTable, coiTable, bound, NIL(array_t),
options, BMC_INITIAL_STATES);
}
if (options->dbgLevel == 2) {
BmcCirCUsPrintCounterExampleAiger(network, nodeToMvfAigTable, coiTable, bound, NIL(array_t),
options, BMC_INITIAL_STATES);
}
} 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);
}
fflush(vis_stdout);
return;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void BmcCirCUsLtlVerifyFGp | ( | 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 passes.
Note: Before calling this function, the LTL formula must be negated.
]
SideEffects []
SeeAlso []
Definition at line 1236 of file bmcCirCUs.c.
{
mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
st_table *nodeToMvfAigTable = NIL(st_table); /* node to mvfAig */
int j, k, l, satFlag;
long startTime, endTime;
int minK = options->minK;
int maxK = options->maxK;
Ctlsp_Formula_t *propFormula;
bAigEdge_t property, loop, pathProperty, tloop;
array_t *loop_array = NIL(array_t);
array_t *previousResultArray;
st_table *coiIndexTable;
satInterface_t *ceInterface;
Bmc_PropertyStatus formulaStatus;
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 */
/* ************** */
startTime = util_cpu_ctime();
if(options->verbosityLevel >= BmcVerbosityMax_c){
fprintf(vis_stdout,"LTL formula is of type FG(p)\n");
}
propFormula = Ctlsp_FormulaReadRightChild(Ctlsp_FormulaReadRightChild(ltlFormula));
property = BmcCirCUsCreatebAigOfPropFormulaOriginal(network, manager,
propFormula);
if (verifyIfConstant(property)){
if (options->verbosityLevel != BmcVerbosityNone_c){
fprintf(vis_stdout, "-- bmc time = %10g\n",
(double)(util_cpu_ctime() - startTime) / 1000.0);
}
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));
bAig_ExpandTimeFrame(network, manager, 0, BMC_INITIAL_STATES);
coiIndexTable = BmcCirCUsGetCoiIndexTable(network, coiTable);
previousResultArray = array_alloc(bAigEdge_t, 0);
ceInterface = 0;
if(options->verbosityLevel != BmcVerbosityNone_c){
fprintf(vis_stdout,"Apply BMC on counterexample of length >= %d and <= %d (+%d)\n",
options->minK, options->maxK, options->step);
}
k= minK;
formulaStatus = BmcPropertyUndecided_c;
while(k <= maxK){
if (options->verbosityLevel >= BmcVerbosityMax_c) {
(void) fprintf(vis_stdout, "\nGenerate counterexample of length %d\n", k);
}
/*
Expand counterexample length to bound. In BMC, counterexample of length bound means
k+1 time frames.
*/
bAig_ExpandTimeFrame(network, manager, k+1, BMC_INITIAL_STATES );
/*
k-loop
*/
loop_array = array_alloc(bAigEdge_t *, 0);
tloop = bAig_Zero;
/*
Loop from last state to any previous states.
*/
for(l=0; l<=k; l++) {
loop = BmcCirCUsConnectFromStateToState(network, k, l, nodeToMvfAigTable,
coiIndexTable, BMC_INITIAL_STATES);
array_insert(bAigEdge_t, loop_array, l, loop);
pathProperty = bAig_Zero;
for(j=l; j<=k; j++){
property = BmcCirCUsCreatebAigOfPropFormula(network, manager, j, propFormula, BMC_INITIAL_STATES);
pathProperty = bAig_Or(manager, pathProperty, property);
}
tloop = bAig_Or(manager, tloop, bAig_And(manager, pathProperty, loop));
}
options->cnfPrefix = k;
ceInterface = BmcCirCUsInterface(manager, network, tloop,
previousResultArray, options,
ceInterface);
satFlag = ceInterface->status;
if(satFlag == SAT_SAT){
formulaStatus = BmcPropertyFailed_c;
break;
}
array_free(loop_array);
/* ==================
Prove termination
================== */
if((checkLevel < 3) &&
(options->inductiveStep !=0) &&
(k % options->inductiveStep == 0))
{
satInterface_t *tInterface=0, *etInterface=0;
bAigEdge_t simplePath, property;
int i;
/* ===========================
Early termination condition
===========================
*/
if (options->earlyTermination) {
if (options->verbosityLevel >= BmcVerbosityMax_c) {
(void) fprintf(vis_stdout, "\nChecking for early termination at k= %d\n", k);
}
bAig_ExpandTimeFrame(network, manager, k+1, BMC_INITIAL_STATES);
simplePath = BmcCirCUsSimlePathConstraint(network, 0, k, nodeToMvfAigTable,
coiIndexTable, BMC_INITIAL_STATES);
options->cnfPrefix = k;
etInterface = BmcCirCUsInterface(manager, network,
simplePath,
previousResultArray,
options, etInterface);
if(etInterface->status == SAT_UNSAT){
formulaStatus = BmcPropertyPassed_c;
if (options->verbosityLevel >= BmcVerbosityMax_c) {
(void) fprintf(vis_stdout, "# BMC: by early termination\n");
}
break;
}
} /* Early termination */
/*
Check for \beta''(k)
*/
if(checkLevel == 0){
if (options->verbosityLevel == BmcVerbosityMax_c) {
(void) fprintf(vis_stdout, "# BMC: Check Beta''\n");
}
bAig_ExpandTimeFrame(network, manager, k+2, BMC_NO_INITIAL_STATES);
simplePath = BmcCirCUsSimlePathConstraint(network, 0, k+1, nodeToMvfAigTable,
coiIndexTable, BMC_NO_INITIAL_STATES);
property = bAig_One;
for(i=1; i<=k+1; i++){
property = bAig_And(manager, property,
bAig_Not(BmcCirCUsCreatebAigOfPropFormula(
network, manager, i,
propFormula, BMC_NO_INITIAL_STATES)));
}
property = bAig_And(manager, property,
BmcCirCUsCreatebAigOfPropFormula(
network, manager, 0,
propFormula, BMC_NO_INITIAL_STATES));
options->cnfPrefix = k+1;
tInterface = 0;
tInterface = BmcCirCUsInterface(manager, network,
bAig_And(manager, property, simplePath),
previousResultArray, options, tInterface);
if(tInterface->status == SAT_UNSAT){
m = k;
if (options->verbosityLevel >= BmcVerbosityMax_c) {
(void)fprintf(vis_stderr,"m = %d\n", m);
}
checkLevel = 1;
}
} /* Check for Beta'' */
/*
Check for \beta'(k)
*/
if(checkLevel == 0){
if (options->verbosityLevel == BmcVerbosityMax_c) {
(void) fprintf(vis_stdout, "# BMC: Check Beta'\n");
}
bAig_ExpandTimeFrame(network, manager, k+2, BMC_NO_INITIAL_STATES);
simplePath = BmcCirCUsSimlePathConstraint(network, 0, k+1, nodeToMvfAigTable,
coiIndexTable, BMC_NO_INITIAL_STATES);
property = bAig_One;
for(i=0; i<=k; i++){
property = bAig_And(manager, property,
bAig_Not(BmcCirCUsCreatebAigOfPropFormula(
network, manager, i,
propFormula, BMC_NO_INITIAL_STATES)));
}
property = bAig_And(manager, property,
BmcCirCUsCreatebAigOfPropFormula(
network, manager, k+1,
propFormula, BMC_NO_INITIAL_STATES));
options->cnfPrefix = k+1;
tInterface = 0;
tInterface = BmcCirCUsInterface(manager, network,
bAig_And(manager, property, simplePath),
previousResultArray, options, tInterface);
if(tInterface->status == SAT_UNSAT){
m = k;
if (options->verbosityLevel >= BmcVerbosityMax_c) {
(void)fprintf(vis_stderr,"m = %d\n", m);
}
checkLevel = 1;
}
} /* Check for Beta' */
/*
Check for Beta
*/
if(checkLevel == 1){
if (options->verbosityLevel == BmcVerbosityMax_c) {
(void) fprintf(vis_stdout, "# BMC: Check Beta\n");
}
bAig_ExpandTimeFrame(network, manager, k+2, BMC_NO_INITIAL_STATES);
simplePath = BmcCirCUsSimlePathConstraint(network, 0, k+1, nodeToMvfAigTable,
coiIndexTable, BMC_NO_INITIAL_STATES);
property = bAig_And(manager,
bAig_Not(BmcCirCUsCreatebAigOfPropFormula(
network, manager, k,
propFormula, BMC_NO_INITIAL_STATES)),
BmcCirCUsCreatebAigOfPropFormula(
network, manager, k+1,
propFormula, BMC_NO_INITIAL_STATES));
options->cnfPrefix = k+1;
tInterface = BmcCirCUsInterface(manager, network,
bAig_And(manager, property, simplePath),
previousResultArray, options, tInterface);
if(tInterface->status == SAT_UNSAT){
checkLevel = 2;
}
} /* Check Beta*/
if(checkLevel == 2){ /* we check Alpha if Beta is unsatisfiable */
if (options->verbosityLevel == BmcVerbosityMax_c) {
(void) fprintf(vis_stdout, "# BMC: Check Alpha \n");
}
bAig_ExpandTimeFrame(network, manager, k+1, BMC_INITIAL_STATES);
simplePath = BmcCirCUsSimlePathConstraint(network, 0, k, nodeToMvfAigTable,
coiIndexTable, BMC_INITIAL_STATES);
property = BmcCirCUsCreatebAigOfPropFormula(
network, manager, k,
propFormula, BMC_INITIAL_STATES);
options->cnfPrefix = k;
tInterface = 0;
tInterface = BmcCirCUsInterface(manager, network,
bAig_And(manager, property, simplePath),
previousResultArray, options, tInterface);
if(tInterface->status == SAT_UNSAT){
n = k;
checkLevel = 3;
if (options->verbosityLevel == BmcVerbosityMax_c) {
(void)fprintf(vis_stdout,"Value of m=%d n=%d\n", m, n);
}
if (m+n-1 <= maxK){
maxK = m+n-1;
checkLevel = 3;
} else {
checkLevel = 4;
}
}
}/* Chek for Alpha */
if (options->verbosityLevel != BmcVerbosityNone_c) {
endTime = util_cpu_ctime();
fprintf(vis_stdout, "-- Check for termination time = %10g\n",
(double)(endTime - startTime) / 1000.0);
}
} /* Check for termination */
k += options->step;
} /* while result and k*/
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){
BmcCirCUsPrintCounterExample(network, nodeToMvfAigTable, coiTable, k, loop_array,
options, BMC_INITIAL_STATES);
}
if(options->dbgLevel == 2){
BmcCirCUsPrintCounterExampleAiger(network, nodeToMvfAigTable, coiTable, k, loop_array,
options, BMC_INITIAL_STATES);
}
array_free(loop_array);
}
if(checkLevel == 3){
(void) fprintf(vis_stdout, "# BMC: no counterexample of length <= (m+n-1) %d is found \n", m+n-1);
formulaStatus = BmcPropertyPassed_c;
}
if(formulaStatus == BmcPropertyPassed_c) {
(void) fprintf(vis_stdout, "# BMC: formula Passed\n");
(void) fprintf(vis_stdout, "# Termination depth = %d\n", k);
} 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);
}
array_free(previousResultArray);
fflush(vis_stdout);
return;
} /* BmcCirCUsLtlVerifyGFp() */
Here is the call graph for this function:
Here is the caller graph for this function:
| void BmcCirCUsLtlVerifyFp | ( | Ntk_Network_t * | network, |
| Ctlsp_Formula_t * | ltl, | ||
| 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.
Using sat as SAT solver.
] SideEffects []
SeeAlso []
How can we manage cone of influence with this part ?
Definition at line 535 of file bmcCirCUs.c.
{
mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
st_table *nodeToMvfAigTable = NIL(st_table);
long startTime, endTime;
bAigEdge_t property, pathProperty, simplePath, tloop, loop;
int bound, k, satFlag;
array_t *loop_array = NIL(array_t);
array_t *objArray;
array_t *auxObjArray;
st_table *coiIndexTable;
satInterface_t *ceInterface;
satInterface_t *tInterface;
Bmc_PropertyStatus formulaStatus;
startTime = util_cpu_ctime();
if(options->verbosityLevel != BmcVerbosityNone_c){
fprintf(vis_stdout,"LTL formula is of type F(p)\n");
}
property = BmcCirCUsCreatebAigOfPropFormulaOriginal(network, manager,
ltl->right);
if (verifyIfConstant(property)){
if (options->verbosityLevel != BmcVerbosityNone_c){
fprintf(vis_stdout, "-- bmc time = %10g\n",
(double)(util_cpu_ctime() - startTime) / 1000.0);
}
return;
}
nodeToMvfAigTable =
(st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
assert(nodeToMvfAigTable != NIL(st_table));
bAig_ExpandTimeFrame(network, manager, 0, BMC_INITIAL_STATES);
coiIndexTable = BmcCirCUsGetCoiIndexTable(network, coiTable);
/*
Hold objects
*/
objArray = array_alloc(bAigEdge_t, 2);
/*
Unused entry is set to bAig_One
*/
array_insert(bAigEdge_t, objArray, 1, bAig_One);
/*
Hold auxiliary objects (constraints on the path)
*/
auxObjArray = array_alloc(bAigEdge_t, 0);
ceInterface = 0;
tInterface = 0;
formulaStatus = BmcPropertyUndecided_c;
if(options->verbosityLevel != BmcVerbosityNone_c){
fprintf(vis_stdout,"Apply BMC on counterexample of length >= %d and <= %d (+%d)\n",
options->minK, options->maxK, options->step);
}
bound = options->minK;
while(bound<=options->maxK) {
if(options->verbosityLevel == BmcVerbosityMax_c)
fprintf(vis_stdout, "\nBMC: Generate counterexample of length %d\n", bound);
/*
Expand counterexample length to bound. In BMC, counterexample of length bound means
bound+1 time frames.
*/
bAig_ExpandTimeFrame(network, manager, bound+1, BMC_INITIAL_STATES );
loop_array = array_alloc(bAigEdge_t *, 0);
tloop = bAig_Zero;
/*
Loop from state 'bound' to any previous states.
*/
for(k=0; k<=bound; k++) {
loop = BmcCirCUsConnectFromStateToState(network, bound, k, nodeToMvfAigTable,
coiIndexTable, BMC_INITIAL_STATES);
array_insert(bAigEdge_t, loop_array, k, loop);
tloop = bAig_Or(manager, tloop, loop);
}
array_insert(bAigEdge_t, objArray, 0, tloop);
/*
tloop equals true for k-loop path
*/
/*
Property false at all states
*/
pathProperty = bAig_One;
for(k=bound; k>=0; k--) {
property = BmcCirCUsCreatebAigOfPropFormula(network, manager, k, ltl->right, BMC_INITIAL_STATES);
pathProperty = bAig_And(manager, pathProperty, property);
}
array_insert(bAigEdge_t, objArray, 1, pathProperty);
options->cnfPrefix = bound;
ceInterface = BmcCirCUsInterfaceWithObjArr(manager, network,
objArray, auxObjArray,
options, ceInterface);
satFlag = ceInterface->status;
if(satFlag == SAT_SAT){
formulaStatus = BmcPropertyFailed_c;
break;
}
array_insert_last(bAigEdge_t, auxObjArray, bAig_Not(tloop));
if((options->inductiveStep !=0) &&
(bound % options->inductiveStep == 0)){
if (options->verbosityLevel == BmcVerbosityMax_c) {
(void) fprintf(vis_stdout,
"\nBMC: Check for termination\n");
}
simplePath = BmcCirCUsSimlePathConstraint(network, 0, bound, nodeToMvfAigTable,
coiIndexTable,
BMC_INITIAL_STATES);
array_insert(bAigEdge_t, objArray, 0, simplePath);
array_insert(bAigEdge_t, objArray, 1, pathProperty);
tInterface = BmcCirCUsInterfaceWithObjArr(manager, network,
objArray, auxObjArray,
options, tInterface);
if(tInterface->status == SAT_UNSAT){
formulaStatus = BmcPropertyPassed_c;
break;
}
}
bound += options->step;
}
array_free(objArray);
array_free(auxObjArray);
st_free_table(coiIndexTable);
sat_FreeInterface(ceInterface);
sat_FreeInterface(tInterface);
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);
}
if(options->dbgLevel == 1){
BmcCirCUsPrintCounterExample(network, nodeToMvfAigTable, coiTable, bound, loop_array,
options, BMC_INITIAL_STATES);
}
if(options->dbgLevel == 2){
BmcCirCUsPrintCounterExampleAiger(network, nodeToMvfAigTable, coiTable, bound, loop_array,
options, BMC_INITIAL_STATES);
}
} else if(formulaStatus == BmcPropertyPassed_c) {
(void) fprintf(vis_stdout, "# BMC: formula Passed\n");
(void) fprintf(vis_stdout, "# Termination depth = %d\n", bound);
} else if(formulaStatus == BmcPropertyUndecided_c) {
(void) fprintf(vis_stdout,"# BMC: formula undecided\n");
}
if (options->verbosityLevel != BmcVerbosityNone_c) {
endTime = util_cpu_ctime();
fprintf(vis_stdout, "-- bmc time = %10g\n", (double)(endTime - startTime) / 1000.0);
}
fflush(vis_stdout);
array_free(loop_array);
} /* BmcCirCUsLtlVerifyFp() */
Here is the call graph for this function:
Here is the caller graph for this function:
| void BmcCirCUsLtlVerifyGeneralLtl | ( | Ntk_Network_t * | network, |
| Ctlsp_Formula_t * | ltl, | ||
| st_table * | coiTable, | ||
| array_t * | constraintArray, | ||
| BmcOption_t * | options, | ||
| int | snf | ||
| ) |
Function********************************************************************
Synopsis [Use BMC technique 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 as were described in the paper "Improving the Encoding of LTL Model Checking into SAT". If snf=1, we use Separated Normal Form technique to encode LTL properties, otherwise we use the original encoding. ]
SideEffects []
SeeAlso []
Definition at line 1586 of file bmcCirCUs.c.
{
mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
st_table *nodeToMvfAigTable = NIL(st_table);
long startTime, endTime;
boolean fairness = (options->fairFile != NIL(FILE));
int minK = options->minK;
int maxK = options->maxK;
boolean boundedFormula;
array_t *ltlConstraintArray = NIL(array_t);
array_t *fairnessArray = NIL(array_t);
int depth, l, bound, f, satFlag, i;
bAigEdge_t noLoop, loop, ploop;
bAigEdge_t result=bAig_NULL, temp, fair;
array_t *loop_arr = NIL(array_t);
array_t *objArray;
array_t *auxObjArray;
st_table *coiIndexTable;
Ctlsp_Formula_t *formula;
satInterface_t *interface;
array_t *formulaArray = NIL(array_t);
int nextAction = 0;
/*
Use when proving termination
*/
BmcCheckForTermination_t *terminationStatus = 0;
Bmc_PropertyStatus formulaStatus;
nodeToMvfAigTable =
(st_table *) Ntk_NetworkReadApplInfo(network,
MVFAIG_NETWORK_APPL_KEY);
assert(nodeToMvfAigTable != NIL(st_table));
if(fairness) {
Ctlsp_Formula_t *formula; /* a generic LTL formula */
int i; /* iteration variable */
ltlConstraintArray = array_alloc(Ctlsp_Formula_t *, 0);
arrayForEachItem(Ctlsp_Formula_t *, constraintArray, i, formula) {
fprintf(vis_stdout, "Formula: ddd");
Ctlsp_FormulaPrint(vis_stdout, formula);
fprintf(vis_stdout, "\n");
BmcGetCoiForLtlFormula(network, formula, coiTable);
formula = Ctlsp_FormulaCreate(Ctlsp_F_c, formula, NIL(Ctlsp_Formula_t));
array_insert_last(Ctlsp_Formula_t *, ltlConstraintArray, formula);
}
}
/*
For bounded formulae use a tighter upper bound if possible.
*/
boundedFormula = Ctlsp_LtlFormulaTestIsBounded(ltl, &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(ltl),
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);
}
bAig_ExpandTimeFrame(network, manager, 1, 1);
coiIndexTable = BmcCirCUsGetCoiIndexTable(network, coiTable);
interface = 0;
/*
Hold objects
*/
objArray = array_alloc(bAigEdge_t, 1);
/*
Hold auxiliary objects (constraints on the path)
*/
auxObjArray = array_alloc(bAigEdge_t, 0);
formulaStatus = BmcPropertyUndecided_c;
bound = minK;
if(snf){
formulaArray = Ctlsp_LtlTranslateIntoSNF(ltl);
}
startTime = util_cpu_ctime();
while(bound<=maxK) {
if(options->verbosityLevel == BmcVerbosityMax_c){
fprintf(vis_stdout, "\nGenerate counterexample of length %d\n", bound);
}
loop_arr = 0;
bAig_ExpandTimeFrame(network, manager, bound+1, BMC_INITIAL_STATES);
if(fairness){
/*
In case of fairness constraints, we only include a loop part of BMC
encoding
*/
noLoop = bAig_Zero;
} else {
if(snf){
noLoop = BmcCirCUsGenerateLogicForLtlSNF(network, formulaArray, 0, bound, -1);
} else {
noLoop = BmcCirCUsGenerateLogicForLtl(network, ltl, 0, bound, -1);
}
}
result = noLoop;
if(noLoop != bAig_One) {
loop_arr = array_alloc(bAigEdge_t, 0);
for(l=0; l<=bound; l++) {
if(snf){
loop = BmcCirCUsGenerateLogicForLtlSNF(network, formulaArray, 0,
bound, l);
} else {
loop = BmcCirCUsGenerateLogicForLtl(network, ltl, 0, bound, l);
}
if(loop == bAig_Zero) continue;
if(fairness) {
fairnessArray = array_alloc(bAigEdge_t, 0);
arrayForEachItem(Ctlsp_Formula_t *, ltlConstraintArray, i, formula) {
fair = BmcCirCUsGenerateLogicForLtl(network, formula, l, bound, -1);
array_insert_last(bAigEdge_t, fairnessArray, fair);
}
}
if(loop != bAig_Zero) {
ploop = BmcCirCUsConnectFromStateToState(network, bound, l, nodeToMvfAigTable, coiIndexTable, 1);
array_insert(bAigEdge_t, loop_arr, l, ploop);
temp = bAig_And(manager, loop, ploop);
if(fairness) {
for(f=0; f < array_n(fairnessArray); f++){
fair = array_fetch(bAigEdge_t, fairnessArray, f);
temp = bAig_And(manager, temp, fair);
}
}
result = bAig_Or(manager, result, temp);
}
if(fairness){
array_free(fairnessArray);
}
}
}
/*
loop = result;
if((noLoop == bAig_Zero) && (loop == bAig_Zero)){
*/
/*
result = noLoop | loop(0) | loop(1) ... | loop(bound)
*/
if(result == bAig_Zero){
if (options->verbosityLevel != BmcVerbosityNone_c){
fprintf(vis_stdout,"# BMC: the formula is trivially true");
fprintf(vis_stdout," for counterexamples of length %d\n", bound);
}
} else {
array_insert(bAigEdge_t, objArray, 0, result);
options->cnfPrefix = bound;
interface = BmcCirCUsInterfaceWithObjArr(manager, network,
objArray, auxObjArray,
options, interface);
satFlag = interface->status;
if(satFlag == SAT_SAT) {
formulaStatus = BmcPropertyFailed_c;
break;
}
array_insert_last(bAigEdge_t, auxObjArray, bAig_Not(result));
}
/*
Use the termination check if the the LTL formula is not bounded
*/
if(!boundedFormula &&
(formulaStatus == BmcPropertyUndecided_c) &&
(nextAction != 1)){
if((options->inductiveStep !=0) &&
(bound % options->inductiveStep == 0))
{
/*
Check for termination for the current value of k.
*/
terminationStatus->k = bound;
BmcCirCUsAutLtlCheckForTermination(network, manager,
nodeToMvfAigTable,
terminationStatus,
coiIndexTable, options);
nextAction = terminationStatus->action;
if(nextAction == 1){
maxK = terminationStatus->k;
} else
if(nextAction == 3){
formulaStatus = BmcPropertyPassed_c;
break;
}
}
} /* terminationStatus */
if(loop_arr) {
array_free(loop_arr);
}
bound += options->step;
}
array_free(objArray);
array_free(auxObjArray);
st_free_table(coiIndexTable);
sat_FreeInterface(interface);
if(formulaStatus == BmcPropertyUndecided_c){
if(nextAction == 1){
/*
No counterexample of length up to maxK is found. By termination
criterion, formula passes
*/
formulaStatus = BmcPropertyPassed_c;
} else
if (boundedFormula && depth <= options->maxK){
/*
No counterexample of length up to the bounded depth of the LTL formula is
found. Formula passes
*/
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", bound);
}
if (options->dbgLevel == 1) {
BmcCirCUsPrintCounterExample(network, nodeToMvfAigTable, coiTable, bound, loop_arr,
options, BMC_INITIAL_STATES);
}
if (options->dbgLevel == 2) {
BmcCirCUsPrintCounterExampleAiger(network, nodeToMvfAigTable, coiTable, bound, loop_arr,
options, BMC_INITIAL_STATES);
}
} 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);
}
}
}
/*
free all used memories
*/
if(terminationStatus){
BmcAutTerminationFree(terminationStatus);
}
if(fairness){
array_free(ltlConstraintArray);
}
if(snf){
Ctlsp_FormulaArrayFree(formulaArray);
}
if (options->verbosityLevel != BmcVerbosityNone_c) {
endTime = util_cpu_ctime();
fprintf(vis_stdout, "-- bmc time = %10g\n", (double)(endTime - startTime) / 1000.0);
}
fflush(vis_stdout);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void BmcCirCUsLtlVerifyGeneralLtlFixPoint | ( | Ntk_Network_t * | network, |
| Ctlsp_Formula_t * | ltl, | ||
| st_table * | coiTable, | ||
| array_t * | constraintArray, | ||
| BmcOption_t * | options | ||
| ) |
Function********************************************************************
Synopsis [Verify LTL property using BMC]
Description [We use the encoding of "Simple Bounded LTL Model Checking", FMCAD04]
SideEffects []
SeeAlso [BmcCirCUsConnectFromStateToState]
Definition at line 1886 of file bmcCirCUs.c.
{
mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
st_table *nodeToMvfAigTable = NIL(st_table);
long startTime, endTime;
bAigEdge_t property, fair;
boolean fairness = (options->fairFile != NIL(FILE));
int minK = options->minK;
int maxK = options->maxK;
boolean boundedFormula;
array_t *ltlConstraintArray = NIL(array_t);
array_t *objArray;
array_t *auxObjArray;
st_table *coiIndexTable;
Ctlsp_Formula_t *formula;
satInterface_t *interface;
int nextAction = 0;
BmcCheckForTermination_t *terminationStatus = 0;
Bmc_PropertyStatus formulaStatus;
array_t *loopArray = NIL(array_t), *smallerExists;
bAigEdge_t tmp, loop, atMostOnce, loopConstraints;
int i, k, depth, satFlag;
startTime = util_cpu_ctime();
nodeToMvfAigTable =
(st_table *) Ntk_NetworkReadApplInfo(network,
MVFAIG_NETWORK_APPL_KEY);
assert(nodeToMvfAigTable != NIL(st_table));
if(fairness) {
ltlConstraintArray = array_alloc(Ctlsp_Formula_t *, 0);
arrayForEachItem(Ctlsp_Formula_t *, constraintArray, i, formula) {
BmcGetCoiForLtlFormula(network, formula, coiTable);
formula = Ctlsp_FormulaCreate(Ctlsp_F_c, formula, NIL(Ctlsp_Formula_t));
array_insert(Ctlsp_Formula_t *, ltlConstraintArray, i, formula);
}
}
/*
For bounded formulae use a tighter upper bound if possible.
*/
boundedFormula = Ctlsp_LtlFormulaTestIsBounded(ltl, &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(ltl),
constraintArray);
assert(terminationStatus);
}
}
if (options->verbosityLevel != BmcVerbosityNone_c){
(void) fprintf(vis_stdout, "General LTL BMC\n");
(void) fprintf(vis_stdout, "Apply BMC on counterexample of length >= %d and <= %d (+%d) \n",
minK, maxK, options->step);
}
bAig_ExpandTimeFrame(network, manager, 1, BMC_INITIAL_STATES);
/*
We need the above line inorder to run the next one.
*/
coiIndexTable = BmcCirCUsGetCoiIndexTable(network, coiTable);
interface = 0;
/*
Hold objects
*/
objArray = array_alloc(bAigEdge_t, 3);
/*
Hold auxiliary objects (constraints on the path)
*/
auxObjArray = array_alloc(bAigEdge_t, 0);
formulaStatus = BmcPropertyUndecided_c;
k = minK;
while(k<=maxK) {
if(options->verbosityLevel == BmcVerbosityMax_c){
fprintf(vis_stdout, "\nGenerate counterexample of length %d\n", k);
}
bAig_ExpandTimeFrame(network, manager, k+1, BMC_INITIAL_STATES);
loopArray = array_alloc(bAigEdge_t, k+1);
array_insert(bAigEdge_t, loopArray, 0, bAig_Zero);
smallerExists = array_alloc(bAigEdge_t, k+1);
array_insert(bAigEdge_t, smallerExists, 0, bAig_Zero);
loop = bAig_One;
for(i=1; i<= k; i++){
tmp = bAig_CreateNode(manager, bAig_NULL, bAig_NULL);
array_insert(bAigEdge_t, loopArray, i, tmp);
tmp = bAig_Then(manager, tmp,
BmcCirCUsConnectFromStateToState(network, k-1, i-1, nodeToMvfAigTable,
coiIndexTable, BMC_INITIAL_STATES));
loop = bAig_And(manager, loop, tmp);
}
array_insert(bAigEdge_t, smallerExists, 1, bAig_Zero);
for(i=1; i<= k; i++){
bAigEdge_t left, right;
left = array_fetch(bAigEdge_t, smallerExists, i);
right = array_fetch(bAigEdge_t, loopArray, i);
array_insert(bAigEdge_t, smallerExists, i+1,
bAig_Or(manager, left, right));
}
atMostOnce = bAig_One;
for(i=1; i<= k; i++){
bAigEdge_t left, right;
left = array_fetch(bAigEdge_t, smallerExists, i);
right = array_fetch(bAigEdge_t, loopArray, i);
tmp = bAig_Then(manager, left, bAig_Not(right));
atMostOnce = bAig_And(manager, atMostOnce, tmp);
}
loopConstraints = bAig_And(manager, loop, atMostOnce);
property = BmcCirCUsGenerateLogicForLtlFixPoint(network, ltl, 0, k, loopArray);
if(fairness) {
fair = bAig_One;
arrayForEachItem(Ctlsp_Formula_t *, ltlConstraintArray, i, formula) {
fair = bAig_And(manager, fair,
BmcCirCUsGenerateLogicForLtlFixPoint(network, formula,
0, k, loopArray));
}
array_insert(bAigEdge_t, objArray, 2, fair);
} else {
array_insert(bAigEdge_t, objArray, 2, bAig_One);
}
array_insert(bAigEdge_t, objArray, 0, loopConstraints);
array_insert(bAigEdge_t, objArray, 1, property);
options->cnfPrefix = k;
interface = BmcCirCUsInterfaceWithObjArr(manager, network,
objArray, objArray,
options, interface);
array_free(smallerExists);
satFlag = interface->status;
if(satFlag == SAT_SAT) {
formulaStatus = BmcPropertyFailed_c;
break;
}
array_free(loopArray);
/*
Use the termination check if the the LTL formula is not bounded
*/
if(!boundedFormula &&
(formulaStatus == BmcPropertyUndecided_c) &&
(nextAction != 1)){
if((options->inductiveStep !=0) &&
(k % options->inductiveStep == 0))
{
/*
Check for termination for the current value of k.
*/
terminationStatus->k = k;
BmcCirCUsAutLtlCheckForTermination(network, manager,
nodeToMvfAigTable,
terminationStatus,
coiIndexTable, options);
nextAction = terminationStatus->action;
if(nextAction == 1){
maxK = terminationStatus->k;
} else
if(nextAction == 3){
formulaStatus = BmcPropertyPassed_c;
maxK = k;
break;
}
}
} /* terminationStatus */
k += options->step;
}
array_free(objArray);
array_free(auxObjArray);
st_free_table(coiIndexTable);
sat_FreeInterface(interface);
if(formulaStatus == BmcPropertyUndecided_c){
/*
If no counterexample of length up to a certain bound, then the property
passes.
*/
if(nextAction == 1){
formulaStatus = BmcPropertyPassed_c;
} else
if (boundedFormula && depth <= options->maxK){
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) {
int loop = k;
/*
Adjust loopArray to print a proper counterexample. The encoding
scheme does not differentiate between loop and no-loop path. If the
path has a loop, then the path length is k-1.
*/
for(i=1; i< k; i++){
bAigEdge_t v = array_fetch(bAigEdge_t, loopArray, i+1);
unsigned int lvalue = aig_value(v);
if(lvalue == 1) {
loop = k-1;
}
array_insert(bAigEdge_t, loopArray, i, v);
}
if (options->dbgLevel == 1) {
BmcCirCUsPrintCounterExample(network, nodeToMvfAigTable,
coiTable, loop, loopArray,
options, BMC_INITIAL_STATES);
}
if (options->dbgLevel == 1) {
BmcCirCUsPrintCounterExampleAiger(network, nodeToMvfAigTable,
coiTable, loop, loopArray,
options, BMC_INITIAL_STATES);
}
array_free(loopArray);
}
} 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);
}
}
}
/*
free all used memories
*/
if(terminationStatus){
BmcAutTerminationFree(terminationStatus);
}
if(fairness){
array_free(ltlConstraintArray);
}
if (options->verbosityLevel != BmcVerbosityNone_c) {
endTime = util_cpu_ctime();
fprintf(vis_stdout, "-- bmc time = %10g\n", (double)(endTime - startTime) / 1000.0);
}
fflush(vis_stdout);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void BmcCirCUsLtlVerifyGp | ( | Ntk_Network_t * | network, |
| Ctlsp_Formula_t * | ltl, | ||
| 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.
Using sat as SAT solver.
]
SideEffects []
SeeAlso []
Definition at line 273 of file bmcCirCUs.c.
{
mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
st_table *nodeToMvfAigTable = NIL(st_table);
long startTime, endTime;
bAigEdge_t property, result, simplePath;
int j, satFlag, k;
int checkInductiveInvariant;
array_t *objArray;
array_t *auxObjArray;
satInterface_t *ceInterface, *etInterface, *tInterface;
st_table *coiIndexTable;
Bmc_PropertyStatus formulaStatus;
assert(Ctlsp_LtlFormulaIsFp(ltl));
startTime = util_cpu_ctime();
if (options->verbosityLevel != BmcVerbosityNone_c){
fprintf(vis_stdout, "LTL formula is of type G(p)\n");
}
property = BmcCirCUsCreatebAigOfPropFormulaOriginal(network, manager, ltl->right);
if (property == mAig_NULL){
return;
}
if (verifyIfConstant(property)){
if (options->verbosityLevel != BmcVerbosityNone_c){
fprintf(vis_stdout, "-- bmc time = %10g\n",
(double)(util_cpu_ctime() - startTime) / 1000.0);
}
return;
}
if (options->verbosityLevel >= BmcVerbosityMax_c){
(void) fprintf(vis_stdout, "\nBMC: Check if the property is an inductive invariant\n");
}
checkInductiveInvariant = BmcCirCUsLtlCheckInductiveInvariant(network, ltl, options, coiTable);
if (checkInductiveInvariant == 1){
(void) fprintf(vis_stdout,"# BMC: The property is an inductive invariant\n");
(void) fprintf(vis_stdout,"# BMC: formula passed\n");
(void) fprintf(vis_stdout, "# Termination depth = 0\n");
if (options->verbosityLevel != BmcVerbosityNone_c){
fprintf(vis_stdout, "-- bmc time = %10g\n",
(double)(util_cpu_ctime() - startTime) / 1000.0);
}
return;
}
nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(network,
MVFAIG_NETWORK_APPL_KEY);
assert(nodeToMvfAigTable != NIL(st_table));
ceInterface = 0;
etInterface = 0;
tInterface = 0;
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);
}
/*
Hold objects
*/
objArray = array_alloc(bAigEdge_t, 2);
/*
Unused entry is set to bAig_One
*/
array_insert(bAigEdge_t, objArray, 1, bAig_One);
/*
Hold auxiliary objects (constraints on the path)
*/
auxObjArray = array_alloc(bAigEdge_t, 0);
bAig_ExpandTimeFrame(network, manager, 1, BMC_NO_INITIAL_STATES);
coiIndexTable = BmcCirCUsGetCoiIndexTable(network, coiTable);
formulaStatus = BmcPropertyUndecided_c;
for(k = options->minK; k <= options->maxK; k += options->step){
if (options->verbosityLevel == BmcVerbosityMax_c){
fprintf(vis_stdout, "\nBMC: Generate counterexample of length %d\n", k);
}
/*
Expand counterexample length to k. In BMC, counterexample of length k means
k+1 time frames.
*/
bAig_ExpandTimeFrame(network, manager, k+1, BMC_INITIAL_STATES);
/*
The property true at any states from (k-step+1) to k
*/
result = bAig_Zero;
for(j=k-options->step+1; j<=k; j++) {
/*
For k = options->minK, j goes outside the lower boundary of
counterexample search.
*/
if(j < options->minK) continue;
property = BmcCirCUsCreatebAigOfPropFormula(network, manager, j, ltl->right, BMC_INITIAL_STATES);
result = bAig_Or(manager, result, property);
}
array_insert(bAigEdge_t, objArray, 0, result);
options->cnfPrefix = k;
ceInterface = BmcCirCUsInterfaceWithObjArr(manager, network, objArray,
auxObjArray, options,
ceInterface);
satFlag = ceInterface->status;
if(satFlag == SAT_SAT){
formulaStatus = BmcPropertyFailed_c;
break;
}
/*
Given that the property does not hold at all previous states.
*/
array_insert_last(bAigEdge_t, auxObjArray, bAig_Not(result));
/*
Prove if the property passes using the induction proof of SSS0.
*/
if((options->inductiveStep !=0) &&
(k % options->inductiveStep == 0)){
array_t *auxArray;
int i;
if (options->verbosityLevel == BmcVerbosityMax_c) {
(void) fprintf(vis_stdout, "\nBMC: Check for termination\n");
}
/*
Expand counterexample length to k+1. In BMC, counterexample of length k+1 means
k+2 time frames.
*/
bAig_ExpandTimeFrame(network, manager, k+2, BMC_NO_INITIAL_STATES);
simplePath = BmcCirCUsSimlePathConstraint(network, 0, k+1, nodeToMvfAigTable,
coiIndexTable, BMC_NO_INITIAL_STATES);
property = BmcCirCUsCreatebAigOfPropFormula(network, manager, k+1, ltl->right,
BMC_NO_INITIAL_STATES);
array_insert(bAigEdge_t, objArray, 0, simplePath);
array_insert(bAigEdge_t, objArray, 1, property);
auxArray = array_alloc(bAigEdge_t, 0);
for(i=0; i<=k; i++){
array_insert_last(bAigEdge_t, auxArray,
bAig_Not(
BmcCirCUsCreatebAigOfPropFormula(network, manager, i, ltl->right,
BMC_NO_INITIAL_STATES)
));
}
options->cnfPrefix = k+1;
tInterface = BmcCirCUsInterfaceWithObjArr(manager, network,
objArray, auxArray,
options, tInterface);
array_free(auxArray);
array_insert(bAigEdge_t, objArray, 1, bAig_One);
if(tInterface->status == SAT_UNSAT){
if (options->verbosityLevel == BmcVerbosityMax_c) {
(void) fprintf(vis_stdout,
"# BMC: No simple path leading to a bad state\n");
}
formulaStatus = BmcPropertyPassed_c;
break;
}
if(options->earlyTermination){
/*
Early termination condition
Check if there is no simple path starts from initial states
*/
simplePath = BmcCirCUsSimlePathConstraint(network, 0, k+1, nodeToMvfAigTable,
coiIndexTable,
BMC_INITIAL_STATES);
array_insert(bAigEdge_t, objArray, 0, simplePath);
etInterface = BmcCirCUsInterfaceWithObjArr(manager, network,
objArray, NIL(array_t),
options, etInterface);
options->cnfPrefix = k+1;
if(etInterface->status == SAT_UNSAT){
if (options->verbosityLevel == BmcVerbosityMax_c) {
(void) fprintf(vis_stdout,
"# BMC: No simple path starting at an initial state\n");
}
formulaStatus = BmcPropertyPassed_c;
break;
}
}
} /* check for termination*/
} /* loop over k*/
array_free(objArray);
array_free(auxObjArray);
sat_FreeInterface(ceInterface);
if(etInterface !=0){
sat_FreeInterface(etInterface);
}
if(tInterface !=0){
sat_FreeInterface(tInterface);
}
st_free_table(coiIndexTable);
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", k);
}
if(options->dbgLevel == 1){
BmcCirCUsPrintCounterExample(network, nodeToMvfAigTable, coiTable, k, 0,
options, BMC_INITIAL_STATES);
}
if(options->dbgLevel == 2){
BmcCirCUsPrintCounterExampleAiger(network, nodeToMvfAigTable, coiTable, k, 0,
options, BMC_INITIAL_STATES);
}
} else if(formulaStatus == BmcPropertyPassed_c) {
(void) fprintf(vis_stdout, "# BMC: formula Passed\n");
(void) fprintf(vis_stdout, "# Termination depth = %d\n", k);
} else if(formulaStatus == BmcPropertyUndecided_c) {
(void) fprintf(vis_stdout,"# BMC: formula undecided\n");
}
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;
} /* BmcCirCUsLtlVerifyGp() */
Here is the call graph for this function:
Here is the caller graph for this function:
| void BmcCirCUsLtlVerifyProp | ( | Ntk_Network_t * | network, |
| Ctlsp_Formula_t * | ltl, | ||
| st_table * | coiTable, | ||
| BmcOption_t * | options | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Apply Bounded Model Checking (BMC) technique 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 78 of file bmcCirCUs.c.
{
mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
st_table *nodeToMvfAigTable = NIL(st_table);
long startTime, endTime;
bAigEdge_t property;
int satFlag;
satInterface_t *interface;
array_t *objArray;
assert(Ctlsp_isPropositionalFormula(ltl));
startTime = util_cpu_ctime();
if (options->verbosityLevel >= BmcVerbosityNone_c){
fprintf(vis_stdout, "LTL formula is propositional\n");
}
property = BmcCirCUsCreatebAigOfPropFormulaOriginal(network, manager, ltl);
if (property == mAig_NULL){
return;
}
if (verifyIfConstant(property)){
if (options->verbosityLevel != BmcVerbosityNone_c){
fprintf(vis_stdout, "-- bmc time = %10g\n",
(double)(util_cpu_ctime() - startTime) / 1000.0);
}
return;
}
nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(network,
MVFAIG_NETWORK_APPL_KEY);
assert(nodeToMvfAigTable != NIL(st_table));
interface = 0;
objArray = array_alloc(bAigEdge_t, 0);
bAig_ExpandTimeFrame(network, manager, 1, BMC_INITIAL_STATES);
property = BmcCirCUsCreatebAigOfPropFormula(network, manager,
0, ltl, BMC_INITIAL_STATES);
array_insert(bAigEdge_t, objArray, 0, property);
options->cnfPrefix = 0;
interface = BmcCirCUsInterfaceWithObjArr(manager, network,
objArray, NIL(array_t),
options, interface);
satFlag = interface->status;
sat_FreeInterface(interface);
if(satFlag == SAT_SAT) {
fprintf(vis_stdout, "# BMC: formula failed\n");
if(options->dbgLevel == 1){
fprintf(vis_stdout, "# BMC: found a counterexample of length 0\n");
BmcCirCUsPrintCounterExample(network, nodeToMvfAigTable, coiTable, 0, 0,
options, BMC_INITIAL_STATES);
}
if(options->dbgLevel == 2){
fprintf(vis_stdout, "# BMC: found a counterexample of length 0\n");
fprintf(vis_stdout, "# The counterexample for Structural Sat problem is incomplete.\n");
BmcCirCUsPrintCounterExampleAiger(network, nodeToMvfAigTable, coiTable, 0, 0,
options, BMC_INITIAL_STATES);
}
}
else if(satFlag != SAT_SAT) {
if(options->verbosityLevel != BmcVerbosityNone_c){
fprintf(vis_stdout,"# BMC: no counterexample found of length 0\n");
}
fprintf(vis_stdout,"# BMC: formula passed\n");
(void) fprintf(vis_stdout, "# Termination depth = 0\n");
}
if (options->verbosityLevel != BmcVerbosityNone_c){
endTime = util_cpu_ctime();
fprintf(vis_stdout, "-- bmc time = %10g\n", (double)(endTime - startTime) / 1000.0);
}
array_free(objArray);
fflush(vis_stdout);
return;
} /* BmcCirCUsLtlVerifyProp() */
Here is the call graph for this function:
Here is the caller graph for this function:
| void BmcCirCUsPrintCounterExample | ( | Ntk_Network_t * | network, |
| st_table * | nodeToMvfAigTable, | ||
| st_table * | coiTable, | ||
| int | length, | ||
| array_t * | loop_arr, | ||
| BmcOption_t * | options, | ||
| int | withInitialState | ||
| ) |
Function********************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
check index such as, k, length, loop
Definition at line 2487 of file bmcCirCUs.c.
{
int *prevLatchValues, *prevInputValues;
mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
int loop, k;
unsigned int lvalue;
bAigEdge_t v;
array_t *latchArr;
lsGen gen;
Ntk_Node_t *node;
int tmp;
bAigTimeFrame_t *timeframe;
FILE *dbgOut = NULL;
latchArr = array_alloc(Ntk_Node_t *, 0);
Ntk_NetworkForEachLatch(network, gen, node){
if (st_lookup_int(coiTable, (char *) node, &tmp)){
array_insert_last(Ntk_Node_t *, latchArr, node);
}
}
if(options->dbgOut)
{
dbgOut = vis_stdout;
vis_stdout = options->dbgOut;
}
if(withInitialState) timeframe = manager->timeframe;
else timeframe = manager->timeframeWOI;
prevLatchValues = ALLOC(int, timeframe->nLatches);
prevInputValues = ALLOC(int, timeframe->nInputs);
loop = -1;
if(loop_arr != 0) {
for(k=array_n(loop_arr)-1; k>=0; k--) {
v = array_fetch(bAigEdge_t, loop_arr, k);
lvalue = aig_value(v);
if(lvalue == 1) {
loop = k;
break;
}
}
}
for(k=0; k<=length; k++) {
if(k == 0) fprintf(vis_stdout, "\n--State %d:\n", k);
else fprintf(vis_stdout, "\n--Goes to state %d:\n", k);
printSatValue(manager, nodeToMvfAigTable,
timeframe->li2index,
timeframe->latchInputs, latchArr,
k, prevLatchValues);
if(options->printInputs == TRUE && k!=0) {
fprintf(vis_stdout, "--On input:\n");
printSatValue(manager, nodeToMvfAigTable,
timeframe->pi2index,
timeframe->inputs, timeframe->inputArr,
k-1, prevInputValues);
}
}
if(loop >=0) {
fprintf(vis_stdout, "\n--Goes back to state %d:\n", loop);
printSatValue(manager, nodeToMvfAigTable,
timeframe->li2index,
timeframe->latchInputs, latchArr,
loop, prevLatchValues);
if(options->printInputs == TRUE && k!=0) {
fprintf(vis_stdout, "--On input:\n");
printSatValue(manager, nodeToMvfAigTable,
timeframe->pi2index,
timeframe->inputs, timeframe->inputArr,
length, prevInputValues);
}
}
array_free(latchArr);
if(options->dbgOut)
{
vis_stdout = dbgOut;
}
return;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void BmcCirCUsPrintCounterExampleAiger | ( | Ntk_Network_t * | network, |
| st_table * | nodeToMvfAigTable, | ||
| st_table * | coiTable, | ||
| int | length, | ||
| array_t * | loop_arr, | ||
| BmcOption_t * | options, | ||
| int | withInitialState | ||
| ) |
Function********************************************************************
Synopsis [Prints the counter-example in Aiger format.]
Description [The Aiger format is as follows, currentState, input, output, nextState the names of the variables aren't printed rather their values are only printed, -i option is set by default.]
SideEffects []
SeeAlso []
check index such as, k, length, loop
Definition at line 2601 of file bmcCirCUs.c.
{
int *prevLatchValues, *prevInputValues;
mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
int loop, k;
unsigned int lvalue;
bAigEdge_t v;
array_t *latchArr;
lsGen gen;
Ntk_Node_t *node;
int tmp;
bAigTimeFrame_t *timeframe;
FILE *dbgOut = NULL;
latchArr = array_alloc(Ntk_Node_t *, 0);
Ntk_NetworkForEachLatch(network, gen, node){
if (st_lookup_int(coiTable, (char *) node, &tmp)){
array_insert_last(Ntk_Node_t *, latchArr, node);
}
}
/* writing into a file is not being done in a standard way, need to confirm
the writing of trace into a file with the vis standard */
if(options->dbgOut)
{
dbgOut = vis_stdout;
vis_stdout = options->dbgOut;
}
if(withInitialState) timeframe = manager->timeframe;
else timeframe = manager->timeframeWOI;
prevLatchValues = ALLOC(int, timeframe->nLatches);
prevInputValues = ALLOC(int, timeframe->nInputs);
loop = -1;
if(loop_arr != 0) {
for(k=array_n(loop_arr)-1; k>=0; k--) {
v = array_fetch(bAigEdge_t, loop_arr, k);
lvalue = aig_value(v);
if(lvalue == 1) {
loop = k;
break;
}
}
}
/* we need to get rid of the file generation for next vis release and look
into ntk package so that the original order can be maintained */
FILE *order = Cmd_FileOpen("inputOrder.txt", "w", NIL(char *), 0) ;
for(k=0; k<array_n(timeframe->inputArr); k++)
{
node = array_fetch(Ntk_Node_t *, timeframe->inputArr, k);
fprintf(order, "%s\n", Ntk_NodeReadName(node));
}
fclose(order);
for(k=0; k<=length; k++) {
/*if(k == 0) fprintf(vis_stdout, "\n--State %d:\n", k);
else fprintf(vis_stdout, "\n--Goes to state %d:\n", k);*/
/*if((loop>=0)||(k<length))
{ */
printSatValueAiger(manager, nodeToMvfAigTable,
timeframe->li2index,
timeframe->latchInputs, latchArr,
k, prevLatchValues);
fprintf(vis_stdout, " ");
if((loop<0)||(k<length))
{
if(k!=length+1) {
printSatValueAiger(manager, nodeToMvfAigTable,
timeframe->pi2index,
timeframe->inputs, timeframe->inputArr,
k, prevInputValues);
fprintf(vis_stdout, " ");
}
if(k!=length+1) {
printSatValueAiger(manager, nodeToMvfAigTable,
timeframe->o2index,
timeframe->outputs, timeframe->outputArr,
k, prevInputValues);
fprintf(vis_stdout, " ");
}
if(k!=length+1) {
printSatValueAiger(manager, nodeToMvfAigTable,
timeframe->li2index,
timeframe->latchInputs, latchArr,
k+1, prevLatchValues);
fprintf(vis_stdout, " ");
}
if((loop < 0)||(k!=length))
{
fprintf(vis_stdout, "\n");
}
}
}
if(loop >=0) {
/*fprintf(vis_stdout, "\n--Goes back to state %d:\n", loop);*/
if(k!=0) {
printSatValueAiger(manager, nodeToMvfAigTable,
timeframe->pi2index,
timeframe->inputs, timeframe->inputArr,
length, prevInputValues);
fprintf(vis_stdout, " ");
}
printSatValueAiger(manager, nodeToMvfAigTable,
timeframe->o2index,
timeframe->outputs, timeframe->outputArr,
k, prevInputValues);
fprintf(vis_stdout, " ");
printSatValueAiger(manager, nodeToMvfAigTable,
timeframe->li2index,
timeframe->latchInputs, latchArr,
loop, prevLatchValues);
fprintf(vis_stdout, "\n");
}
array_free(latchArr);
if(options->dbgOut)
{
vis_stdout = dbgOut;
}
return;
} /* BmcCirCUsPrintCounterExampleAiger */
Here is the call graph for this function:
Here is the caller graph for this function:
| bAigEdge_t BmcCirCUsSimlePathConstraint | ( | Ntk_Network_t * | network, |
| int | fromState, | ||
| int | toState, | ||
| st_table * | nodeToMvfAigTable, | ||
| st_table * | coiIndexTable, | ||
| int | withInitialState | ||
| ) |
Function********************************************************************
Synopsis [Create AIG graph for simple path constraint]
Description [Create AIG graph that constrains a path starting from 'fromState' and ending at 'toState' to be a simple path. A simple path is a path such that every state in the path is distinct. i.e for all states in the path Si != Sj for fromState <= i < j <= toState.]
SideEffects []
SeeAlso []
Definition at line 2405 of file bmcCirCUs.c.
{
int i, j;
bAigEdge_t loop, nLoop;
mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
nLoop = bAig_One;
for(i=fromState+1; i<=toState; i++) {
for(j=fromState; j<i; j++) {
/*
We want state Si == Sj, but the following function returns
S(i+1) == Sj. So we call the function with i-1.
*/
loop = BmcCirCUsConnectFromStateToState(
network, i-1, j, nodeToMvfAigTable, coiIndexTable, withInitialState);
nLoop = bAig_And(manager, nLoop, bAig_Not(loop));
}
}
return(nLoop);
} /* BmcCirCUsSimplePathConstraint */
Here is the call graph for this function:
Here is the caller graph for this function:
| void BmcRestoreAssertion | ( | bAig_Manager_t * | manager, |
| satManager_t * | cm | ||
| ) |
Function********************************************************************
Synopsis [ Restore aseerted node for SAT solving]
Description [ Restore aseerted node for SAT solving]
SideEffects []
SeeAlso [bAig_ExpandTimeFrame]
Definition at line 3734 of file bmcCirCUs.c.
{
int size, i, v;
array_t *asserted;
if(manager->timeframe && manager->timeframe->assertedArray) {
asserted = manager->timeframe->assertedArray;
size = asserted->num;
cm->assertion = sat_ArrayAlloc(size);
for(i=0; i<size; i++) {
v = array_fetch(int, asserted, i);
sat_ArrayInsert(cm->assertion, v);
}
}
else {
cm->assertion = 0;
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static int printSatValue | ( | bAig_Manager_t * | manager, |
| st_table * | nodeToMvfAigTable, | ||
| st_table * | li2index, | ||
| bAigEdge_t ** | baigArr, | ||
| array_t * | nodeArr, | ||
| int | bound, | ||
| int * | prevValue | ||
| ) | [static] |
AutomaticStart
Function********************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
Definition at line 2760 of file bmcCirCUs.c.
{
Ntk_Node_t * node;
int value, lvalue;
char *symbolicValue;
bAigEdge_t *li, v, tv;
int i, j, timeframe, index;
int changed=0;
MvfAig_Function_t *mvfAig;
timeframe = bound;
li = baigArr[timeframe];
for(i=0; i<array_n(nodeArr); i++) {
if(timeframe == 0) prevValue[i] = -1;
node = array_fetch(Ntk_Node_t *, nodeArr, i);
mvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
if(mvfAig == 0) continue;
value = -1;
for (j=0; j< array_n(mvfAig); j++) {
v = MvfAig_FunctionReadComponent(mvfAig, j);
index = -1;
if(!st_lookup_int(li2index, (char *)v, &index)) {
fprintf(vis_stdout, "printSatValueERROR \n");
}
v = li[index];
if(v == bAig_One) {
value = j;
break;
}
if(v != bAig_Zero) {
tv = bAig_GetCanonical(manager, v);
lvalue = bAig_GetValueOfNode(manager, tv);
if(lvalue == 1){
value = j;
break;
}
}
}
if(value >=0) {
if (value != prevValue[i]){
Var_Variable_t *nodeVar = Ntk_NodeReadVariable(node);
prevValue[i] = value;
changed = 1;
if (Var_VariableTestIsSymbolic(nodeVar)) {
symbolicValue = Var_VariableReadSymbolicValueFromIndex(nodeVar, value);
fprintf(vis_stdout,"%s:%s\n", Ntk_NodeReadName(node), symbolicValue);
}
else {
fprintf(vis_stdout,"%s:%d\n", Ntk_NodeReadName(node), value);
}
}
}
} /* for j loop */
if (changed == 0){
fprintf(vis_stdout, "<Unchanged>\n");
}
return 0;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static int printSatValueAiger | ( | bAig_Manager_t * | manager, |
| st_table * | nodeToMvfAigTable, | ||
| st_table * | li2index, | ||
| bAigEdge_t ** | baigArr, | ||
| array_t * | nodeArr, | ||
| int | bound, | ||
| int * | prevValue | ||
| ) | [static] |
Function********************************************************************
Synopsis [Prints the counter-example in the Aiger Format.]
Description []
SideEffects []
SeeAlso [BmcCirCUsPrintCounterExampleAiger]
Definition at line 2842 of file bmcCirCUs.c.
{
Ntk_Node_t * node;
int value, lvalue;
char *symbolicValue;
bAigEdge_t *li, v, tv;
int i, j, timeframe, index;
MvfAig_Function_t *mvfAig;
timeframe = bound;
li = baigArr[timeframe];
for(i=0; i<array_n(nodeArr); i++) {
if(timeframe == 0) prevValue[i] = -1;
node = array_fetch(Ntk_Node_t *, nodeArr, i);
mvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
if(mvfAig == 0) continue;
value = -1;
for (j=0; j< array_n(mvfAig); j++) {
v = MvfAig_FunctionReadComponent(mvfAig, j);
index = -1;
if(!st_lookup_int(li2index, (char *)v, &index)) {
fprintf(vis_stdout, "printSatValueERROR \n");
}
v = li[index];
if(v == bAig_One) {
value = j;
break;
}
if(v != bAig_Zero) {
tv = bAig_GetCanonical(manager, v);
lvalue = bAig_GetValueOfNode(manager, tv);
if(lvalue == 1){
value = j;
break;
}
}
}
if(value >=0) {
Var_Variable_t *nodeVar = Ntk_NodeReadVariable(node);
prevValue[i] = value;
if (Var_VariableTestIsSymbolic(nodeVar)) {
symbolicValue = Var_VariableReadSymbolicValueFromIndex(nodeVar, value);
fprintf(vis_stdout,"%s", symbolicValue);
}
else {
fprintf(vis_stdout,"%d", value);
}
}
else
{
fprintf(vis_stdout,"x");
}
} /* for j loop */
return 0;
} /* printSatValueAiger */
Here is the call graph for this function:
Here is the caller graph for this function:
| static int StringCheckIsInteger | ( | char * | string, |
| int * | value | ||
| ) | [static] |
Function********************************************************************
Synopsis [ Check the given string is integer]
Description [ Check the given string is integer]
SideEffects []
SeeAlso []
Definition at line 3211 of file bmcCirCUs.c.
{
char *ptr;
long l;
l = strtol (string, &ptr, 0) ;
if(*ptr != '\0')
return 0;
if ((l > MAXINT) || (l < -1 - MAXINT))
return 1 ;
*value = (int) l;
return 2 ;
}
Here is the caller graph for this function:
| static int verifyIfConstant | ( | bAigEdge_t | property | ) | [static] |
Function********************************************************************
Synopsis [Check if the property is TRUE or FALSE]
Description []
SideEffects []
SeeAlso []
Definition at line 3771 of file bmcCirCUs.c.
{
if (property == bAig_One){
fprintf(vis_stdout,"# BMC: Empty counterexample because the property is always FALSE\n");
fprintf(vis_stdout,"# BMC: formula failed\n");
return 1;
} else if (property == bAig_Zero){
fprintf(vis_stdout,"# BMC: The property is always TRUE\n");
fprintf(vis_stdout,"# BMC: formula passed\n");
return 1;
}
return 0;
}
Here is the caller graph for this function:
Variable Documentation
char rcsid [] UNUSED = "$Id: bmcCirCUs.c,v 1.56 2010/04/09 23:50:57 fabio Exp $" [static] |
CFile***********************************************************************
FileName [bmcCirCUs.c]
PackageName [bmc]
Synopsis [BMC ltl model checker using CirCUs.]
Author [HoonSang Jin, 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.]
Definition at line 21 of file bmcCirCUs.c.
