Index: vis_dev/vis-2.3/src/debug/debug.c =================================================================== --- vis_dev/vis-2.3/src/debug/debug.c (revision 42) +++ vis_dev/vis-2.3/src/debug/debug.c (revision 44) @@ -132,22 +132,44 @@ { Ntk_Network_t * ntk; - int c,verbose; + int c,verbose = 0; + array_t * excludes = NIL(array_t); Dbg_Abnormal_t * abnormal; ntk = Ntk_HrcManagerReadCurrentNetwork(*hmgr); + char * subs; if (ntk == NIL(Ntk_Network_t)) { (void) fprintf(vis_stdout, "** abn error: No network\n"); return 1; } - while ((c = util_getopt(argc, argv, "vh:m:k:o:")) != EOF) { + while ((c = util_getopt(argc, argv, "vhs:")) != EOF) { switch(c) { + case 'h': + goto usage; case 'v': verbose = 1; break; + case 's': + subs = util_strsav(util_optarg); + excludes = array_alloc(char*,0); + array_insert_last(char*,excludes,subs); + break; + default : + goto usage; } } abnormal = Dbg_DebugAbnormalAlloc(ntk); abnormal->verbose = verbose; - Dbg_AddAbnormalPredicatetoNetwork(abnormal); -} + printf("SUBS %s \n",subs); + Dbg_AddAbnormalPredicatetoNetwork(abnormal,excludes); + printf("\t # Abnormal predicate created %d\n", array_n(abnormal->abnormal)); + return 0; + usage : + (void) fprintf(vis_stderr, "usage: _createAbn [-h] [-v verboseLevel] [-s substystem excludes\n"); + (void) fprintf(vis_stderr, " -h \tprint the command usage\n"); + (void) fprintf(vis_stderr, " -v \t verbosity\n"); + (void) fprintf(vis_stderr, " -s \texclude the abnormal predicate\ + for this subssytem\n"); + return 1; +} + /**Function******************************************************************** @@ -190,5 +212,4 @@ array_t * formulaArray; array_t * LTLformulaArray; -char * ltlFileName = NIL(char); array_t * faultNodes = array_alloc(Ntk_Node_t*,0); @@ -201,5 +222,4 @@ -printf("MAX K %d", options->maxK); if (verbose) { @@ -252,5 +272,4 @@ } Ctlsp_Formula_t *ltlFormula = array_fetch(Ctlsp_Formula_t *, LTLformulaArray, 0); - @@ -283,5 +302,5 @@ int l; // return the clause number - int noLoopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, k, cnfClauses); + int noLoopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, k, cnfClauses); printf("LTL %d \n",noLoopIndex); @@ -298,5 +317,5 @@ assert(nodeToMvfAigTable != NIL(st_table)); - Dbg_InitAbn(abn,manager, nodeToMvfAigTable,cnfClauses); + Dbg_InitAbn(abn,manager, nodeToMvfAigTable,k,cnfClauses); //loop abnormal @@ -305,28 +324,45 @@ Dbg_ForEachAbnormal(abn,aIndex,abnNode){ char * nodeName = Ntk_NodeReadName(abnNode); - //set abnormal - int cnfIndex = array_fetch(int,abn->abnCnfIndexArray, aIndex); + //set abnormal for each step + array_t * cnfIndexArray = array_fetch(array_t*,abn->abnCnfIndexArray,aIndex); + int cnfIndex; + int step; bAigEdge_t* abnBAig = array_fetch(bAigEdge_t*,abn->abnAigArray, aIndex); - int abnIndex = BmcGenerateCnfFormulaForAigFunction(manager,abnBAig[1],0,cnfClauses); - array_insert(int,cnfClauses->clauseArray,cnfIndex,abnIndex); - FILE *cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0); - BmcWriteClauses(manager, cnfFile, cnfClauses, options); - fclose(cnfFile); - + array_t * cnfVal = array_alloc(int,0); + arrayForEachItem(int, cnfIndexArray, step, cnfIndex){ + int abnIndex = BmcGenerateCnfFormulaForAigFunction(manager,abnBAig[1],step,cnfClauses); + array_insert(int,cnfClauses->clauseArray,cnfIndex,abnIndex); + array_insert_last(int,cnfVal,abnIndex); + FILE *cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0); + BmcWriteClauses(manager, cnfFile, cnfClauses, options); + fclose(cnfFile); + printf("AINDEX %d\n",aIndex); + if(aIndex == 0) + { + FILE *cnfFile = Cmd_FileOpen("test_aks.cnf", "w", NIL(char *), 0); + BmcWriteClauses(manager, cnfFile, cnfClauses, options); + fclose(cnfFile); + + } + }//end for each step + //SAT procedure //assig assig input from cex //TODO build cex correctly - int res = Dbg_SatCheck("assig",options->cnfFileName,options->verbosityLevel); + int res = Dbg_SatCheck("assig",options->satInFile,options->verbosityLevel); // Build set of FaultCandidates if (res == SAT_SAT) { char * realNodeName = util_strsav(nodeName); - realNodeName[strlen(nodeName)-4] = '\0'; + realNodeName[strlen(nodeName)-3] = '\0'; + printf("Real = %s\n", realNodeName); Ntk_Node_t * realNode = Ntk_NetworkFindNodeByName(network,realNodeName); array_insert_last(Ntk_Node_t*,faultNodes,realNode); } - - array_insert(int,cnfClauses->clauseArray,cnfIndex,-abnIndex); + arrayForEachItem(int, cnfIndexArray, step, cnfIndex){ + int abnIndex = array_fetch(int,cnfVal,step); + array_insert(int,cnfClauses->clauseArray,cnfIndex,-abnIndex); + } } @@ -335,7 +371,10 @@ latches %d \n",cnfClauses->noOfClauses,st_count(CoiTable)); + (void) fprintf(vis_stdout,"Number of Fault candidates %d\n", array_n(faultNodes)); (void) fprintf(vis_stdout,"gates : \n"); + + printNodeArray(faultNodes); @@ -346,6 +385,6 @@ array_free(faultNodes); return 0; - -} +} + /**Function******************************************************************** @@ -420,9 +459,9 @@ if (argc - util_optind != 0) { - outName = util_strsav(argv[util_optind]); - /* create SAT Solver input file */ + outName = util_strsav(argv[util_optind]); + /* create SAT Solver input file */ options->cnfFileName= outName; - options->satInFile = options->cnfFileName; - cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0); + options->satInFile = options->cnfFileName; + cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0); } Index: vis_dev/vis-2.3/src/debug/debug.h =================================================================== --- vis_dev/vis-2.3/src/debug/debug.h (revision 42) +++ vis_dev/vis-2.3/src/debug/debug.h (revision 44) @@ -126,5 +126,6 @@ EXTERN void Dbg_DebugAbnormalFree(Dbg_Abnormal_t * abn); EXTERN void Dbg_AbnormalFreeCallback(void *data); -EXTERN void Dbg_AddAbnormalPredicatetoNetwork(Dbg_Abnormal_t* abnormal); +EXTERN void Dbg_AddAbnormalPredicatetoNetwork(Dbg_Abnormal_t* abnormal,array_t* +excludes); EXTERN void Dbg_AddAbnormalPredicate(Dbg_Abnormal_t * abn, Ntk_Node_t* abnNode); EXTERN void Dbg_AddFreeInput(Dbg_Abnormal_t * abn, Ntk_Node_t* fNode); @@ -133,5 +134,5 @@ EXTERN Dbg_Abnormal_t * Dbg_NetworkReadAbnormal(Ntk_Network_t * network); EXTERN void Dbg_InitAbn(Dbg_Abnormal_t * abn, bAig_Manager_t * manager, -st_table * nodeToMvfAigTable, BmcCnfClauses_t *cnfClauses); +st_table * nodeToMvfAigTable, int k, BmcCnfClauses_t *cnfClauses); EXTERN int Dbg_SatCheck(char * forceAssigName, char * cnfFileName, int verbose); EXTERN BmcCnfClauses_t* Dbg_GenerateCNF(Ntk_Network_t * network, @@ -140,5 +141,4 @@ - /**AutomaticEnd***************************************************************/ Index: vis_dev/vis-2.3/src/debug/debugAbnormal.c =================================================================== --- vis_dev/vis-2.3/src/debug/debugAbnormal.c (revision 42) +++ vis_dev/vis-2.3/src/debug/debugAbnormal.c (revision 44) @@ -19,6 +19,7 @@ char * nodeName = util_strsav(Ntk_NodeReadName(node)); //Create var Name - char * newVarName = (char *) malloc(strlen(nodeName) + strlen(varName) +1); - sprintf(newVarName,"%s_%s",nodeName,varName); + //char * newVarName = (char *) malloc(strlen(nodeName) + strlen(varName) +1); + //sprintf(newVarName,"%s_%s",nodeName,varName); + char * newVarName = util_strcat3(nodeName,varName,""); Var_Variable_t * var = Var_VariableAlloc(NIL(Hrc_Node_t),newVarName); //Create new Node @@ -45,5 +46,7 @@ For a combinatorial node n is tranformed into (abn_n)?i_n:n If the abnormal predicate is active then n is replaced by a free input. - We assume that the combinatorial gate at on one bit only.] + We assume that the combinatorial gate at on one bit only. + The array excludes contains name of submodules which we do not want to add + abnormal predicates.] SideEffects [fill the abnormal structure] @@ -53,5 +56,5 @@ ******************************************************************************/ -void Dbg_AddAbnormalPredicatetoNetwork(Dbg_Abnormal_t* abnormal ) /*abnormal struct*/ +void Dbg_AddAbnormalPredicatetoNetwork(Dbg_Abnormal_t* abnormal,array_t* excludes) { @@ -61,8 +64,11 @@ Ntk_NetworkForEachNode(ntk,gen,node){ //For each combinatorial node - if(Ntk_NodeTestIsCombinational(node)){ + if(Ntk_NodeTestIsCombinational(node) && !Ntk_NodeTestIsLatchDataInput(node)){ if(Ntk_NodeReadNumFanins(node) > 1 && Ntk_NodeReadNumFanouts(node)> 0) { char * nodeName = util_strsav(Ntk_NodeReadName(node)); + + + if(!Dbg_TestNodeInSubs(nodeName,excludes)){ printf("%s \n", nodeName); @@ -125,4 +131,5 @@ Tbl_TableWriteBlifMvToFile(table,0,vis_stdout); } + } } } @@ -132,4 +139,5 @@ (void *) abnormal); } + /**Function******************************************************************** @@ -289,10 +297,11 @@ Synopsis [Initialize the abnormal predicate in the clauses array abni =0] - Description [Fill the Dbg data structure, abnAigArray conains the set of Aig + Description [Fill the Dbg data structure, abnAigArray contains the set of Aig for the set of abnormal perdicate. Each abnormal are set to zero in the clause - array.predicabnCnfIndexArray is the cnf index. The correspondance is made by - the index in the table, the index of a node in abnArray is the same in + array.predicabnCnfIndexArray is the cnf index for each k steps. + The correspondance is made by the index in the table, + the index of a node in abnArray is the same in abnAigArray and in abnIndexArray. If this array were alredy computed nothing - is done, if the aig or index information either.] + is done, if the aig or index information either. ] SideEffects [Fill abnAigArray and abnCnfIndexArray] @@ -304,4 +313,5 @@ bAig_Manager_t * manager, st_table * nodeToMvfAigTable, +int k, BmcCnfClauses_t *cnfClauses) { @@ -315,5 +325,6 @@ int size = array_n(abn->abnormal); array_t * abnAigArray = array_alloc(bAigEdge_t *,size); - array_t * abnIndexArray = array_alloc(int,size); + array_t * abnIndexArray = array_alloc(array_t*,size); + int i; int aIndex; Ntk_Node_t * abnNode; @@ -322,5 +333,5 @@ if (abnMvfAig == NIL(MvfAig_Function_t)){ (void) fprintf(vis_stdout, "No multi-valued function for this node %s \ - create abnormal predicate firs \n", Ntk_NodeReadName(abnNode)); + create abnormal predicate first \n", Ntk_NodeReadName(abnNode)); return ; } @@ -335,12 +346,19 @@ } array_insert(bAigEdge_t*,abnAigArray,aIndex,abnBAig); - int abnIndex = BmcGenerateCnfFormulaForAigFunction(manager,abnBAig[0],0,cnfClauses); - array_insert(int,abnIndexArray,aIndex,cnfClauses->nextIndex); - // Create clause - array_t *abnClause = NIL(array_t); - abnClause = array_alloc(int, 0); - array_insert_last(int, abnClause, abnIndex); - BmcCnfInsertClause(cnfClauses, abnClause); - array_free(abnClause); + // Cnf Index + array_t * indexArray = array_alloc(int,k); + for (i = 0; i <= k;i++) + { + int abnIndex = BmcGenerateCnfFormulaForAigFunction(manager,abnBAig[0],i,cnfClauses); + array_insert(int,indexArray,i,cnfClauses->nextIndex); + // Create clause + array_t *abnClause = NIL(array_t); + abnClause = array_alloc(int, 0); + array_insert_last(int, abnClause, abnIndex); + BmcCnfInsertClause(cnfClauses, abnClause); + array_free(abnClause); + } + array_insert(array_t*,abnIndexArray,aIndex,indexArray); + //array_free(indexArray); } abn->abnAigArray = abnAigArray; Index: vis_dev/vis-2.3/src/debug/debugInt.h =================================================================== --- vis_dev/vis-2.3/src/debug/debugInt.h (revision 42) +++ vis_dev/vis-2.3/src/debug/debugInt.h (revision 44) @@ -56,5 +56,5 @@ array_t * freeInputs; /* Array of Ntk_Node_t* */ array_t * abnAigArray; /* Array of bAigEdge_t* as many entries as possible value */ - array_t * abnCnfIndexArray; /* Array of int */ + array_t * abnCnfIndexArray; /* Array of array of cnf index for each steps */ int verbose; }; @@ -86,4 +86,5 @@ void mdd_GetState_Values(mdd_manager *mgr, mdd_t * top, FILE * f); void printNodeArray(array_t * nodeArray); +boolean Dbg_TestNodeInSubs(char* nodeName,array_t * subsName); /**AutomaticEnd***************************************************************/ Index: vis_dev/vis-2.3/src/debug/debugUtilities.c =================================================================== --- vis_dev/vis-2.3/src/debug/debugUtilities.c (revision 42) +++ vis_dev/vis-2.3/src/debug/debugUtilities.c (revision 44) @@ -236,3 +236,33 @@ } } - +/**Function******************************************************************** + + Synopsis [Test if a node is in a given submodule] + + Description [Return true if the node is in one of the submdule, + else return false. The comparison is made by the name of the node + compare to the name of the submodule. Node name n that belongs to a + subsystem named sub as in the following form : sub.n] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ + +boolean Dbg_TestNodeInSubs(char* nodeName,array_t * subsName) +{ + assert(nodeName != NIL(char)); + if(subsName == NIL(array_t)) + return 0; + if(array_n(subsName) == 0) + return 0; + int i; + char * subName; + arrayForEachItem(char*, subsName, i, subName){ + if(strstr(nodeName,subName) != NULL) + return 1; + } + return 0; +} +