/**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.] ******************************************************************************/ #include "bmcInt.h" #include "sat.h" #include "baig.h" static char rcsid[] UNUSED = "$Id: bmcCirCUs.c,v 1.56 2010/04/09 23:50:57 fabio Exp $"; /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Type declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Structure declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Variable declarations */ /*---------------------------------------------------------------------------*/ /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Static function prototypes */ /*---------------------------------------------------------------------------*/ 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); /**AutomaticEnd***************************************************************/ /*---------------------------------------------------------------------------*/ /* Definition of exported functions */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ /*---------------------------------------------------------------------------*/ /**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 [] ******************************************************************************/ void BmcCirCUsLtlVerifyProp( Ntk_Network_t *network, Ctlsp_Formula_t *ltl, st_table *coiTable, BmcOption_t *options) { 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() */ /**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 [] ******************************************************************************/ int BmcCirCUsLtlCheckInductiveInvariant( Ntk_Network_t *network, Ctlsp_Formula_t *ltl, BmcOption_t *options, st_table *CoiTable) { 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 */ /**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 [] ******************************************************************************/ void BmcCirCUsLtlVerifyGp( Ntk_Network_t *network, Ctlsp_Formula_t *ltl, st_table *coiTable, BmcOption_t *options) { 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() */ /**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 [] ******************************************************************************/ void BmcCirCUsLtlVerifyFp( Ntk_Network_t *network, Ctlsp_Formula_t *ltl, st_table *coiTable, BmcOption_t *options) { 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 ); /** * How can we manage cone of influence with this part ? **/ 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() */ /**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 [] ******************************************************************************/ bAigEdge_t BmcCirCUsGenerateLogicForLtl( Ntk_Network_t *network, Ctlsp_Formula_t *ltl, int from, int to, int loop) { 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 = (loopleft, 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=(fromright, 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); } /**Function******************************************************************** Synopsis [Build AIG graph for BMC encoding using Separated Normal Form (SNF)] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ bAigEdge_t BmcCirCUsGenerateLogicForLtlSNF( Ntk_Network_t *network, array_t *formulaArray, int fromState, int toState, int loop) { 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 */ /**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 [] ******************************************************************************/ bAigEdge_t BmcCirCUsGenerateLogicForLtlFixPoint( Ntk_Network_t *network, Ctlsp_Formula_t *ltl, int from, int to, array_t *loopArray) { 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 */ /**Function******************************************************************** Synopsis [The recursive function of BmcCirCUsGenerateLogicForLtlFixPoint] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ bAigEdge_t BmcCirCUsGenerateLogicForLtlFixPointRecursive( Ntk_Network_t *network, Ctlsp_Formula_t *ltl, int from, int to, int translation, /* 0 auxilary translation. 1 final translation */ array_t *loopArray, st_table *ltl2AigTable) { 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); } /**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 [] ******************************************************************************/ void BmcCirCUsLtlVerifyFGp( Ntk_Network_t *network, Ctlsp_Formula_t *ltlFormula, st_table *coiTable, BmcOption_t *options) { 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() */ /**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 [] ******************************************************************************/ void BmcCirCUsLtlVerifyGeneralLtl( Ntk_Network_t *network, Ctlsp_Formula_t *ltl, st_table *coiTable, array_t *constraintArray, BmcOption_t *options, int snf) { 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); } /**Function******************************************************************** Synopsis [Verify LTL property using BMC] Description [We use the encoding of "Simple Bounded LTL Model Checking", FMCAD04] SideEffects [] SeeAlso [BmcCirCUsConnectFromStateToState] ******************************************************************************/ void BmcCirCUsLtlVerifyGeneralLtlFixPoint( Ntk_Network_t *network, Ctlsp_Formula_t *ltl, st_table *coiTable, array_t *constraintArray, BmcOption_t *options) { 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); } /**Function******************************************************************** Synopsis [Apply BMC on a safety properties] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ void BmcCirCUsLtlCheckSafety( Ntk_Network_t *network, Ctlsp_Formula_t *ltl, BmcOption_t *options, st_table *coiTable) { 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; } /**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 [] ******************************************************************************/ bAigEdge_t BmcCirCUsConnectFromStateToState( Ntk_Network_t *network, int from, int to, st_table *nodeToMvfAigTable, st_table *coiIndexTable, int withInitialState) { 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; ldbgOut) { dbgOut = vis_stdout; vis_stdout = options->dbgOut; } /** check index such as, k, length, loop */ 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; } /**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 [] ******************************************************************************/ void BmcCirCUsPrintCounterExampleAiger( Ntk_Network_t *network, st_table *nodeToMvfAigTable, st_table *coiTable, int length, array_t *loop_arr, BmcOption_t *options, int withInitialState) { 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; } /** check index such as, k, length, loop */ 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; kinputArr); 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)||(kli2index, timeframe->latchInputs, latchArr, k, prevLatchValues); fprintf(vis_stdout, " "); if((loop<0)||(kpi2index, 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 */ /**Function******************************************************************** Synopsis [] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ static int printSatValue( bAig_Manager_t *manager, st_table *nodeToMvfAigTable, st_table *li2index, bAigEdge_t **baigArr, array_t *nodeArr, int bound, int *prevValue) { 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=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, "\n"); } return 0; } /**Function******************************************************************** Synopsis [Prints the counter-example in the Aiger Format.] Description [] SideEffects [] SeeAlso [BmcCirCUsPrintCounterExampleAiger] ******************************************************************************/ static int printSatValueAiger( bAig_Manager_t *manager, st_table *nodeToMvfAigTable, st_table *li2index, bAigEdge_t **baigArr, array_t *nodeArr, int bound, int *prevValue) { 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=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 */ /**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 [] ******************************************************************************/ bAigEdge_t BmcCirCUsCreatebAigOfPropFormula( Ntk_Network_t *network, bAig_Manager_t *manager, int bound, Ctlsp_Formula_t *ltl, int withInitialState) { 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_NOT_c: result = mAig_Not(left); break; **/ 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 */ /**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 [] ******************************************************************************/ bAigEdge_t BmcCirCUsCreatebAigOfPropFormulaOriginal( Ntk_Network_t *network, bAig_Manager_t *manager, Ctlsp_Formula_t *ltl ) { 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_NOT_c: result = mAig_Not(left); break; **/ 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 */ /**Function******************************************************************** Synopsis [ Check the given string is integer] Description [ Check the given string is integer] SideEffects [] SeeAlso [] ******************************************************************************/ static int StringCheckIsInteger( char *string, int *value) { 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 ; } /**Function******************************************************************** Synopsis [ CirCUs interface for bounded model checking.] Description [ CirCUs interface for bounded model checking. ] SideEffects [] SeeAlso [] ******************************************************************************/ satInterface_t * BmcCirCUsInterface( bAig_Manager_t *manager, Ntk_Network_t *network, bAigEdge_t object, array_t *auxObjectArray, BmcOption_t *bmcOption, satInterface_t *interface) { 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; istatus = 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); } /**Function******************************************************************** Synopsis [ CirCUs interface for bounded model checking.] Description [ CirCUs interface for bounded model checking. ] SideEffects [] SeeAlso [] ******************************************************************************/ 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 *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; istatus = SAT_UNSAT; break; } sat_ArrayInsert(cm->auxObj, tv); } } if(objectArray) { cm->obj = sat_ArrayAlloc(objectArray->num+1); size = objectArray->num; for(i=0; istatus = 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); } /**Function******************************************************************** Synopsis [ Create Manager for debug purpose.] Description [ Create Manager for debug purpose.] SideEffects [] SeeAlso [] ******************************************************************************/ satManager_t * BmcCirCUsCreateManager( Ntk_Network_t *network) { 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); } /**Function******************************************************************** Synopsis [Return a list of AIG in the initialized timeframe corrsponding to the input of all lateches in COI table] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ st_table * BmcCirCUsGetCoiIndexTable( Ntk_Network_t *network, st_table *coiTable) { 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); } /**Function******************************************************************** Synopsis [ Restore aseerted node for SAT solving] Description [ Restore aseerted node for SAT solving] SideEffects [] SeeAlso [bAig_ExpandTimeFrame] ******************************************************************************/ void BmcRestoreAssertion(bAig_Manager_t *manager, satManager_t *cm) { 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; iassertion, v); } } else { cm->assertion = 0; } } /*---------------------------------------------------------------------------*/ /* Definition of static functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Check if the property is TRUE or FALSE] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ static int verifyIfConstant( bAigEdge_t property) { 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; }