Changeset 42

Timestamp:

Jan 13, 2012, 6:32:51 PM (12 years ago)

Author:

cecile

Message:

Fault candidates OK

Location:

vis_dev/vis-2.3/src/debug

Files:

• debug.c (modified) (3 diffs)
• debug.h (modified) (1 diff)
• debugAbnormal.c (modified) (5 diffs)
• debugInt.h (modified) (1 diff)
• debugUtilities.c (modified) (5 diffs)

vis_dev/vis-2.3/src/debug/debug.c

@@ -191 +191 @@
 array_t          * LTLformulaArray;
 char             * ltlFileName     = NIL(char);
-
+array_t          * faultNodes = array_alloc(Ntk_Node_t*,0);
 
 /*
@@ -286 +286 @@
    
 
-        array_t           *objClause = NIL(array_t);
+        array_t *objClause = NIL(array_t);
         objClause = array_alloc(int, 0);   
         array_insert_last(int, objClause, noLoopIndex);
@@ -295 +295 @@
     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;
  

vis_dev/vis-2.3/src/debug/debug.h

@@ -134 +134 @@
 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);
 
 

vis_dev/vis-2.3/src/debug/debugAbnormal.c

@@ -44 +44 @@
   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 +68 @@
 
                 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 +84 @@
                 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 +96 @@
                 //the new row
                 int r = Tbl_TableAddRow(table);
-
+        
                 int colNum;
             for (colNum = 0; colNum < Tbl_TableReadNumInputs(table); colNum++) {
@@ -104 +106 @@
                     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);
+        }
           }
         }

vis_dev/vis-2.3/src/debug/debugInt.h

@@ -85 +85 @@
 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***************************************************************/

vis_dev/vis-2.3/src/debug/debugUtilities.c

@@ -1 +1 @@
 #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 +109 @@
 ******************************************************************************/
 
-int Dbg_SatCheck(char * forceAssigName, char * cnfFileName
+int Dbg_SatCheck(char * forceAssigName, char * cnfFileName,int verbose
 )
 {
@@ -138 +149 @@
    sat_Main(cm);
 
+if(verbose){
    if(cm->status == SAT_UNSAT) {
     if(cm->option->forcedAssignArr)
@@ -154 +166 @@
     sat_FreeManager(cm);
   }
+}
 return cm->status;
 }
@@ -192 +205 @@
 
 }
+/**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);
+    }
+  }
+}
+