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