Index: /vis_dev/vis-2.3/src/debug/debug.c =================================================================== --- /vis_dev/vis-2.3/src/debug/debug.c (revision 41) +++ /vis_dev/vis-2.3/src/debug/debug.c (revision 42) @@ -191,5 +191,5 @@ array_t * LTLformulaArray; char * ltlFileName = NIL(char); - +array_t * faultNodes = array_alloc(Ntk_Node_t*,0); /* @@ -286,5 +286,5 @@ - array_t *objClause = NIL(array_t); + array_t *objClause = NIL(array_t); objClause = array_alloc(int, 0); array_insert_last(int, objClause, noLoopIndex); @@ -295,38 +295,54 @@ st_table * nodeToMvfAigTable = NIL(st_table); nodeToMvfAigTable = -(st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY); -assert(nodeToMvfAigTable != NIL(st_table)); + (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY); + assert(nodeToMvfAigTable != NIL(st_table)); Dbg_InitAbn(abn,manager, nodeToMvfAigTable,cnfClauses); - //loop abnormal + //loop abnormal int aIndex; Ntk_Node_t * abnNode; - Dbg_ForEachAbnormal(abn,aIndex,abnNode){ - if(aIndex<=0){ - //set abnormal + Dbg_ForEachAbnormal(abn,aIndex,abnNode){ + char * nodeName = Ntk_NodeReadName(abnNode); + //set abnormal int cnfIndex = array_fetch(int,abn->abnCnfIndexArray, aIndex); 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); - + //SAT procedure - int res = Dbg_SatCheck("assig",options->cnfFileName); - - array_insert(int,cnfClauses->clauseArray,cnfIndex,-abnIndex); - } - } + //assig assig input from cex + //TODO build cex correctly + int res = Dbg_SatCheck("assig",options->cnfFileName,options->verbosityLevel); + // Build set of FaultCandidates + if (res == SAT_SAT) + { + char * realNodeName = util_strsav(nodeName); + realNodeName[strlen(nodeName)-4] = '\0'; + Ntk_Node_t * realNode = Ntk_NetworkFindNodeByName(network,realNodeName); + array_insert_last(Ntk_Node_t*,faultNodes,realNode); + } + + + array_insert(int,cnfClauses->clauseArray,cnfIndex,-abnIndex); + } if(verbose) (void) fprintf(vis_stdout, "The _sat_debug generates %d clauses with %d\ - latches %d nodetomvf.\n",cnfClauses->noOfClauses,st_count(CoiTable),st_count(nodeToMvfAigTable)); - + 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); + + Ctlsp_FormulaArrayFree(LTLformulaArray); BmcCnfClausesFree(cnfClauses); BmcOptionFree(options); +array_free(faultNodes); return 0; Index: /vis_dev/vis-2.3/src/debug/debug.h =================================================================== --- /vis_dev/vis-2.3/src/debug/debug.h (revision 41) +++ /vis_dev/vis-2.3/src/debug/debug.h (revision 42) @@ -134,7 +134,8 @@ EXTERN void Dbg_InitAbn(Dbg_Abnormal_t * abn, bAig_Manager_t * manager, st_table * nodeToMvfAigTable, BmcCnfClauses_t *cnfClauses); -EXTERN int Dbg_SatCheck(char * forceAssigName, char * cnfFileName); +EXTERN int Dbg_SatCheck(char * forceAssigName, char * cnfFileName, int verbose); EXTERN BmcCnfClauses_t* Dbg_GenerateCNF(Ntk_Network_t * network, BmcOption_t * option, st_table *CoiTable); +EXTERN int Dbg_GetDefaultValue(Tbl_Table_t * table); Index: /vis_dev/vis-2.3/src/debug/debugAbnormal.c =================================================================== --- /vis_dev/vis-2.3/src/debug/debugAbnormal.c (revision 41) +++ /vis_dev/vis-2.3/src/debug/debugAbnormal.c (revision 42) @@ -44,5 +44,6 @@ with a new table including the abnormal predicate. For a combinatorial node n is tranformed into (abn_n)?i_n:n - If the abnormal predicate is activ then n is replaced by a free input] + 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.] SideEffects [fill the abnormal structure] @@ -67,6 +68,8 @@ Tbl_Table_t *table = Ntk_NodeReadTable(node); - (void) fprintf(vis_stdout, "** old table\n"); - Tbl_TableWriteBlifMvToFile(table,2,vis_stdout); + if(abnormal->verbose){ + (void) fprintf(vis_stdout, "** old table\n"); + Tbl_TableWriteBlifMvToFile(table,2,vis_stdout); + } // Build new variables abnormal and input Ntk_Node_t * abnNode = Dbg_CreateNewNode(ntk,node,"abn"); @@ -81,6 +84,5 @@ Tbl_TableAddColumn(table,i,0); int iIndex = Tbl_TableReadVarIndex(table, i, 0); - - //For each row already there in the table + int rowNum; for(rowNum = 0; rowNum < Tbl_TableReadNumRows(table);rowNum++){ @@ -94,5 +96,5 @@ //the new row int r = Tbl_TableAddRow(table); - + int colNum; for (colNum = 0; colNum < Tbl_TableReadNumInputs(table); colNum++) { @@ -104,11 +106,23 @@ Tbl_TableSetEntry(table, entry, r, colNum, 0); } + int defaultVal = Dbg_GetDefaultValue(table); + if(defaultVal == -1) + { + (void) fprintf(vis_stdout, "Error default value of the table \ + of node %s\n", nodeName); + return; + } + int outVal = (defaultVal +1 )% 2; + if(abnormal->verbose) + (void) fprintf(vis_stdout, "Default value : %d\n",defaultVal); for (colNum = 0; colNum < Tbl_TableReadNumOutputs(table); colNum++){ Tbl_Entry_t * entry = Tbl_EntryAlloc(Tbl_EntryNormal_c); - Tbl_EntrySetValue(entry,1,1); + Tbl_EntrySetValue(entry,outVal,outVal); Tbl_TableSetEntry(table, entry, r, colNum, 1); } + if(abnormal->verbose){ printf("---------------\n"); Tbl_TableWriteBlifMvToFile(table,0,vis_stdout); + } } } Index: /vis_dev/vis-2.3/src/debug/debugInt.h =================================================================== --- /vis_dev/vis-2.3/src/debug/debugInt.h (revision 41) +++ /vis_dev/vis-2.3/src/debug/debugInt.h (revision 42) @@ -85,4 +85,5 @@ st_table * generateAllLatches(Ntk_Network_t * ntk); void mdd_GetState_Values(mdd_manager *mgr, mdd_t * top, FILE * f); +void printNodeArray(array_t * nodeArray); /**AutomaticEnd***************************************************************/ Index: /vis_dev/vis-2.3/src/debug/debugUtilities.c =================================================================== --- /vis_dev/vis-2.3/src/debug/debugUtilities.c (revision 41) +++ /vis_dev/vis-2.3/src/debug/debugUtilities.c (revision 42) @@ -1,3 +1,14 @@ #include "debug.h" +void printNodeArray(array_t * nodeArray) +{ + int i; + Ntk_Node_t* node; + arrayForEachItem(Ntk_Node_t *, nodeArray, i, node){ + printf("%s\n",Ntk_NodeReadName(node)); + } + + +} + void printLatch(st_table* CoiTable) { @@ -98,5 +109,5 @@ ******************************************************************************/ -int Dbg_SatCheck(char * forceAssigName, char * cnfFileName +int Dbg_SatCheck(char * forceAssigName, char * cnfFileName,int verbose ) { @@ -138,4 +149,5 @@ sat_Main(cm); +if(verbose){ if(cm->status == SAT_UNSAT) { if(cm->option->forcedAssignArr) @@ -154,4 +166,5 @@ sat_FreeManager(cm); } +} return cm->status; } @@ -192,2 +205,34 @@ } +/**Function******************************************************************** + + Synopsis [Return the default value of a Node] + + Description [Given a table of a node , return its default value if it exists + else -1 This function only work for binary gate with only one default + value.] + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int Dbg_GetDefaultValue(Tbl_Table_t * table) +{ + Tbl_Entry_t * defEntry; + int defIndex; + lsList * rangeList; + Tbl_TableForEachDefaultEntry(table,defEntry,defIndex) + { + rangeList = Tbl_EntryReadList(defEntry); + int length = lsLength(rangeList); + if ( length != 1) + return -1; + Tbl_Range_t * range; + int valDefault; + lsGen gen; + Tbl_EntryForEachValue(defEntry,valDefault,gen,range){ + return Tbl_RangeEnd(range); + } + } +} +