Changeset 44

Timestamp:

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

Author:

cecile

Message:

abnormal predicate done

Location:

vis_dev/vis-2.3/src/debug

Files:

• debug.c (modified) (10 diffs)
• debug.h (modified) (3 diffs)
• debugAbnormal.c (modified) (11 diffs)
• debugInt.h (modified) (2 diffs)
• debugUtilities.c (modified) (1 diff)

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

@@ -132 +132 @@
 {
   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 <subsystemName> \texclude the abnormal predicate\
+  for this subssytem\n");
+  return 1;
+}
+
 /**Function********************************************************************
 
@@ -190 +212 @@
 array_t          * formulaArray;
 array_t          * LTLformulaArray;
-char             * ltlFileName     = NIL(char);
 array_t          * faultNodes = array_alloc(Ntk_Node_t*,0);
 
@@ -201 +222 @@
 
 
-printf("MAX K %d", options->maxK);
 
 if (verbose) {
@@ -252 +272 @@
 }
 Ctlsp_Formula_t *ltlFormula  = array_fetch(Ctlsp_Formula_t *, LTLformulaArray, 0);
-
 
 
@@ -283 +302 @@
     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 +317 @@
     assert(nodeToMvfAigTable != NIL(st_table));
 
-    Dbg_InitAbn(abn,manager, nodeToMvfAigTable,cnfClauses);
+    Dbg_InitAbn(abn,manager, nodeToMvfAigTable,k,cnfClauses);
 
     //loop abnormal
@@ -305 +324 @@
     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 +371 @@
                 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 +385 @@
 array_free(faultNodes);
 return 0;
- 
-}
+}
+
 /**Function********************************************************************
 
@@ -420 +459 @@
    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); 
   }
   

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

@@ -126 +126 @@
 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 +134 @@
 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 +141 @@
 
 
-
 /**AutomaticEnd***************************************************************/
 

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;

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

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

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

@@ -236 +236 @@
   }
 }
-
+/**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;
+}
+