/**CFile*********************************************************************** FileName [bmcUtil.c] PackageName [bmc] Synopsis [Utilities for BMC package] 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" #include "sat.h" #include "baig.h" static char rcsid[] UNUSED = "$Id: bmcUtil.c,v 1.82 2010/04/10 04:07:06 fabio Exp $"; /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ #define MAX_LENGTH 320 /* Max. length of a string while reading a file */ /*---------------------------------------------------------------------------*/ /* Type declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Structure declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Variable declarations */ /*---------------------------------------------------------------------------*/ /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Static function prototypes */ /*---------------------------------------------------------------------------*/ static int StringCheckIsInteger(char *string, int *value); static int nameCompare(const void * name1, const void * name2); static void printValue(mAig_Manager_t *manager, Ntk_Network_t *network, st_table *nodeToMvfAigTable, BmcCnfClauses_t *cnfClauses, array_t *varNames, st_table *resultTable, int state, int *prevValue); static void printValueAiger(mAig_Manager_t *manager, Ntk_Network_t *network, st_table *nodeToMvfAigTable, BmcCnfClauses_t *cnfClauses, array_t *varNames, st_table *resultTable, int state, int *prevValue); static void printValueAigerInputs(mAig_Manager_t *manager, Ntk_Network_t *network, st_table *nodeToMvfAigTable, BmcCnfClauses_t *cnfClauses, array_t *varNames, st_table *resultTable, int state, int *prevValue); /**AutomaticEnd***************************************************************/ /*---------------------------------------------------------------------------*/ /* Definition of exported functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Compute cube that is close to target states.] SideEffects [] ******************************************************************************/ mdd_t * Bmc_ComputeCloseCube( mdd_t *states, mdd_t *target, int *dist, Fsm_Fsm_t *modelFsm) { array_t *PSVars = Fsm_FsmReadPresentStateVars( modelFsm ); mdd_manager *mddMgr = Ntk_NetworkReadMddManager( Fsm_FsmReadNetwork( modelFsm ) ); mdd_t *result = BmcComputeCloseCube( states, target, dist, PSVars, mddMgr ); return result; } /**Function******************************************************************** Synopsis [Build multi-valued function for a given node.] SideEffects [The mvf of this node is a function of combinational input nodes.] ******************************************************************************/ MvfAig_Function_t * Bmc_NodeBuildMVF( Ntk_Network_t *network, Ntk_Node_t *node) { MvfAig_Function_t * MvfAig; lsGen tmpGen; Ntk_Node_t *tmpNode; array_t *mvfArray; array_t *tmpRoots = array_alloc(Ntk_Node_t *, 0); st_table *tmpLeaves = st_init_table(st_ptrcmp, st_ptrhash); array_insert_last(Ntk_Node_t *, tmpRoots, node); Ntk_NetworkForEachCombInput(network, tmpGen, tmpNode) { st_insert(tmpLeaves, (char *) tmpNode, (char *) ntmaig_UNUSED); } mvfArray = ntmaig_NetworkBuildMvfAigs(network, tmpRoots, tmpLeaves); MvfAig = array_fetch(MvfAig_Function_t *, mvfArray, 0); array_free(tmpRoots); st_free_table(tmpLeaves); array_free(mvfArray); return MvfAig; } /**Function******************************************************************** Synopsis [Returns MvfAig corresponding to a node; returns NIL if node not in table.] SideEffects [None] ******************************************************************************/ MvfAig_Function_t * Bmc_ReadMvfAig( Ntk_Node_t * node, st_table * nodeToMvfAigTable) { MvfAig_Function_t *result; if (st_lookup(nodeToMvfAigTable, node, &result)){ return result; } return NIL(MvfAig_Function_t); } /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Evaluate states satisfying X target] Description [Evaluate states satisfying X target.] SideEffects [] ******************************************************************************/ mdd_t * BmcFsmEvaluateX( Fsm_Fsm_t *modelFsm, mdd_t *targetMdd) { mdd_t *fromLowerBound; mdd_t *fromUpperBound; mdd_t *result; Img_ImageInfo_t * imageInfo; mdd_t *careStates; array_t *careStatesArray = array_alloc(array_t *, 0); imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 1, 0); /* * The lower bound is the conjunction of the fair states, * and the target states. */ fromLowerBound = mdd_dup(targetMdd); /* * The upper bound is the same as the lower bound. */ fromUpperBound = mdd_dup(fromLowerBound); /* careSet is the set of all unreachabel states. */ careStates = mdd_one(Fsm_FsmReadMddManager(modelFsm)); array_insert(mdd_t *, careStatesArray, 0, careStates); result = Img_ImageInfoComputePreImageWithDomainVars(imageInfo, fromLowerBound, fromUpperBound, careStatesArray); mdd_free(fromLowerBound); mdd_free(fromUpperBound); return result; } /* BmcFsmEvaluateX */ /**Function******************************************************************** Synopsis [Compute cube that is close to target states. Support is an array of mddids representing the total support; that is, all the variables on which aSet may depend. It dos the function only if CUDD is the BDD package.] SideEffects [] ******************************************************************************/ mdd_t * BmcComputeCloseCube( mdd_t *aSet, mdd_t *target, int *dist, array_t *Support, mdd_manager *mddMgr) { if (bdd_get_package_name() == CUDD && target != NIL(mdd_t)) { mdd_t *range; /* range of Support */ mdd_t *legalSet; /* aSet without the don't cares */ mdd_t *closeCube; /* Check that support of set is contained in Support. assert(SetCheckSupport(aSet, Support, mddMgr)); */ assert(!mdd_is_tautology(aSet, 0)); range = mdd_range_mdd(mddMgr, Support); legalSet = bdd_and(aSet, range, 1, 1); mdd_free(range); closeCube = mdd_closest_cube(legalSet, target, dist); mdd_free(legalSet); return closeCube; } else { return aSet; /*return BMC_ComputeAMinterm(aSet, Support, mddMgr);*/ }/* if CUDD */ } /* BmcComputeCloseCube */ /**Function******************************************************************** Synopsis [Build AND/INV graph for intial states] Description [Build AND/INV graph for intial states. Returns bAig Id of the bAig Function that represents the intial states. The initial states are computed as follows. For each latch i, the relation (x_i = g_i(u)) is built, where x_i is the present state variable of latch i, and g_i(u) is the multi-valued initialization function of latch i, in terms of the input variables u. These relations are then conjuncted. ] SideEffects [] SeeAlso [] ******************************************************************************/ mAigEdge_t BmcCreateMaigOfInitialStates( Ntk_Network_t *network, st_table *nodeToMvfAigTable, st_table *CoiTable) { mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network); st_generator *stGen; Ntk_Node_t *latch, *latchInit; MvfAig_Function_t *initMvfAig, *latchMvfAig; bAigEdge_t resultAnd = bAig_One; bAigEdge_t resultOr; int i; st_foreach_item(CoiTable, stGen, &latch, NULL) { latchInit = Ntk_LatchReadInitialInput(latch); /* Get the multi-valued function for each node*/ initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable); if (initMvfAig == NIL(MvfAig_Function_t)){ (void) fprintf(vis_stdout, "No multi-valued function for this node %s \n", Ntk_NodeReadName(latchInit)); return bAig_NULL; } latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable); if (latchMvfAig == NIL(MvfAig_Function_t)){ latchMvfAig = Bmc_NodeBuildMVF(network, latch); array_free(latchMvfAig); latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable); } resultOr = bAig_Zero; for(i=0; itype == Ctlsp_TRUE_c){ return mAig_One; } if (formula->type == Ctlsp_FALSE_c){ return mAig_Zero; } assert(Ctlsp_isPropositionalFormula(formula)); if (formula->type == Ctlsp_ID_c){ char *nodeNameString = Ctlsp_FormulaReadVariableName(formula); char *nodeValueString = Ctlsp_FormulaReadValueName(formula); 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 = MvfAig_FunctionReadComponent(tmpMvfAig, nodeValue); return bAig_GetCanonical(manager, result); } /* right can be mAig_NULL for unery operators, but left can't be mAig_Null */ left = BmcCreateMaigOfPropFormula(network, manager, formula->left); if (left == mAig_NULL){ return mAig_NULL; } right = BmcCreateMaigOfPropFormula(network, manager, formula->right); switch(formula->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; } /* BmcCreateMaigOfPropFormula */ /**Function******************************************************************** Synopsis [Build MDD for safety property in form of AG(p). Where p is either a propositional formula or a path formula contains only the temporal property X.] Description [Build MDD for a safety formula. Returns NIL if the conversion fails. The calling application is responsible for freeing the returned MDD.] SideEffects [] SeeAlso [Ctlsp_FormulaReadClass] ******************************************************************************/ mdd_t * BmcCreateMddOfSafetyProperty( Fsm_Fsm_t *fsm, Ctlsp_Formula_t *formula) { mdd_manager *manager = Ntk_NetworkReadMddManager(Fsm_FsmReadNetwork(fsm)); mdd_t *left, *right, *result; if (formula == NIL(Ctlsp_Formula_t)) { return NIL(mdd_t); } if (formula->type == Ctlsp_TRUE_c){ return bdd_one(manager); } if (formula->type == Ctlsp_FALSE_c){ return mdd_zero(manager); } #if 0 if (!Ctlsp_isPropositionalFormula(formula)) { (void) fprintf(vis_stderr, "bmc error: Only propositional formula can be converted to bdd \n"); fprintf(vis_stdout, "\nFormula: "); Ctlsp_FormulaPrint(vis_stdout, formula); fprintf(vis_stdout, "\n"); return NIL(mdd_t); } #endif /* Atomic proposition. */ if (formula->type == Ctlsp_ID_c){ return BmcModelCheckAtomicFormula(fsm, formula); } /* right can be NIL(mdd_t) for unery operators, but left can't be NIL(mdd_t) */ left = BmcCreateMddOfSafetyProperty(fsm, formula->left); if (left == NIL(mdd_t)){ return NIL(mdd_t); } right = BmcCreateMddOfSafetyProperty(fsm, formula->right); assert(right != NIL(mdd_t)); switch(formula->type) { case Ctlsp_NOT_c: result = mdd_not(left); break; case Ctlsp_OR_c: result = mdd_or(left, right, 1, 1); break; case Ctlsp_AND_c: result = mdd_and(left, right, 1, 1); break; case Ctlsp_THEN_c: result = mdd_or(left, right, 0, 1); break; case Ctlsp_EQ_c: result = mdd_xnor(left, right); break; case Ctlsp_XOR_c: result = mdd_xor(left, right); break; case Ctlsp_X_c: result = BmcFsmEvaluateX(fsm, left); break; default: /* return NIL(mdd_t) if the type is not supported */ return NIL(mdd_t); /* fail("Unexpected type"); */ } return result; } /**Function******************************************************************** Synopsis [Generate the CNF formula of a given function represented by AND/INVERTER graph] Description [Generate an array of clausese for a function represented in AND/INVERETER graph structure. the CNF formula of node to the output file specifies by cnfFile. It stores CNF index for each node in the cnfIndexTable. The generated CNF is in dimacs format. It is an error to call this function on a constand zero/one node.] SideEffects [] SeeAlso [] ******************************************************************************/ int BmcGenerateCnfFormulaForAigFunction( bAig_Manager_t *manager, bAigEdge_t node, int k, BmcCnfClauses_t *cnfClauses) { int leftIndex, rightIndex, nodeIndex; array_t *clause; assert( (node != bAig_One) && (node != bAig_Zero)); if(bAig_IsInverted(node)){ /* The generated clauses are in dimacs formate that uses negative number to indicate complement */ return -1*BmcGenerateCnfFormulaForAigFunction(manager, bAig_NonInvertedEdge(node), k, cnfClauses); } if (BmcCnfReadOrInsertNode(cnfClauses, bAig_NodeReadName(manager, node), k, &nodeIndex)){ return nodeIndex; } if (bAig_isVarNode(manager, node)){ return nodeIndex; } leftIndex = BmcGenerateCnfFormulaForAigFunction(manager, bAig_GetCanonical(manager, leftChild(node)), k, cnfClauses); rightIndex = BmcGenerateCnfFormulaForAigFunction(manager, bAig_GetCanonical(manager, rightChild(node)), k, cnfClauses); clause = array_alloc(int, 3); array_insert(int, clause, 0, -leftIndex ); array_insert(int, clause, 1, -rightIndex); array_insert(int, clause, 2, nodeIndex ); BmcCnfInsertClause(cnfClauses, clause); array_free(clause); clause = array_alloc(int, 2); array_insert(int, clause, 0, leftIndex); array_insert(int, clause, 1, -nodeIndex); BmcCnfInsertClause(cnfClauses, clause); array_free(clause); clause = array_alloc(int, 2); array_insert(int, clause, 0, rightIndex); array_insert(int, clause, 1, -nodeIndex); BmcCnfInsertClause(cnfClauses, clause); array_free(clause); return(nodeIndex); } /**Function******************************************************************** Synopsis [Generate CNF for bdd function] Description [ The function of each node f = var*thenChild + -var*elseChild var is the variable at this node. For each node there are four cases: - both childeren are constant -> do nothing. - the then child is constant 1 -> generate clauses for f = var + elseChild. - the else child is constant 0 -> generate clauses for f = var * thenChild. - the else child is constant 1 -> generate clauses for f = -var + thenChild. - else -> generate clauses for f = var*thenChild + -var*elseChild. ------------------------------------------------ function | clauses ------------------------------------------------ c = a*b | (-a + -b + c)*(a + -c)*(b + -c) c = a+b | (a + b + -c)*(-a + c)*(-b + c) f = c*a + -c*b | (-a + -c + f)*(a + -c + -f)* | (-b + c + f)*(b + c + -f) return the cnf index of the bdd function ] SideEffects [] SeeAlso [] ******************************************************************************/ int BmcGenerateCnfFormulaForBdd( bdd_t *bddFunction, int k, BmcCnfClauses_t *cnfClauses) { bdd_manager *bddManager = bdd_get_manager(bddFunction); bdd_node *node, *thenNode, *elseNode, *funcNode; int is_complemented; int nodeIndex=0, thenIndex, elseIndex; bdd_gen *gen; int varIndex, flag; array_t *tmpClause; st_table *bddToCnfIndexTable; bdd_t *currentBddNode; int cut = 5; if (bddFunction == NULL){ return 0; } funcNode = bdd_get_node(bddFunction, &is_complemented); if (bdd_is_constant(funcNode)){ if (is_complemented){ /* add an empty clause to indicate FALSE (un-satisfiable)*/ BmcAddEmptyClause(cnfClauses); } return 0; } if(bdd_size(bddFunction) <= cut){ return BmcGenerateCnfFormulaForBddOffSet(bddFunction, k, cnfClauses); } bddToCnfIndexTable = st_init_table(st_numcmp, st_numhash); foreach_bdd_node(bddFunction, gen, node){ if (bdd_is_constant(node)){ /* do nothing */ continue; } /* bdd_size() returns 1 if bdd is constant one. */ /* Use offset method to generate CNF if the size of the node <= cut (include the constant 1 node). */ /*#if 0*/ if(bdd_size(currentBddNode = bdd_construct_bdd_t(bddManager, bdd_regular(node))) <= cut){ if (bdd_size(currentBddNode) == cut){ nodeIndex = BmcGenerateCnfFormulaForBddOffSet(currentBddNode, k, cnfClauses); st_insert(bddToCnfIndexTable, (char *) (long) bdd_regular(node), (char *) (long)nodeIndex); continue; } continue; } /*#endif*/ varIndex = BmcGetCnfVarIndexForBddNode(bddManager, bdd_regular(node), k, cnfClauses); nodeIndex = varIndex; thenNode = bdd_bdd_T(node); elseNode = bdd_bdd_E(node); if (!((bdd_is_constant(thenNode)) && (bdd_is_constant(elseNode)))){ nodeIndex = cnfClauses->cnfGlobalIndex++; /* index of the function of this node */ if (bdd_is_constant(thenNode)){ /* the thenNode can be only constant one*/ flag = st_lookup_int(bddToCnfIndexTable, bdd_regular(elseNode), &elseIndex); assert(flag); /* test if the elseNode is complemented arc? */ if (bdd_is_complement(elseNode)){ elseIndex = -1*elseIndex; } BmcCnfGenerateClausesForOR(elseIndex, varIndex, nodeIndex, cnfClauses); } else if (bdd_is_constant(elseNode)){ /* one or zero */ flag = st_lookup_int(bddToCnfIndexTable, bdd_regular(thenNode), &thenIndex); assert(flag); /* test if the elseNode is complemented arc? */ if (bdd_is_complement(elseNode)){ /* Constant zero */ BmcCnfGenerateClausesForAND(thenIndex, varIndex, nodeIndex, cnfClauses); } else { /* Constant one */ BmcCnfGenerateClausesForOR(thenIndex, -varIndex, nodeIndex, cnfClauses); } } else { flag = st_lookup_int(bddToCnfIndexTable, bdd_regular(thenNode), &thenIndex); if(flag == 0){ thenIndex = BmcGenerateCnfFormulaForBddOffSet(bdd_construct_bdd_t(bddManager, bdd_regular(thenNode)), k, cnfClauses); st_insert(bddToCnfIndexTable, (char *) (long) bdd_regular(thenNode), (char *) (long)thenIndex); } /*assert(flag);*/ flag = st_lookup_int(bddToCnfIndexTable, bdd_regular(elseNode), &elseIndex); if(flag == 0){ elseIndex = BmcGenerateCnfFormulaForBddOffSet( bdd_construct_bdd_t(bddManager, bdd_regular(elseNode)), k, cnfClauses); st_insert(bddToCnfIndexTable, (char *) (long) bdd_regular(elseNode), (char *)(long) elseIndex); } /*assert(flag);*/ /* test if the elseNode is complemented arc? */ if (bdd_is_complement(elseNode)){ elseIndex = -1*elseIndex; } tmpClause = array_alloc(int, 3); assert(abs(thenIndex) <= cnfClauses->cnfGlobalIndex); assert(abs(varIndex) <= cnfClauses->cnfGlobalIndex); assert(abs(nodeIndex) <= cnfClauses->cnfGlobalIndex); array_insert(int, tmpClause, 0, -thenIndex); array_insert(int, tmpClause, 1, -varIndex); array_insert(int, tmpClause, 2, nodeIndex); BmcCnfInsertClause(cnfClauses, tmpClause); array_insert(int, tmpClause, 0, thenIndex); array_insert(int, tmpClause, 1, -varIndex); array_insert(int, tmpClause, 2, -nodeIndex); BmcCnfInsertClause(cnfClauses, tmpClause); array_insert(int, tmpClause, 0, -elseIndex); array_insert(int, tmpClause, 1, varIndex); array_insert(int, tmpClause, 2, nodeIndex); BmcCnfInsertClause(cnfClauses, tmpClause); array_insert(int, tmpClause, 0, elseIndex); array_insert(int, tmpClause, 1, varIndex); array_insert(int, tmpClause, 2, -nodeIndex); BmcCnfInsertClause(cnfClauses, tmpClause); array_free(tmpClause); } } st_insert(bddToCnfIndexTable, (char *) (long) bdd_regular(node), (char *) (long) nodeIndex); } /* foreach_bdd_node() */ st_free_table(bddToCnfIndexTable); return (is_complemented? -nodeIndex: nodeIndex); } /* BmcGenerateCnfFormulaForBdd() */ /**Function******************************************************************** Synopsis [Generate CNF for bdd function based on the off set of the bdd function] Description [Express the negation of bdd function in disjunctive normal form(DNF), and generate a clause for each disjunct in the DNF.] SideEffects [] SeeAlso [] ******************************************************************************/ int BmcGenerateCnfFormulaForBddOffSet( bdd_t *bddFunction, int k, BmcCnfClauses_t *cnfClauses) { bdd_manager *bddManager = bdd_get_manager(bddFunction); bdd_node *node, *funcNode; int is_complemented; bdd_gen *gen; int varIndex; array_t *tmpClause; array_t *cube; int i, value; bdd_t *newVar; if (bddFunction == NULL){ return 0; } /* Because the top node of bddFunction represents a variable in bddFunction, newVar is used to represent the function of bddFunction. Setting the cnfIndex of newVar to 1(0) is like setting the function of bddFunction to 1(0). */ newVar = bdd_create_variable(bddManager); bddFunction = bdd_xnor(newVar, bddFunction); funcNode = bdd_get_node(bddFunction, &is_complemented); if (bdd_is_constant(funcNode)){ if (is_complemented){ /* add an empty clause to indicate FALSE (un-satisfiable)*/ BmcAddEmptyClause(cnfClauses); } return 0; } bddFunction = bdd_not(bddFunction); foreach_bdd_cube(bddFunction, gen, cube){ tmpClause = array_alloc(int,0); arrayForEachItem(int, cube, i, value) { if (value != 2){ node = bdd_bdd_ith_var(bddManager, i); varIndex = BmcGetCnfVarIndexForBddNode(bddManager, bdd_regular(node), k, cnfClauses); if (value == 1){ varIndex = -varIndex; } array_insert_last(int, tmpClause, varIndex); } } BmcCnfInsertClause(cnfClauses, tmpClause); array_free(tmpClause); }/* foreach_bdd_cube() */ varIndex = BmcGetCnfVarIndexForBddNode(bddManager, bdd_regular(bdd_get_node(newVar, &is_complemented)), k, cnfClauses); return (varIndex); } /* BmcGenerateCnfFormulaForBddOffSet() */ #if 0 /**Function******************************************************************** Synopsis [Generate the CNF formula of a given function represented by AND/INVERTER graph] Description [Generate an array of clausese for a function represented in AND/INVERETER graph structure. the CNF formula of node to the output file specifies by cnfFile. It stores CNF index for each node in the cnfIndexTable. The generated CNF is in dimacs format. It is an error to call this function on a constand zero/one node.] SideEffects [] SeeAlso [] ******************************************************************************/ int BmcGenerateCnfForAigFunction( bAig_Manager_t *manager, Ntk_Network_t *network, bAigEdge_t node, int k, BmcCnfClauses_t *cnfClauses) { int leftIndex, rightIndex, nodeIndex; array_t *clause; if(bAig_IsInverted(node)){ /* The generated clauses are in dimacs formate that uses negative number to indicate complement */ return -1*BmcGenerateCnfFormulaForAigFunction(manager, bAig_NonInvertedEdge(node), k, cnfClauses); } { char *name = bAig_NodeReadName(manager, node); char *found = strchr(name, '='); if (found != NIL(char)){ int value = atoi(found+1); int length = found-name; char toName[length+1]; Ntk_Node_t *node; toName[length] = '\0'; strncpy(toName, name, length); node = Ntk_NetworkFindNodeByName(network, toName); if ((node != NIL( Ntk_Node_t)) && Ntk_NodeTestIsLatch(node)){ MvfAig_Function_t *tmpMvfAig; st_table *nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY); bAigEdge_t mAigNode; if (nodeToMvfAigTable == NIL(st_table)){ (void) fprintf(vis_stderr, "bmc error: please run build_partiton_maigs first"); return mAig_NULL; } if (k==0){ node = Ntk_LatchReadInitialInput(node); } else { node = Ntk_LatchReadDataInput(node); k--; } tmpMvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable); if (tmpMvfAig == NIL(MvfAig_Function_t)){ tmpMvfAig = Bmc_NodeBuildMVF(network, node); array_free(tmpMvfAig); tmpMvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable); } mAigNode = MvfAig_FunctionReadComponent(tmpMvfAig, value); BmcGenerateCnfForAigFunction(manager, network, mAigNode, k, cnfClauses); } } } if (BmcCnfReadOrInsertNode(cnfClauses, bAig_NodeReadName(manager, node), k, &nodeIndex)){ return nodeIndex; } if (bAig_isVarNode(manager, node)){ return nodeIndex; } leftIndex = BmcGenerateCnfForAigFunction(manager, network, leftChild(node), k, cnfClauses); rightIndex = BmcGenerateCnfForAigFunction(manager, network, rightChild(node), k, cnfClauses); clause = array_alloc(int, 3); array_insert(int, clause, 0, -leftIndex ); array_insert(int, clause, 1, -rightIndex); array_insert(int, clause, 2, nodeIndex ); BmcCnfInsertClause(cnfClauses, clause); array_free(clause); clause = array_alloc(int, 2); array_insert(int, clause, 0, leftIndex); array_insert(int, clause, 1, -nodeIndex); BmcCnfInsertClause(cnfClauses, clause); array_free(clause); clause = array_alloc(int, 2); array_insert(int, clause, 0, rightIndex); array_insert(int, clause, 1, -nodeIndex); BmcCnfInsertClause(cnfClauses, clause); array_free(clause); return(nodeIndex); } #endif /**Function******************************************************************** Synopsis [ c = a <-> b = (a=0)*(b=0) + (a=1)*(b=1) .... For a given term (a=i)*(b=i), if either is Zero, don't generate clauses for this term. if both are One, don't generate clauses for c. ] SideEffects [] ******************************************************************************/ void BmcGenerateClausesFromStateTostate( bAig_Manager_t *manager, bAigEdge_t *fromAigArray, bAigEdge_t *toAigArray, int mvfSize, int fromState, int toState, BmcCnfClauses_t *cnfClauses, int outIndex) { array_t *clause, *tmpclause; int toIndex, fromIndex, cnfIndex; int i; /* used to turn off the warning messages: might be left uninitialized. We are sure that these two variables will not be used uninitialized. */ toIndex =0; fromIndex = 0; for(i=0; i< mvfSize; i++){ if ((fromAigArray[i] == bAig_One) && (toAigArray[i] == bAig_One)){ return; /* the clause is always true */ } } clause = array_alloc(int, 0); for(i=0; i< mvfSize; i++){ if ((fromAigArray[i] != bAig_Zero) && (toAigArray[i] != bAig_Zero)){ if (toAigArray[i] != bAig_One){ /* to State */ toIndex = BmcGenerateCnfFormulaForAigFunction(manager,toAigArray[i], toState,cnfClauses); } if (fromAigArray[i] != bAig_One){ /* from State */ fromIndex = BmcGenerateCnfFormulaForAigFunction(manager, fromAigArray[i], fromState, cnfClauses); } /* Create new var for the output of this node. We don't create variable for this node, we only use its index number. */ cnfIndex = cnfClauses->cnfGlobalIndex++; /* index of the output of the OR of T(from, to) */ assert(abs(cnfIndex) <= cnfClauses->cnfGlobalIndex); assert(abs(fromIndex) <= cnfClauses->cnfGlobalIndex); assert(abs(toIndex) <= cnfClauses->cnfGlobalIndex); if (toAigArray[i] == bAig_One){ tmpclause = array_alloc(int, 2); array_insert(int, tmpclause, 0, -fromIndex); array_insert(int, tmpclause, 1, cnfIndex); BmcCnfInsertClause(cnfClauses, tmpclause); array_free(tmpclause); tmpclause = array_alloc(int, 2); array_insert(int, tmpclause, 0, fromIndex); array_insert(int, tmpclause, 1, -cnfIndex); BmcCnfInsertClause(cnfClauses, tmpclause); array_free(tmpclause); } else if (fromAigArray[i] == bAig_One){ tmpclause = array_alloc(int, 2); array_insert(int, tmpclause, 0, -toIndex); array_insert(int, tmpclause, 1, cnfIndex); BmcCnfInsertClause(cnfClauses, tmpclause); array_free(tmpclause); tmpclause = array_alloc(int, 2); array_insert(int, tmpclause, 0, toIndex); array_insert(int, tmpclause, 1, -cnfIndex); BmcCnfInsertClause(cnfClauses, tmpclause); array_free(tmpclause); } else { tmpclause = array_alloc(int, 3); array_insert(int, tmpclause, 0, -toIndex); array_insert(int, tmpclause, 1, -fromIndex); array_insert(int, tmpclause, 2, cnfIndex); BmcCnfInsertClause(cnfClauses, tmpclause); array_free(tmpclause); tmpclause = array_alloc(int, 2); array_insert(int, tmpclause, 0, toIndex); array_insert(int, tmpclause, 1, -cnfIndex); BmcCnfInsertClause(cnfClauses, tmpclause); array_free(tmpclause); tmpclause = array_alloc(int, 2); array_insert(int, tmpclause, 0, fromIndex); array_insert(int, tmpclause, 1, -cnfIndex); BmcCnfInsertClause(cnfClauses, tmpclause); array_free(tmpclause); } array_insert_last(int, clause, cnfIndex); } /* if */ } /* for i loop */ if (outIndex != 0 ){ array_insert_last(int, clause, -outIndex); } BmcCnfInsertClause(cnfClauses, clause); array_free(clause); return; } /**Function******************************************************************** Synopsis [Write the set of clauses in diamacs format to the output file.] SideEffects [] ******************************************************************************/ void BmcWriteClauses( mAig_Manager_t *maigManager, FILE *cnfFile, BmcCnfClauses_t *cnfClauses, BmcOption_t *options) { st_generator *stGen; char *name; int cnfIndex, i, k; if (options->verbosityLevel == BmcVerbosityMax_c) { fprintf(vis_stdout, "Number of Variables = %d Number of Clauses = %d\n", cnfClauses->cnfGlobalIndex-1, cnfClauses->noOfClauses); } st_foreach_item_int(cnfClauses->cnfIndexTable, stGen, &name, &cnfIndex) { fprintf(cnfFile, "c %s %d\n",name, cnfIndex); } (void) fprintf(cnfFile, "p cnf %d %d\n", cnfClauses->cnfGlobalIndex-1, cnfClauses->noOfClauses); if (cnfClauses->clauseArray != NIL(array_t)) { for (i = 0; i < cnfClauses->nextIndex; i++) { k = array_fetch(int, cnfClauses->clauseArray, i); (void) fprintf(cnfFile, "%d%c", k, (k == 0) ? '\n' : ' '); } } return; } /**Function******************************************************************** Synopsis [Check the satisfiability of CNF formula written in file] Description [Run SAT solver on input file] SideEffects [] ******************************************************************************/ array_t * BmcCheckSAT(BmcOption_t *options) { array_t *result = NIL(array_t); if(options->satSolver == cusp){ result = BmcCallCusp(options); } if(options->satSolver == CirCUs){ result = BmcCallCirCUs(options); } /* Adjust alarm if timeout in effect. This is necessary because the * alarm may have gone off while the SAT solver is running. Since * the CPU time of a child process is charged to the parent only when * the child terminates, the SIGALRM handler assumes that more time * is left than it is in reality. We could do this adjustment right * after calling the SAT solver, but we prefer to give ourselves the * extra time to report the result even if this means using more time * than we are allotted. */ if (options->timeOutPeriod > 0) { int residualTime = options->timeOutPeriod - (util_cpu_ctime() - options->startTime) / 1000; /* Make sure we do not cancel the alarm if no time is left. */ if (residualTime <= 0) { residualTime = 1; } (void) alarm(residualTime); } return result; } /**Function******************************************************************** Synopsis [Check the satisfiability of CNF formula written in file] Description [Run CirCUs on input file] SideEffects [] ******************************************************************************/ array_t * BmcCallCirCUs( BmcOption_t *options) { satOption_t *satOption; array_t *result = NIL(array_t); satManager_t *cm; int maxSize; satOption = sat_InitOption(); satOption->verbose = options->verbosityLevel; satOption->verbose = 0; cm = sat_InitManager(0); cm->comment = ALLOC(char, 2); cm->comment[0] = ' '; cm->comment[1] = '\0'; cm->stdOut = stdout; cm->stdErr = stderr; cm->option = satOption; cm->each = sat_InitStatistics(); cm->unitLits = sat_ArrayAlloc(16); cm->pureLits = sat_ArrayAlloc(16); maxSize = 10000 << (bAigNodeSize-4); cm->nodesArray = ALLOC(bAigEdge_t, maxSize); cm->maxNodesArraySize = maxSize; cm->nodesArraySize = bAigNodeSize; sat_AllocLiteralsDB(cm); sat_ReadCNF(cm, options->satInFile); if (options->verbosityLevel == BmcVerbosityMax_c) { (void)fprintf(vis_stdout,"Calling SAT solver (CirCUs) ..."); (void) fflush(vis_stdout); } sat_Main(cm); if (options->verbosityLevel == BmcVerbosityMax_c) { (void) fprintf(vis_stdout," done "); (void) fprintf(vis_stdout, "(%g s)\n", cm->each->satTime); } if(cm->status == SAT_UNSAT) { if (options->verbosityLevel != BmcVerbosityNone_c){ (void) fprintf(vis_stdout, "# SAT: Counterexample not found\n"); } fflush(cm->stdOut); } else if(cm->status == SAT_SAT) { if (options->verbosityLevel != BmcVerbosityNone_c){ (void) fprintf(vis_stdout, "# SAT: Counterexample found\n"); } if (options->verbosityLevel == BmcVerbosityMax_c){ sat_ReportStatistics(cm, cm->each); } fflush(cm->stdOut); result = array_alloc(int, 0); { int i, size, value; size = cm->initNumVariables * bAigNodeSize; for(i=bAigNodeSize; i<=size; i+=bAigNodeSize) { value = SATvalue(i); if(value == 1) { array_insert_last(int, result, SATnodeID(i)); } else if(value == 0) { array_insert_last(int, result, -(SATnodeID(i))); } } } } //Bing: To avoid SEVERE memory leakage FREE(cm->nodesArray); sat_FreeManager(cm); return result; } /* BmcCallCirCUs */ /**Function******************************************************************** Synopsis [Check the satisfiability of CNF formula written in file] Description [Run external solver on input file] SideEffects [] ******************************************************************************/ array_t * BmcCallCusp(BmcOption_t *options) { FILE *fp; static char parseBuffer[1024]; int satStatus; char line[MAX_LENGTH]; int num = 0; array_t *result = NIL(array_t); char *tmpStr, *tmpStr1, *tmpStr2; long solverStart; int satTimeOutPeriod = 0; strcpy(parseBuffer,"cusp -distill -velim -cnf "); options->satSolverError = FALSE; /* assume no error*/ if (options->timeOutPeriod > 0) { /* Compute the residual CPU time and subtract a little time to give vis a chance to clean up before its own time out expires. */ satTimeOutPeriod = options->timeOutPeriod - 1 - (util_cpu_ctime() - options->startTime) / 1000; if (satTimeOutPeriod <= 0){ /* no time left to run SAT solver*/ options->satSolverError=TRUE; return NIL(array_t); } tmpStr2 = util_inttostr(satTimeOutPeriod); tmpStr1 = util_strcat3(options->satInFile," -t ", tmpStr2); tmpStr = util_strcat3(tmpStr1, " >", options->satOutFile); FREE(tmpStr1); FREE(tmpStr2); } else { tmpStr = util_strcat3(options->satInFile, " >", options->satOutFile); } strcat(parseBuffer, tmpStr); FREE(tmpStr); if (options->verbosityLevel == BmcVerbosityMax_c) { (void)fprintf(vis_stdout,"Calling SAT solver (cusp) ..."); (void) fflush(vis_stdout); solverStart = util_cpu_ctime(); } else { /* to remove uninitialized variables warning */ solverStart = 0; } /* Call Sat Solver*/ satStatus = system(parseBuffer); if (satStatus != 0){ (void) fprintf(vis_stderr, "Can't run cusp. It may not be in your path. Status = %d\n", satStatus); options->satSolverError = TRUE; return NIL(array_t); } if (options->verbosityLevel == BmcVerbosityMax_c) { (void) fprintf(vis_stdout," done "); (void) fprintf(vis_stdout, "(%g s)\n", (double) (util_cpu_ctime() - solverStart)/1000.0); } fp = Cmd_FileOpen(options->satOutFile, "r", NIL(char *), 0); if (fp == NIL(FILE)) { (void) fprintf(vis_stderr, "** bmc error: Cannot open the file %s\n", options->satOutFile); options->satSolverError = TRUE; return NIL(array_t); } /* Skip the lines until the result */ while(1) { if (fgets(line, MAX_LENGTH - 1, fp) == NULL) break; if(strstr(line,"UNSATISFIABLE") || strstr(line,"SATISFIABLE") || strstr(line,"MEMOUT") || strstr(line,"TIMEOUT")) break; } if(strstr(line,"UNSATISFIABLE") != NIL(char)) { if (options->verbosityLevel != BmcVerbosityNone_c){ (void) fprintf(vis_stdout, "# SAT: Counterexample not found\n"); } } else if(strstr(line,"SATISFIABLE") != NIL(char)) { if (options->verbosityLevel != BmcVerbosityNone_c){ (void) fprintf(vis_stdout, "# SAT: Counterexample found\n"); } /* Skip the initial v of the result line */ result = array_alloc(int, 0); while (fgets(line, MAX_LENGTH - 1, fp) != NULL) { char *word; if (line[0] != 'v') { (void) fprintf(vis_stderr, "** bmc error: Cannot find assignment in file %s\n", options->satOutFile); options->satSolverError = TRUE; return NIL(array_t); } word = strtok(&(line[1])," \n"); while (word != NIL(char)) { num = atoi(word); if (num == 0) break; array_insert_last(int, result, num); word = strtok(NIL(char)," \n"); } if (num == 0) break; } } else if(strstr(line,"MEMOUT") != NIL(char)) { (void) fprintf(vis_stdout,"# SAT: SAT Solver Memory out\n"); options->satSolverError = TRUE; } else if(strstr(line,"TIMEOUT") != NIL(char)) { (void) fprintf(vis_stdout, "# SAT: SAT Solver Time out occurred after %d seconds.\n", satTimeOutPeriod); options->satSolverError = TRUE; } else { (void) fprintf(vis_stdout, "# SAT: SAT Solver failed, try again\n"); options->satSolverError = TRUE; } (void) fflush(vis_stdout); (void) fclose(fp); return result; } /* BmcCallCusp */ /**Function******************************************************************** Synopsis [Print CounterExample.] SideEffects [Print a counterexample that was returned from the SAT solver in term of an array of integer "result". The counterexample starts from state 0 and of lenght eqaual to "length". If loopClause is not empty, this function print a loopback from the last state to a state in loopClause that exist in "result".] ******************************************************************************/ void BmcPrintCounterExample( Ntk_Network_t *network, st_table *nodeToMvfAigTable, BmcCnfClauses_t *cnfClauses, array_t *result, int length, st_table *CoiTable, BmcOption_t *options, array_t *loopClause) { mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network); lsGen gen; st_generator *stGen; Ntk_Node_t *node; int k; array_t *latches = array_alloc(int, 0); int *prevValueLatches; array_t *inputs = array_alloc(int, 0); int *prevValueInputs; int tmp; int loop; st_table *resultTable = st_init_table(st_numcmp, st_numhash); /* Initialize resultTable from the result to speed up the search in the result array. */ for(k=0; k< array_n(result); k++){ st_insert(resultTable, (char *) (long) array_fetch(int, result, k), (char *) 0); } /* sort latches by name */ st_foreach_item(CoiTable, stGen, &node, NULL) { array_insert_last(char*, latches, Ntk_NodeReadName(node)); } array_sort(latches, nameCompare); /* Use to store the last value of each latch. If the current value of a latch differs from its corresponding value in this array, we will print the new values. */ prevValueLatches = ALLOC(int, array_n(latches)); prevValueInputs = 0; if(options->printInputs == TRUE){ /* sort inputs by name */ Ntk_NetworkForEachInput(network, gen, node){ array_insert_last(char*, inputs, Ntk_NodeReadName(node)); } array_sort(inputs, nameCompare); prevValueInputs = ALLOC(int, array_n(inputs)); } loop = -1; /* no loop back */ if(loopClause != NIL(array_t)){ for(k=0; k < array_n(loopClause); k++){ /* if (searchArray(result, array_fetch(int, loopClause, k)) > -1){ */ if (st_lookup_int(resultTable, (char *)(long)array_fetch(int, loopClause, k), &tmp)){ loop = k; break; } } } /* Ntk_NetworkForEachPrimaryOutput(network, gen, node){ array_insert_last(char*, outputs, Ntk_NodeReadName(node)); } array_sort(outputs, nameCompare); */ for (k=0; k<= length; k++){ if (k == 0){ (void) fprintf(vis_stdout, "\n--State %d:\n", k); } else { (void) fprintf(vis_stdout, "\n--Goes to state %d:\n", k); } /* Print the current values of the latches if they are different form their previous values. */ printValue(manager, network, nodeToMvfAigTable, cnfClauses, latches, resultTable, k, prevValueLatches); #if 0 (void) fprintf(vis_stdout, "--Primary output:\n"); printValue(manager, network, nodeToMvfAigTable, cnfClauses, outputs, result, k); #endif if((options->printInputs == TRUE) && (k !=0)) { (void) fprintf(vis_stdout, "--On input:\n"); printValue(manager, network, nodeToMvfAigTable, cnfClauses, inputs, resultTable, k-1, prevValueInputs); } } /* for k loop */ if(loop != -1){ (void) fprintf(vis_stdout, "\n--Goes back to state %d:\n", loop); printValue(manager, network, nodeToMvfAigTable, cnfClauses, latches, resultTable, loop, prevValueLatches); if((options->printInputs == TRUE)) { (void) fprintf(vis_stdout, "--On input:\n"); printValue(manager, network, nodeToMvfAigTable, cnfClauses, inputs, resultTable, length, prevValueInputs); } } array_free(latches); FREE(prevValueLatches); if(options->printInputs == TRUE){ array_free(inputs); FREE(prevValueInputs); } st_free_table(resultTable); return; } /* BmcPrintCounterExample() */ /**Function******************************************************************** Synopsis [Print CounterExample in Aiger format.] SideEffects [Print a counterexample that was returned from the SAT solver in term of an array of integer "result". The counterexample starts from state 0 and of lenght eqaual to "length". If loopClause is not empty, this function print a loopback from the last state to a state in loopClause that exist in "result".] ******************************************************************************/ void BmcPrintCounterExampleAiger( Ntk_Network_t *network, st_table *nodeToMvfAigTable, BmcCnfClauses_t *cnfClauses, array_t *result, int length, st_table *CoiTable, BmcOption_t *options, array_t *loopClause) { mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network); lsGen gen; st_generator *stGen; Ntk_Node_t *node; int k; array_t *latches = array_alloc(int, 0); int *prevValueLatches; array_t *inputs = array_alloc(int, 0); array_t *outputs = array_alloc(int, 0); int *prevValueInputs; int *prevValueOutputs; int tmp; int loop; st_table *resultTable = st_init_table(st_numcmp, st_numhash); char *nodeName; /* Initialize resultTable from the result to speed up the search in the result array. */ for(k=0; k< array_n(result); k++){ st_insert(resultTable, (char *) (long) array_fetch(int, result, k), (char *) 0); } /* sort latches by name */ st_foreach_item(CoiTable, stGen, &node, NULL) { array_insert_last(char*, latches, Ntk_NodeReadName(node)); } /* Use to store the last value of each latch. If the current value of a latch differs from its corresponding value in this array, we will print the new values. */ /* the file generation needs to be removed for final vis release */ FILE *order = Cmd_FileOpen("inputOrder.txt", "w", NIL(char *), 0); for (k=0; k< array_n(latches); k++) { nodeName = array_fetch(char *, latches, k); if((nodeName[0] == '$') && (nodeName[1] == '_')) { fprintf(order, "%s\n", &nodeName[2]); } } fclose(order); prevValueLatches = ALLOC(int, array_n(latches)); Ntk_NetworkForEachInput(network, gen, node){ array_insert_last(char*, inputs, Ntk_NodeReadName(node)); } prevValueInputs = ALLOC(int, array_n(inputs)); loop = -1; /* no loop back */ if(loopClause != NIL(array_t)){ for(k=0; k < array_n(loopClause); k++){ /* if (searchArray(result, array_fetch(int, loopClause, k)) > -1){ */ if (st_lookup_int(resultTable, (char *)(long)array_fetch(int, loopClause, k), &tmp)){ loop = k; break; } } } Ntk_NetworkForEachPrimaryOutput(network, gen, node){ array_insert_last(char*, outputs, Ntk_NodeReadName(node)); } prevValueOutputs = ALLOC(int, array_n(outputs)); for (k=0; k< length; k++){ /* This will print latches whose name doesn't start with $_. The latches whose name starts with $_ are latches added to the model by the aigtoblif translator. */ printValueAiger(manager, network, nodeToMvfAigTable, cnfClauses, latches, resultTable, k, prevValueLatches); fprintf(vis_stdout, " "); #if 0 (void) fprintf(vis_stdout, "--Primary output:\n"); printValue(manager, network, nodeToMvfAigTable, cnfClauses, outputs, result, k); #endif if((loop<0)||(kprintInputs == TRUE){ array_free(inputs); FREE(prevValueInputs); } st_free_table(resultTable); return; } /* BmcPrintCounterExampleAiger() */ /**Function******************************************************************** Synopsis [Print CounterExample.] SideEffects [Print a counterexample that was returned from the SAT solver in term of an array of integer "result". The counterexample starts from state 0 and of lenght eqaual to "length". If loopClause is not empty, this function print a loopback from the last state to a state in loopClause that exist in "result".] ******************************************************************************/ void BmcAutPrintCounterExample( Ntk_Network_t *network, Ltl_Automaton_t *automaton, st_table *nodeToMvfAigTable, BmcCnfClauses_t *cnfClauses, array_t *result, int length, st_table *CoiTable, BmcOption_t *options, array_t *loopClause) { mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network); lsGen gen; st_generator *stGen; Ntk_Node_t *node; int k; array_t *latches = array_alloc(int, 0); int *prevValueLatches; array_t *inputs = array_alloc(int, 0); int *prevValueInputs; int tmp; int loop; st_table *resultTable = st_init_table(st_numcmp, st_numhash); /* Initialize resultTable from the result to speed up the search in the result array. */ for(k=0; k< array_n(result); k++){ st_insert(resultTable, (char *) (long) array_fetch(int, result, k), (char *) 0); } /* sort latches by name */ st_foreach_item(CoiTable, stGen, &node, NULL) { array_insert_last(char*, latches, Ntk_NodeReadName(node)); } array_sort(latches, nameCompare); /* Use to store the last value of each latch. If the current value of a latch differs from its corresponding value in this array, we will print the new values. */ prevValueLatches = ALLOC(int, array_n(latches)); prevValueInputs = 0; if(options->printInputs == TRUE){ /* sort inputs by name */ Ntk_NetworkForEachInput(network, gen, node){ array_insert_last(char*, inputs, Ntk_NodeReadName(node)); } array_sort(inputs, nameCompare); prevValueInputs = ALLOC(int, array_n(inputs)); } loop = -1; /* no loop back */ if(loopClause != NIL(array_t)){ for(k=0; k < array_n(loopClause); k++){ /* if (searchArray(result, array_fetch(int, loopClause, k)) > -1){ */ if (st_lookup_int(resultTable, (char *)(long)array_fetch(int, loopClause, k), &tmp)){ loop = k; break; } } } /* Ntk_NetworkForEachPrimaryOutput(network, gen, node){ array_insert_last(char*, outputs, Ntk_NodeReadName(node)); } array_sort(outputs, nameCompare); */ for (k=0; k<= length; k++){ if (k == 0){ (void) fprintf(vis_stdout, "\n--State %d:\n", k); } else { (void) fprintf(vis_stdout, "\n--Goes to state %d:\n", k); } /* Print the current values of the latches if they are different form their previous values. */ printValue(manager, network, nodeToMvfAigTable, cnfClauses, latches, resultTable, k, prevValueLatches); { lsGen lsGen; vertex_t *vtx; Ltl_AutomatonNode_t *state; int stateIndex; bdd_node *node; int is_complemented; foreach_vertex(automaton->G, lsGen, vtx) { state = (Ltl_AutomatonNode_t *) vtx->user_data; node = bdd_get_node(state->Encode, &is_complemented); stateIndex = state->cnfIndex[k]; if (st_lookup_int(resultTable, (char *)(long)stateIndex, &tmp)){ (void) fprintf(vis_stdout,"n%d \n", state->index); } } } #if 0 (void) fprintf(vis_stdout, "--Primary output:\n"); printValue(manager, network, nodeToMvfAigTable, cnfClauses, outputs, result, k); #endif if((options->printInputs == TRUE) && (k !=0)) { (void) fprintf(vis_stdout, "--On input:\n"); printValue(manager, network, nodeToMvfAigTable, cnfClauses, inputs, resultTable, k-1, prevValueInputs); } } /* for k loop */ if(loop != -1){ (void) fprintf(vis_stdout, "\n--Goes back to state %d:\n", loop); printValue(manager, network, nodeToMvfAigTable, cnfClauses, latches, resultTable, loop, prevValueLatches); if((options->printInputs == TRUE)) { (void) fprintf(vis_stdout, "--On input:\n"); printValue(manager, network, nodeToMvfAigTable, cnfClauses, inputs, resultTable, length, prevValueInputs); } } array_free(latches); FREE(prevValueLatches); if(options->printInputs == TRUE){ array_free(inputs); FREE(prevValueInputs); } st_free_table(resultTable); return; } /* BmcPrintCounterExample() */ /**Function******************************************************************** Synopsis [Generate CNF formula for a path from state 'from' to state 'to'] Description [Unfold the transition relation 'k' states (k = to-from +1), and generate clauses for each state. For a multi-valued latch of 4 vlaues. Two binary variables are used to rpresent X, x1 and x0. For this latch, there exist three multi-valued functions. One for the binary reoresentation of the variable. For example the second entry of the mvf = 1, iff ~x1 and x0. The second mfv is for the data input of the latch. If the And/Inv graph attached to an entry of this mvf equal to 1, X equal to the binary representation corresponding to this entry. For example, if the And/ INV graph attached to the first entry =1, then X = ~x1 & ~x0. To generate the CNF to the transition relation, first generate CNF to next state varaible using mvf of the latch. Then, generate CNF for latch data input using current state variavles. Finaly, generate CNF for the AND of these two MVF. This for every entry of the MVF. Then OR the results. The third MVF is for the initial value of the latch. It is treat the same as the latch data input except if the initial value is constant. The initialState value may be either BMC_INITIAL_STATES to generate the clause for the intial states. BMC_NO_INITIAL_STATES otherwise. ] SideEffects [] SeeAlso [] ******************************************************************************/ void BmcCnfGenerateClausesForPath( Ntk_Network_t *network, int from, int to, int initialState, BmcCnfClauses_t *cnfClauses, st_table *nodeToMvfAigTable, st_table *CoiTable) { mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network); st_generator *stGen; Ntk_Node_t *latch, *latchData, *latchInit; MvfAig_Function_t *initMvfAig, *dataMvfAig, *latchMvfAig; bAigEdge_t *initBAig, *latchBAig, *dataBAig; int i, k, mvfSize; st_foreach_item(CoiTable, stGen, &latch, NULL) { latchInit = Ntk_LatchReadInitialInput(latch); latchData = Ntk_LatchReadDataInput(latch); /* Get the multi-valued function for each node*/ initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable); if (initMvfAig == NIL(MvfAig_Function_t)){ (void) fprintf(vis_stdout, "No multi-valued function for this node %s \n", Ntk_NodeReadName(latchInit)); return; } dataMvfAig = Bmc_ReadMvfAig(latchData, nodeToMvfAigTable); if (dataMvfAig == NIL(MvfAig_Function_t)){ (void) fprintf(vis_stdout, "No multi-valued function for this node %s \n", Ntk_NodeReadName(latchData)); return; } latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable); if (latchMvfAig == NIL(MvfAig_Function_t)){ latchMvfAig = Bmc_NodeBuildMVF(network, latch); array_free(latchMvfAig); latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable); } mvfSize = array_n(initMvfAig); initBAig = ALLOC(bAigEdge_t, mvfSize); dataBAig = ALLOC(bAigEdge_t, mvfSize); latchBAig = ALLOC(bAigEdge_t, mvfSize); for(i=0; i< mvfSize; i++){ dataBAig[i] = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(dataMvfAig, i)); latchBAig[i] = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(latchMvfAig, i)); initBAig[i] = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(initMvfAig, i)); } /* if (from == 0){ */ if (initialState == BMC_INITIAL_STATES){ /* Generate the CNF for the initial state of the latch */ BmcGenerateClausesFromStateTostate(manager, initBAig, latchBAig, mvfSize, -1, 0, cnfClauses, 0); } /* Generate the CNF for the transition functions */ for (k=from; k < to; k++){ BmcGenerateClausesFromStateTostate(manager, dataBAig, latchBAig, mvfSize, k, k+1, cnfClauses, 0); } /* for k state loop */ FREE(initBAig); FREE(dataBAig); FREE(latchBAig); }/* For each latch loop*/ return; } /**Function******************************************************************** Synopsis [Generate CNF formula for a loop-free path] Description [This function generates CNF formula for a loop-free path from state fromState to state toState. A loop free path is a path from a state S0 to state Sn such that every state in the path is distinct. i.e for all states in the path Si != Sj for 0<= i < j <= n. The initialState value may be either BMC_INITIAL_STATES to generate the clause for the intial states. BMC_NO_INITIAL_STATES otherwise. ] SideEffects [] SeeAlso [] ******************************************************************************/ void BmcCnfGenerateClausesForLoopFreePath( Ntk_Network_t *network, int fromState, int toState, int initialState, BmcCnfClauses_t *cnfClauses, st_table *nodeToMvfAigTable, st_table *CoiTable) { int state; /* Generate clauses for a path from fromState to toState. */ BmcCnfGenerateClausesForPath(network, fromState, toState, initialState, cnfClauses, nodeToMvfAigTable, CoiTable); /* Restrict the above path to be loop-free path. */ /* for(state=0; state< toState; state++){ */ /* Don't include the last state because we know it is not equal any of the previous states. The property fails at this state, and true at all other states. */ /* for(state=1; state < toState; state++){ */ for(state= fromState + 1; state <= toState; state++){ BmcCnfGenerateClausesForNoLoopToAnyPreviouseStates(network, fromState, state, cnfClauses, nodeToMvfAigTable, CoiTable); } return; } /**Function******************************************************************** Synopsis [Generate Clauses for no loop from last state to any of the previouse states] Description [Generate Clauses for no loop from last state (toState) to any of the previous states starting from fromState. It generates the CNF clauses such that the last state of the path is not equal to any of the path previous states. ] SideEffects [] SeeAlso [] ******************************************************************************/ void BmcCnfGenerateClausesForNoLoopToAnyPreviouseStates( Ntk_Network_t *network, int fromState, int toState, BmcCnfClauses_t *cnfClauses, st_table *nodeToMvfAigTable, st_table *CoiTable) { mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network); st_generator *stGen; Ntk_Node_t *latch; MvfAig_Function_t *latchMvfAig; bAigEdge_t *latchBAig; array_t *orClause; int lastIndex, prevIndex, andIndex1, andIndex2; int i, k, mvfSize; /* Generates the clauses to check if the toState is not equal to any previouse states starting from fromState. Assume there are two state varaibles a and b. To check if Si != Sj, we must generate clauses for the formula ( ai != aj + bi != bj). */ for(k=fromState; k < toState; k++){ orClause = array_alloc(int,0); st_foreach_item(CoiTable, stGen, &latch, NULL) { latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable); if (latchMvfAig == NIL(MvfAig_Function_t)){ latchMvfAig = Bmc_NodeBuildMVF(network, latch); array_free(latchMvfAig); latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable); } mvfSize = array_n(latchMvfAig); latchBAig = ALLOC(bAigEdge_t, mvfSize); for(i=0; i< mvfSize; i++){ latchBAig[i] = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(latchMvfAig, i)); } for (i=0; i< mvfSize; i++){ prevIndex = BmcGenerateCnfFormulaForAigFunction(manager, latchBAig[i], k ,cnfClauses); lastIndex = BmcGenerateCnfFormulaForAigFunction(manager, latchBAig[i], toState ,cnfClauses); andIndex1 = cnfClauses->cnfGlobalIndex++; BmcCnfGenerateClausesForAND(prevIndex, -lastIndex, andIndex1, cnfClauses); andIndex2 = cnfClauses->cnfGlobalIndex++; BmcCnfGenerateClausesForAND(-prevIndex, lastIndex, andIndex2, cnfClauses); array_insert_last(int, orClause, andIndex1); array_insert_last(int, orClause, andIndex2); } FREE(latchBAig); }/* For each latch loop*/ BmcCnfInsertClause(cnfClauses, orClause); array_free(orClause); } /* foreach k*/ return; } /**Function******************************************************************** Synopsis [Generate Clauses for last state equal to any of the previouse states] Description [ Change it! Generate Clauses for no loop from last state (toState) to any of the previous states starting from fromState. It generates the CNF clauses such that the last state of the path is not equal to any of the path previous states. ] SideEffects [] SeeAlso [] ******************************************************************************/ void BmcCnfGenerateClausesForLoopToAnyPreviouseStates( Ntk_Network_t *network, int fromState, int toState, BmcCnfClauses_t *cnfClauses, st_table *nodeToMvfAigTable, st_table *CoiTable) { mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network); st_generator *stGen; Ntk_Node_t *latch; MvfAig_Function_t *latchMvfAig; bAigEdge_t *latchBAig; array_t *orClause; int lastIndex, prevIndex, andIndex1, andIndex2; int i, k, mvfSize; /* Generates the clauses to check if the toState is not equal to any previouse states starting from fromState. Assume there are two state varaibles a and b. To check if Si != Sj, we must generate clauses for the formula ( ai != aj + bi != bj). */ for(k=fromState; k < toState; k++){ orClause = array_alloc(int,0); st_foreach_item(CoiTable, stGen, &latch, NULL) { latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable); if (latchMvfAig == NIL(MvfAig_Function_t)){ latchMvfAig = Bmc_NodeBuildMVF(network, latch); array_free(latchMvfAig); latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable); } mvfSize = array_n(latchMvfAig); latchBAig = ALLOC(bAigEdge_t, mvfSize); for(i=0; i< mvfSize; i++){ latchBAig[i] = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(latchMvfAig, i)); } for (i=0; i< mvfSize; i++){ prevIndex = BmcGenerateCnfFormulaForAigFunction(manager, latchBAig[i], k ,cnfClauses); lastIndex = BmcGenerateCnfFormulaForAigFunction(manager, latchBAig[i], toState ,cnfClauses); andIndex1 = cnfClauses->cnfGlobalIndex++; BmcCnfGenerateClausesForAND(prevIndex, lastIndex, andIndex1, cnfClauses); andIndex2 = cnfClauses->cnfGlobalIndex++; BmcCnfGenerateClausesForAND(-prevIndex, -lastIndex, andIndex2, cnfClauses); array_insert_last(int, orClause, andIndex1); array_insert_last(int, orClause, andIndex2); } FREE(latchBAig); }/* For each latch loop*/ BmcCnfInsertClause(cnfClauses, orClause); array_free(orClause); } /* foreach k*/ return; } /**Function******************************************************************** Synopsis [Generate CNF formula for a path from state 'from' to state 'to'] Description [Unfold the transition relation 'k' states (k = to-from +1), and generate clauses for each state. For a multi-valued latch of 4 vlaues. Two binary variables are used to rpresent X, x1 and x0. For this latch, there exist three multi-valued functions. One for the binary reoresentation of the variable. For example the second entry of the mvf = 1, iff ~x1 and x0. The second mfv is for the data input of the latch. If the And/Inv graph attached to an entry of this mvf equal to 1, X equal to the binary representation corresponding to this entry. For example, if the And/ INV graph attached to the first entry =1, then X = ~x1 & ~x0. To generate the CNF to the transition relation, first generate CNF to next state varaible using mvf of the latch. Then, generate CNF for latch data input using current state variavles. Finaly, generate CNF for the AND of these two MVF. This for every entry of the MVF. Then OR the results. The third MVF is for the initial value of the latch. It is treat the same as the latch data input except if the initial value is constant. ] SideEffects [] SeeAlso [] ******************************************************************************/ void BmcCnfGenerateClausesFromStateToState( Ntk_Network_t *network, int from, int to, BmcCnfClauses_t *cnfClauses, st_table *nodeToMvfAigTable, st_table *CoiTable, int loop) { mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network); st_generator *stGen; Ntk_Node_t *latch, *latchData; MvfAig_Function_t *dataMvfAig, *latchMvfAig; bAigEdge_t *latchBAig, *dataBAig; int i, mvfSize; st_foreach_item(CoiTable, stGen, &latch, NULL) { latchData = Ntk_LatchReadDataInput(latch); dataMvfAig = Bmc_ReadMvfAig(latchData, nodeToMvfAigTable); if (dataMvfAig == NIL(MvfAig_Function_t)){ (void) fprintf(vis_stdout, "No multi-valued function for this node %s \n", Ntk_NodeReadName(latchData)); return; } latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable); if (latchMvfAig == NIL(MvfAig_Function_t)){ latchMvfAig = Bmc_NodeBuildMVF(network, latch); } mvfSize = array_n(dataMvfAig); dataBAig = ALLOC(bAigEdge_t, mvfSize); latchBAig = ALLOC(bAigEdge_t, mvfSize); for(i=0; i< mvfSize; i++){ dataBAig[i] = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(dataMvfAig, i)); latchBAig[i] = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(latchMvfAig, i)); } BmcGenerateClausesFromStateTostate(manager, dataBAig, latchBAig, mvfSize, from, to, cnfClauses, loop); FREE(dataBAig); FREE(latchBAig); } /* For each latch loop*/ return; } /**Function******************************************************************** Synopsis [Generate CNF clauses for the AND gate] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ void BmcCnfGenerateClausesForAND( int a, int b, int c, BmcCnfClauses_t *cnfClauses) { array_t *tmpClause; tmpClause = array_alloc(int, 3); array_insert(int, tmpClause, 0, -a); array_insert(int, tmpClause, 1, -b); array_insert(int, tmpClause, 2, c); BmcCnfInsertClause(cnfClauses, tmpClause); array_free(tmpClause); tmpClause = array_alloc(int, 2); array_insert(int, tmpClause, 0, a); array_insert(int, tmpClause, 1, -c); BmcCnfInsertClause(cnfClauses, tmpClause); array_insert(int, tmpClause, 0, b); BmcCnfInsertClause(cnfClauses, tmpClause); array_free(tmpClause); return; } /**Function******************************************************************** Synopsis [Generate CNF clauses for the OR gate] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ void BmcCnfGenerateClausesForOR( int a, int b, int c, BmcCnfClauses_t *cnfClauses) { array_t *tmpClause; tmpClause = array_alloc(int, 3); array_insert(int, tmpClause, 0, a); array_insert(int, tmpClause, 1, b); array_insert(int, tmpClause, 2, -c); BmcCnfInsertClause(cnfClauses, tmpClause); array_free(tmpClause); tmpClause = array_alloc(int, 2); array_insert(int, tmpClause, 0, -a); array_insert(int, tmpClause, 1, c); BmcCnfInsertClause(cnfClauses, tmpClause); array_insert(int, tmpClause, 0, -b); BmcCnfInsertClause(cnfClauses, tmpClause); array_free(tmpClause); return; } /**Function******************************************************************** Synopsis [Alloc Memory for BmcCnfClauses_t] SideEffects [] SeeAlso [] ******************************************************************************/ BmcCnfClauses_t * BmcCnfClausesAlloc(void) { BmcCnfClauses_t *result = ALLOC(BmcCnfClauses_t, 1); if (!result){ return result; } result->clauseArray = array_alloc(int, 0); result->cnfIndexTable = st_init_table(strcmp, st_strhash); result->freezedKeys = array_alloc(nameType_t *, 0); result->nextIndex = 0; result->noOfClauses = 0; result->cnfGlobalIndex = 1; result->emptyClause = FALSE; result->freezed = FALSE; return result; } /*BmcCnfClausesAlloc()*/ /**Function******************************************************************** Synopsis [Free Memory for BmcCnfClauses_t] SideEffects [] SeeAlso [] ******************************************************************************/ void BmcCnfClausesFree( BmcCnfClauses_t *cnfClauses) { st_generator *stGen; char *name; int cnfIndex; array_free(cnfClauses->clauseArray); array_free(cnfClauses->freezedKeys); if (cnfClauses->cnfIndexTable != NIL(st_table)){ st_foreach_item_int(cnfClauses->cnfIndexTable, stGen, (char **) &name, &cnfIndex) { FREE(name); } st_free_table(cnfClauses->cnfIndexTable); } FREE(cnfClauses); cnfClauses = NIL(BmcCnfClauses_t); } /* BmcCnfClausesFree() */ /**Function******************************************************************** Synopsis [Freeze the current state of CNF] Description [The current state of CNF is stored in the structure BmcCnfStates_t. This information may use later to store CNF to this state by calling BmcCnfClausesRestore().] SideEffects [] SeeAlso [BmcCnfClausesRestore() BmcCnfClausesUnFreeze() ] ******************************************************************************/ BmcCnfStates_t * BmcCnfClausesFreeze( BmcCnfClauses_t * cnfClauses) { BmcCnfStates_t *state = ALLOC(BmcCnfStates_t, 1); state->nextIndex = cnfClauses->nextIndex; state->noOfClauses = cnfClauses->noOfClauses; state->cnfGlobalIndex = cnfClauses->cnfGlobalIndex; /* This variable is used when deleting any new entries in cnfClauses->freezedKeys that will be added after CNF is freezed.*/ state->freezedKeySize = array_n(cnfClauses->freezedKeys); state->emptyClause = cnfClauses->emptyClause; state->freezed = cnfClauses->freezed; cnfClauses->freezed = TRUE; return state; } /* mcCnfClausesFreeze() */ /**Function******************************************************************** Synopsis [Unfreeze CNF] Description [Keeps the current state of CNF] SideEffects [] SeeAlso [] ******************************************************************************/ void BmcCnfClausesUnFreeze( BmcCnfClauses_t *cnfClauses, BmcCnfStates_t *state) { int i; cnfClauses->freezed = FALSE; if (array_n(cnfClauses->freezedKeys) != 0){ int freezedKeySize = array_n(cnfClauses->freezedKeys); for (i=0; i< (freezedKeySize-state->freezedKeySize); i++){ (cnfClauses->freezedKeys)->num--; } } } /* BmcCnfClausesUnFreeze() */ /**Function******************************************************************** Synopsis [Restore the CNF to its previouse state] Description [Restore the CNF to its previouse state that CNF was when BmcCnfClausesFreeze() was last called] SideEffects [] SeeAlso [] ******************************************************************************/ void BmcCnfClausesRestore( BmcCnfClauses_t *cnfClauses, BmcCnfStates_t *state) { int i, index; nameType_t *key; cnfClauses->nextIndex = state->nextIndex; cnfClauses->noOfClauses = state->noOfClauses; cnfClauses->cnfGlobalIndex = state->cnfGlobalIndex; cnfClauses->emptyClause = state->emptyClause; cnfClauses->freezed = state->freezed; if (array_n(cnfClauses->freezedKeys) != 0){ int freezedKeySize = array_n(cnfClauses->freezedKeys); for (i=0; i< (freezedKeySize-state->freezedKeySize); i++){ key = array_fetch_last(nameType_t *, cnfClauses->freezedKeys); if (st_delete_int(cnfClauses->cnfIndexTable, &key, &index)){ FREE(key); } (cnfClauses->freezedKeys)->num--; } } } /* BmcCnfClausesRestore() */ /**Function******************************************************************** Synopsis [Add clause to the clauseArray] Description [Add a clause to the clause array. clause is of type array_t. The user must free clause.] SideEffects [] SeeAlso [] ******************************************************************************/ void BmcCnfInsertClause( BmcCnfClauses_t *cnfClauses, array_t *clause) { int i, lit; if (clause != NIL(array_t)){ if (array_n(clause) == 0){ /* empty clause */ cnfClauses->emptyClause = TRUE; return; } for (i=0; i< array_n(clause); i++){ lit = array_fetch(int, clause, i); array_insert(int, cnfClauses->clauseArray, cnfClauses->nextIndex++, lit); } array_insert(int, cnfClauses->clauseArray, cnfClauses->nextIndex++, 0); /*End Of clause*/ cnfClauses->noOfClauses++; cnfClauses->emptyClause = FALSE; } return; }/* BmcCnfInsertClause() */ /**Function******************************************************************** Synopsis [Add an empty clause] SideEffects [] SeeAlso [] ******************************************************************************/ void BmcAddEmptyClause( BmcCnfClauses_t *cnfClauses) { cnfClauses->emptyClause = TRUE; }/* BmcAddEmptyClause() */ /**Function******************************************************************** Synopsis [Return the cnfIndex of the node] Description [If CNF was generated for this node, return its cnfIndex, otherwise insert the name of this node in the cnfIndexTable, and return its cnfIndex. The key to the cnfIndexTable is (nodeName_state).] SideEffects [] ******************************************************************************/ int BmcCnfReadOrInsertNode( BmcCnfClauses_t *cnfClauses, nameType_t *nodeName, int state, int *nodeIndex) { nameType_t *varName; int index; char *stateStr = util_inttostr(state); varName = util_strcat3(nodeName, "_", stateStr); FREE(stateStr); if (!st_lookup_int(cnfClauses->cnfIndexTable, varName, &index)) { index = cnfClauses->cnfGlobalIndex++; st_insert(cnfClauses->cnfIndexTable, varName, (char*) (long) index); if(cnfClauses->freezed == TRUE){ array_insert_last(nameType_t *, cnfClauses->freezedKeys, varName); } *nodeIndex = index; return 0; /* Inserted */ } else { /* The node has been visited */ *nodeIndex = index; FREE(varName); return 1; } } /**Function******************************************************************** Synopsis [Find the Cone of Influnce (COI) for an LTL formula] Description [Return a list of state variables (latches) that are in the COI of the LTL formula.] SideEffects [] ******************************************************************************/ void BmcGetCoiForLtlFormula( Ntk_Network_t *network, Ctlsp_Formula_t *formula, st_table *ltlCoiTable) { st_table *visited = st_init_table(st_ptrcmp, st_ptrhash); BmcGetCoiForLtlFormulaRecursive(network, formula, ltlCoiTable, visited); st_free_table(visited); return; } /* BmcGetCoiForLtlFormula() */ /**Function******************************************************************** Synopsis [Recursive function to find the COI of a network node.] Description [] SideEffects [] ******************************************************************************/ void BmcGetCoiForLtlFormulaRecursive( Ntk_Network_t *network, Ctlsp_Formula_t *formula, st_table *ltlCoiTable, st_table *visited) { if (formula == NIL(Ctlsp_Formula_t)) { return; } /* leaf node */ if (formula->type == Ctlsp_ID_c){ char *name = Ctlsp_FormulaReadVariableName(formula); Ntk_Node_t *node = Ntk_NetworkFindNodeByName(network, name); int tmp; if (st_lookup_int(visited, (char *) node, &tmp)){ /* Node already visited */ return; } BmcGetCoiForNtkNode(node, ltlCoiTable, visited); return; } BmcGetCoiForLtlFormulaRecursive(network, formula->left, ltlCoiTable, visited); BmcGetCoiForLtlFormulaRecursive(network, formula->right, ltlCoiTable, visited); return; } /* BmcGetCoiForLtlFormulaRecursive() */ /**Function******************************************************************** Synopsis [Genrate COI for a non-latch network node] Description [For each fanins of the given node, if its latch, add it to the CoiTable and return. If it is not latch, call this function to look for any latches in the fanins of this node.] SideEffects [] ******************************************************************************/ void BmcGetCoiForNtkNode( Ntk_Node_t *node, st_table *CoiTable, st_table *visited) { int i, j; Ntk_Node_t *faninNode; if(node == NIL(Ntk_Node_t)){ return; } if (st_lookup_int(visited, (char *) node, &j)){ /* Node already visited */ return; } st_insert(visited, (char *) node, (char *) 0); if (Ntk_NodeTestIsLatch(node)){ st_insert(CoiTable, (char *) node, (char *) 0); } Ntk_NodeForEachFanin(node, i, faninNode) { BmcGetCoiForNtkNode(faninNode, CoiTable, visited); } return; } /* BmcGetCoiForNtkNode() */ /**Function******************************************************************** Synopsis [Find Mdd for states satisfying Atomic Formula.] Description [An atomic formula defines a set of states in the following way: it states a designated ``net'' (specified by the full path name) takes a certain value. The net should be purely a function of latches; as a result an evaluation of the net yields a set of states.] SideEffects [] ******************************************************************************/ mdd_t * BmcModelCheckAtomicFormula( Fsm_Fsm_t *modelFsm, Ctlsp_Formula_t *ctlFormula) { mdd_t * resultMdd; mdd_t *tmpMdd; Ntk_Network_t *network = Fsm_FsmReadNetwork(modelFsm); char *nodeNameString = Ctlsp_FormulaReadVariableName(ctlFormula); char *nodeValueString = Ctlsp_FormulaReadValueName(ctlFormula); Ntk_Node_t *node = Ntk_NetworkFindNodeByName(network, nodeNameString); Var_Variable_t *nodeVar; int nodeValue; graph_t *modelPartition; vertex_t *partitionVertex; Mvf_Function_t *MVF; nodeVar = Ntk_NodeReadVariable(node); if (Var_VariableTestIsSymbolic(nodeVar)) { nodeValue = Var_VariableReadIndexFromSymbolicValue(nodeVar, nodeValueString); } else { nodeValue = atoi(nodeValueString); } modelPartition = Part_NetworkReadPartition(network); if (!(partitionVertex = Part_PartitionFindVertexByName(modelPartition, nodeNameString))) { lsGen tmpGen; Ntk_Node_t *tmpNode; array_t *mvfArray; array_t *tmpRoots = array_alloc(Ntk_Node_t *, 0); st_table *tmpLeaves = st_init_table(st_ptrcmp, st_ptrhash); array_insert_last(Ntk_Node_t *, tmpRoots, node); Ntk_NetworkForEachCombInput(network, tmpGen, tmpNode) { st_insert(tmpLeaves, (char *) tmpNode, (char *) NTM_UNUSED); } mvfArray = Ntm_NetworkBuildMvfs(network, tmpRoots, tmpLeaves, NIL(mdd_t)); MVF = array_fetch(Mvf_Function_t *, mvfArray, 0); array_free(tmpRoots); st_free_table(tmpLeaves); array_free(mvfArray); tmpMdd = Mvf_FunctionReadComponent(MVF, nodeValue); resultMdd = mdd_dup(tmpMdd); Mvf_FunctionFree(MVF); } else { MVF = Part_VertexReadFunction(partitionVertex); tmpMdd = Mvf_FunctionReadComponent(MVF, nodeValue); resultMdd = mdd_dup(tmpMdd); } if (Part_PartitionReadMethod(modelPartition) == Part_Frontier_c && Ntk_NodeTestIsCombOutput(node)) { array_t *psVars = Fsm_FsmReadPresentStateVars(modelFsm); mdd_manager *mgr = Ntk_NetworkReadMddManager(Fsm_FsmReadNetwork(modelFsm)); array_t *supportList; st_table *supportTable = st_init_table(st_numcmp, st_numhash); int i, j; int existIntermediateVars; int mddId; Mvf_Function_t *mvf; vertex_t *vertex; array_t *varBddRelationArray, *varArray; mdd_t *iv, *ivMdd, *relation; for (i = 0; i < array_n(psVars); i++) { mddId = array_fetch(int, psVars, i); st_insert(supportTable, (char *)(long)mddId, NULL); } existIntermediateVars = 1; while (existIntermediateVars) { existIntermediateVars = 0; supportList = mdd_get_support(mgr, resultMdd); for (i = 0; i < array_n(supportList); i++) { mddId = array_fetch(int, supportList, i); if (!st_lookup(supportTable, (char *)(long)mddId, NULL)) { vertex = Part_PartitionFindVertexByMddId(modelPartition, mddId); mvf = Part_VertexReadFunction(vertex); varBddRelationArray = mdd_fn_array_to_bdd_rel_array(mgr, mddId, mvf); varArray = mdd_id_to_bdd_array(mgr, mddId); assert(array_n(varBddRelationArray) == array_n(varArray)); for (j = 0; j < array_n(varBddRelationArray); j++) { iv = array_fetch(mdd_t *, varArray, j); relation = array_fetch(mdd_t *, varBddRelationArray, j); ivMdd = bdd_cofactor(relation, iv); mdd_free(relation); tmpMdd = resultMdd; resultMdd = bdd_compose(resultMdd, iv, ivMdd); mdd_free(tmpMdd); mdd_free(iv); mdd_free(ivMdd); } array_free(varBddRelationArray); array_free(varArray); existIntermediateVars = 1; } } array_free(supportList); } st_free_table(supportTable); } return resultMdd; } /**Function******************************************************************** Synopsis [Read fairness constraints from file and check for errors.] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ array_t * BmcReadFairnessConstraints( FILE *fp /* pointer to the fairness constraint file */) { array_t *constraintArray; /* raw fairness constraints */ array_t *ltlConstraintArray; /* constraints converted to LTL */ if (fp == NIL(FILE) ) { /* Nothing to be done. */ return NIL(array_t); } /* Read constraints from file and check for errors. */ constraintArray = Ctlsp_FileParseFormulaArray(fp); if (constraintArray == NIL(array_t)) { (void) fprintf(vis_stderr, "** ctlsp error: error reading fairness constraints.\n"); return NIL(array_t); } if (array_n(constraintArray) == 0) { (void) fprintf(vis_stderr, "** ctlsp error: fairness file is empty.\n"); return NIL(array_t); } /* * Check that each constraint is an LTL formula. */ ltlConstraintArray = Ctlsp_FormulaArrayConvertToLTL(constraintArray); Ctlsp_FormulaArrayFree(constraintArray); if (ltlConstraintArray == NIL(array_t)) { (void) fprintf(vis_stderr, "** ctlsp error: fairness constraints are not LTL formulae.\n"); return NIL(array_t); } return ltlConstraintArray; } /* BmcReadFairnessConstraints */ /**Function******************************************************************** Synopsis [return the cnf index for a bdd node] SideEffects [] ******************************************************************************/ int BmcGetCnfVarIndexForBddNode( bdd_manager *bddManager, bdd_node *node, int state, BmcCnfClauses_t *cnfClauses) { array_t *mvar_list = mdd_ret_mvar_list(bddManager); array_t *bvar_list = mdd_ret_bvar_list(bddManager); char name[100]; char *nodeName; bvar_type bv; mvar_type mv; int nodeIndex = bdd_node_read_index(node); int index, rtnNodeIndex, rtnCode; /* If the node is for a multi-valued varaible. */ if (nodeIndex < array_n(bvar_list)){ bv = array_fetch(bvar_type, bvar_list, nodeIndex); /* get the multi-valued varaible. */ mv = array_fetch(mvar_type, mvar_list, bv.mvar_id); arrayForEachItem(int, mv.bvars, index, rtnNodeIndex) { if (nodeIndex == rtnNodeIndex){ break; } } assert(index < mv.encode_length); /* printf("Name of bdd node %s %d\n", mv.name, index); */ sprintf(name, "%s_%d", mv.name, index); } else { sprintf(name, "Bdd_%d", nodeIndex); } nodeName = util_strsav(name); rtnCode = BmcCnfReadOrInsertNode(cnfClauses, nodeName, state, &nodeIndex); if(rtnCode == 1) { FREE(nodeName); } return nodeIndex; } /*---------------------------------------------------------------------------*/ /* Definition of static functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Test that the given string is an integer. Returns 0 if string is not an integer, 1 if the integer is too big for int, and 2 if integer fits in int.] SideEffects [Sets the pointer value if the string is an integer small enough for int.] ******************************************************************************/ 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 [Compare procedure for name comparison.] Description [Compare procedure for name comparison.] SideEffects [] ******************************************************************************/ static int nameCompare( const void * name1, const void * name2) { return(strcmp(*(char**)name1, *(char **)name2)); } /* end of signatureCompare */ /**Function******************************************************************** Synopsis [Print the valuse of variables in the variable list "varNames".] Description [For each variable in the variable list, this functions prints its value in the resultTable if it is different for its value in prevValue. If this variable is a symbolic variable, this function prints its symbolic value.] SideEffects [] ******************************************************************************/ static void printValue( mAig_Manager_t *manager, Ntk_Network_t *network, st_table *nodeToMvfAigTable, BmcCnfClauses_t *cnfClauses, array_t *varNames, st_table *resultTable, int state, int *prevValue) { Ntk_Node_t *node; int i, j; bAigEdge_t bAigId; nameType_t *varName, *nodeName; int value, index; MvfAig_Function_t *MvfAig; int changed = 0; int tmp; for (j=0; j< array_n(varNames); j++) { if (state == 0){ prevValue[j] = -1; } nodeName = array_fetch(char *, varNames, j); /* Fetch the node corresponding to this node name. */ node = Ntk_NetworkFindNodeByName(network, nodeName); /* Get the multi-valued function for each node */ MvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable); /* In case of the multi-valued function is not build for this node, do nothing. We may notify the user. */ if (MvfAig == NIL(MvfAig_Function_t)){ continue; } /* No CNF index for this variable at time "state in the " */ value = -1; for (i=0; i< array_n(MvfAig); i++) { bAigId = MvfAig_FunctionReadComponent(MvfAig, i); /* constant value */ if (bAigId == bAig_One){ /* This variable equal the constant i. */ value = i; break; } if (bAigId != bAig_Zero){ char *tmpStr; nodeName = bAig_NodeReadName(manager, bAigId); /* Build the variable name at state "state". */ tmpStr = util_inttostr(state); varName = util_strcat3(nodeName, "_", tmpStr); if (st_lookup_int(cnfClauses->cnfIndexTable, varName, &index)) { if (bAig_IsInverted(bAigId)){ index = -index; } /*if (searchArray(result, index) > -1){*/ if (st_lookup_int(resultTable, (char *)(long)index, &tmp)){ value = i; break; } } /* if st_lookup_int() */ FREE(tmpStr); FREE(varName); } /* if (bAigId != bAig_Zero) */ } if (value >= 0){ if (value != prevValue[j]){ Var_Variable_t *nodeVar = Ntk_NodeReadVariable(node); prevValue[j] = value; changed = 1; if (Var_VariableTestIsSymbolic(nodeVar)) { char *symbolicValue = Var_VariableReadSymbolicValueFromIndex(nodeVar, value); (void) fprintf(vis_stdout,"%s:%s\n", Ntk_NodeReadName(node), symbolicValue); } else { (void) fprintf(vis_stdout,"%s:%d\n", Ntk_NodeReadName(node), value); } } } else { /* This variable does not have value in the current time frame. It means its value is not important at this time frame. */ (void) fprintf(vis_stdout,"%s:X\n", Ntk_NodeReadName(node)); } } /* for j loop */ if (changed == 0){ fprintf( vis_stdout, "\n"); } }/* end of printValue() */ /**Function******************************************************************** Synopsis [Print the valuse of variables in the variable list "varNames".] Description [For each variable in the variable list, this functions prints the values of names, which do not start with $_ as these are true latches of the model. Since this is in aiger format, hence all the values are printed even if they didn't change from the previous values.] SideEffects [] ******************************************************************************/ static void printValueAiger( mAig_Manager_t *manager, Ntk_Network_t *network, st_table *nodeToMvfAigTable, BmcCnfClauses_t *cnfClauses, array_t *varNames, st_table *resultTable, int state, int *prevValue) { Ntk_Node_t *node; int i, j; bAigEdge_t bAigId; nameType_t *varName, *nodeName; int value, index; MvfAig_Function_t *MvfAig; int tmp; char * NodeName; for (j=0; j< array_n(varNames); j++) { if (state == 0){ prevValue[j] = -1; } nodeName = array_fetch(char *, varNames, j); /* Fetch the node corresponding to this node name. */ node = Ntk_NetworkFindNodeByName(network, nodeName); /* Get the multi-valued function for each node */ MvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable); /* In case of the multi-valued function is not build for this node, do nothing. We may notify the user. */ if (MvfAig == NIL(MvfAig_Function_t)){ continue; } /* No CNF index for this variable at time "state in the " */ value = -1; for (i=0; i< array_n(MvfAig); i++) { bAigId = MvfAig_FunctionReadComponent(MvfAig, i); /* constant value */ if (bAigId == bAig_One){ /* This variable equal the constant i. */ value = i; break; } if (bAigId != bAig_Zero){ char *tmpStr; nodeName = bAig_NodeReadName(manager, bAigId); /* Build the variable name at state "state". */ tmpStr = util_inttostr(state); varName = util_strcat3(nodeName, "_", tmpStr); if (st_lookup_int(cnfClauses->cnfIndexTable, varName, &index)) { if (bAig_IsInverted(bAigId)){ index = -index; } /*if (searchArray(result, index) > -1){*/ if (st_lookup_int(resultTable, (char *)(long)index, &tmp)){ value = i; break; } } /* if st_lookup_int() */ FREE(tmpStr); FREE(varName); } /* if (bAigId != bAig_Zero) */ } NodeName = Ntk_NodeReadName(node); if(!((NodeName[0] == '$') && (NodeName[1] == '_'))) { if (value >= 0){ Var_Variable_t *nodeVar = Ntk_NodeReadVariable(node); prevValue[j] = value; if (Var_VariableTestIsSymbolic(nodeVar)) { char *symbolicValue = Var_VariableReadSymbolicValueFromIndex(nodeVar, value); (void) fprintf(vis_stdout,"%s", symbolicValue); } else { (void) fprintf(vis_stdout,"%d", value); } } else { /* This variable does not have value in the current time frame. It means its value is not important at this time frame. */ (void) fprintf(vis_stdout,"x" ); } } /* these nodes are latches in front of inputs so they will be printed out as inputs */ } /* for j loop */ }/* end of printValueAiger() */ /**Function******************************************************************** Synopsis [Print the valuse of variables in the variable list "varNames".] Description [For each variable in the variable list, this functions checks if the name starts with $_, which means that those latches are actually storing the value of inputs. This modification to the model is externally done and not done by VIS so this method is only specific to certain type of model, the output of aigtoblif translator.] SideEffects [] ******************************************************************************/ static void printValueAigerInputs( mAig_Manager_t *manager, Ntk_Network_t *network, st_table *nodeToMvfAigTable, BmcCnfClauses_t *cnfClauses, array_t *varNames, st_table *resultTable, int state, int *prevValue) { Ntk_Node_t *node; int i, j; bAigEdge_t bAigId; nameType_t *varName, *nodeName; int value, index; MvfAig_Function_t *MvfAig; int tmp; char * NodeName; for (j=0; j< array_n(varNames); j++) { if (state == 0){ prevValue[j] = -1; } nodeName = array_fetch(char *, varNames, j); /* Fetch the node corresponding to this node name. */ node = Ntk_NetworkFindNodeByName(network, nodeName); /* Get the multi-valued function for each node */ MvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable); /* In case of the multi-valued function is not build for this node, do nothing. We may notify the user. */ if (MvfAig == NIL(MvfAig_Function_t)){ continue; } /* No CNF index for this variable at time "state in the " */ value = -1; for (i=0; i< array_n(MvfAig); i++) { bAigId = MvfAig_FunctionReadComponent(MvfAig, i); /* constant value */ if (bAigId == bAig_One){ /* This variable equal the constant i. */ value = i; break; } if (bAigId != bAig_Zero){ char *tmpStr; nodeName = bAig_NodeReadName(manager, bAigId); /* Build the variable name at state "state". */ tmpStr = util_inttostr(state); varName = util_strcat3(nodeName, "_", tmpStr); if (st_lookup_int(cnfClauses->cnfIndexTable, varName, &index)) { if (bAig_IsInverted(bAigId)){ index = -index; } /*if (searchArray(result, index) > -1){*/ if (st_lookup_int(resultTable, (char *)(long)index, &tmp)){ value = i; break; } } /* if st_lookup_int() */ FREE(tmpStr); FREE(varName); } /* if (bAigId != bAig_Zero) */ } NodeName = Ntk_NodeReadName(node); if((NodeName[0] == '$') && (NodeName[1] == '_')) { if (value >= 0){ Var_Variable_t *nodeVar = Ntk_NodeReadVariable(node); prevValue[j] = value; if (Var_VariableTestIsSymbolic(nodeVar)) { char *symbolicValue = Var_VariableReadSymbolicValueFromIndex(nodeVar, value); (void) fprintf(vis_stdout,"%s", symbolicValue); } else { (void) fprintf(vis_stdout,"%d", value); } } else { /* This variable does not have value in the current time frame. It means its value is not important at this time frame. */ (void) fprintf(vis_stdout,"x" ); } } /* these nodes are latches in front of inputs so they will be printed out as inputs */ } /* for j loop */ }/* end of printValueAigerInputs() */