Changeset 44 for vis_dev/vis-2.3/src/debug/debugAbnormal.c

Timestamp:

Jan 24, 2012, 3:41:23 PM (13 years ago)

Author:

cecile

Message:

abnormal predicate done

File:

• vis_dev/vis-2.3/src/debug/debugAbnormal.c (modified) (11 diffs)

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

@@ -19 +19 @@
         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 +46 @@
   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 +56 @@
 ******************************************************************************/
 
-void Dbg_AddAbnormalPredicatetoNetwork(Dbg_Abnormal_t* abnormal ) /*abnormal struct*/
+void Dbg_AddAbnormalPredicatetoNetwork(Dbg_Abnormal_t* abnormal,array_t* excludes)
 {
 
@@ -61 +64 @@
   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 +131 @@
                  Tbl_TableWriteBlifMvToFile(table,0,vis_stdout);
         }
+      }
           }
         }
@@ -132 +139 @@
  (void *) abnormal);
 }
+
 /**Function********************************************************************
  
@@ -289 +297 @@
   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 +313 @@
 bAig_Manager_t   * manager,
 st_table * nodeToMvfAigTable,
+int k,
 BmcCnfClauses_t *cnfClauses)
 {
@@ -315 +325 @@
    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 +333 @@
     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 +346 @@
     }
     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;