Changeset 35

Timestamp:

Jan 3, 2012, 11:12:40 AM (13 years ago)

Author:

cecile

Message:

modify mv table

Location:

vis_dev/vis-2.3/src/debug

Files:

• debug.c (modified) (4 diffs)
• debug.h (modified) (1 diff)
• debug.make (modified) (1 diff)
• debugUtilities.c (modified) (1 diff)

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

@@ -7 +7 @@
   Synopsis    [Debug package initialization, ending, and the command debug]
 
-  Author      [Originated from SIS.]
+  Author      [Cecile B.]
 
   Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
@@ -61 +61 @@
 /*---------------------------------------------------------------------------*/
 
+static int CommandSatDebug(Hrc_Manager_t ** hmgr, int argc, char ** argv);
 static int CommandDebug(Hrc_Manager_t ** hmgr, int argc, char ** argv);
 static int CommandTransition(Hrc_Manager_t ** hmgr,int  argc, char ** argv);
+static int CommandCreateAbnormal(Hrc_Manager_t ** hmgr,int  argc, char ** argv);
 
 
@@ -88 +90 @@
    * underscore, the command will be listed under "help -a" but not "help".
    */
-  Cmd_CommandAdd("_debug_test", CommandDebug, /* doesn't changes_network */ 0);
-  Cmd_CommandAdd("_transition",  CommandTransition,      0);
+  Cmd_CommandAdd("_debug_test",  CommandDebug, /* doesn't changes_network */ 0);
+  Cmd_CommandAdd("_transition",  CommandTransition, 1);
+  Cmd_CommandAdd("_sat_debug",   CommandSatDebug, 0);
+  Cmd_CommandAdd("_createAbn",   CommandCreateAbnormal, 1);
 
 }
@@ -122 +126 @@
 /*---------------------------------------------------------------------------*/
 
+
+static int CommandCreateAbnormal(Hrc_Manager_t ** hmgr,int  argc, char ** argv)
+{
+  Ntk_Network_t * ntk;
+  ntk = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
+  if (ntk == NIL(Ntk_Network_t)) {
+        (void) fprintf(vis_stdout, "** abn error: No network\n");
+        return 1;
+  }
+  lsGen gen;
+  Ntk_Node_t* node;
+
+  (void) fprintf(vis_stdout, "** NODE **\n");
+  Ntk_NetworkForEachNode(ntk,gen,node){
+          if(Ntk_NodeTestIsCombinational(node)){
+                if(Ntk_NodeReadNumFanins(node) > 1 && Ntk_NodeReadNumFanouts(node)> 0)
+                {
+                  if(strcmp(Ntk_NodeReadName(node),"_n2")==0)
+                  {
+                        char * nodeName = util_strsav(Ntk_NodeReadName(node));
+                printf("%s \n",  nodeName); 
+                        (void) fprintf(vis_stdout, "** read table\n");
+                        Tbl_Table_t    *table =  Ntk_NodeReadTable(node);
+
+                        Tbl_TableWriteBlifMvToFile(table,2,vis_stdout);
+                        // Build new variables abnormal  and  input
+                        //abn
+                        char * abnName = (char *) malloc(strlen(nodeName) + 5);
+                        sprintf(abnName,"abn_%s",Ntk_NodeReadName(node));
+                        Var_Variable_t * abn = Var_VariableAlloc(NIL(Hrc_Node_t),abnName);
+                        Ntk_Node_t * newNode = Ntk_NodeCreateInNetwork(ntk, abnName,abn);
+                        Ntk_NodeDeclareAsPrimaryInput(newNode);
+                        //new free inputs
+                        char * iName = (char *) malloc(strlen(nodeName) + 3);
+                        sprintf(iName,"i_%s",Ntk_NodeReadName(node));
+                        Var_Variable_t * i = Var_VariableAlloc(NIL(Hrc_Node_t),iName);
+                        Ntk_Node_t * newNode2 = Ntk_NodeCreateInNetwork(ntk, iName, i);
+                        Ntk_NodeDeclareAsPrimaryInput(newNode2);
+                        //Add in the table
+                        Tbl_TableAddColumn(table,abn,0);
+                        int abnIndex = Tbl_TableReadVarIndex(table, abn, 0);
+                        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++){
+                                Tbl_Entry_t *abnEntry = Tbl_EntryAlloc(Tbl_EntryNormal_c);
+                                Tbl_EntrySetValue(abnEntry,0,0);
+                                Tbl_TableSetEntry(table, abnEntry, rowNum, abnIndex, 0);
+                                Tbl_Entry_t *iEntry = Tbl_EntryAlloc(Tbl_EntryNormal_c);
+                                Tbl_EntrySetValue(iEntry,0,1);
+                                Tbl_TableSetEntry(table, iEntry, rowNum, iIndex, 0);
+                        }
+                        //the new row
+                        int r = Tbl_TableAddRow(table);
+
+                        int colNum;
+                    for (colNum = 0; colNum < Tbl_TableReadNumInputs(table); colNum++) {
+                                Tbl_Entry_t * entry = Tbl_EntryAlloc(Tbl_EntryNormal_c);
+                                printf("entry : colNum %d \n",colNum);
+                                if(colNum == abnIndex || colNum == iIndex)
+                                        Tbl_EntrySetValue(entry,1,1);
+                                else
+                                        Tbl_EntrySetValue(entry,0,1);
+                            Tbl_TableSetEntry(table, entry, r, colNum, 0);
+                        }
+                        for (colNum = 0; colNum < Tbl_TableReadNumOutputs(table); colNum++){
+                                Tbl_Entry_t * entry = Tbl_EntryAlloc(Tbl_EntryNormal_c);
+                                Tbl_EntrySetValue(entry,1,1);
+                            Tbl_TableSetEntry(table, entry, r, colNum, 1);
+                        }
+                         printf("---------------\n");
+                         Tbl_TablePrintStats(table, vis_stdout);
+                         Tbl_TableWriteBlifMvToFile(table,0,vis_stdout);
+                         free(abnName);
+                         free(iName);
+                  }
+                }
+         }
+  }
+  // TODO
+  //Remplacer l'ancien network par le nouveau 
+}
+/**Function********************************************************************
+
+  Synopsis    [Implements the _sat_debug command.]
+
+  CommandName [_sat_debug]
+
+  CommandSynopsis [locate faulty candidates]
+
+  CommandArguments [\[-h\] \[-v\]]
+  
+  CommandDescription [This command compute the fault candidates of a given
+  properties.<p>
+
+  Command options:<p>  
+
+  <dl>
+  <dt> -h
+  <dd> Print the command usage.
+  </dl>
+
+  <dt> -v
+  <dd> Verbose mode.
+  </dl>
+  ]
+
+  SideEffects []
+
+******************************************************************************/
+
+
+static int 
+CommandSatDebug(
+Hrc_Manager_t ** hmgr, 
+int argc, 
+char ** argv){
+int            c,i;
+int            verbose = 0;              /* default value */
+BmcOption_t  *options = BmcOptionAlloc();
+Ntk_Network_t * network;
+bAig_Manager_t    *manager;
+
+
+/*
+ * Parse command line options.
+ */
+util_getopt_reset();
+while ((c = util_getopt(argc, argv, "vh:m:k:o:")) != EOF) {
+  switch(c) {
+    case 'v':
+      verbose = 1;
+          options->verbosityLevel =  verbose;
+      break;
+    case 'h':
+      goto usage;
+        case 'm':
+      for (i = 0; i < strlen(util_optarg); i++) {
+                if (!isdigit((int)util_optarg[i])) {
+                        goto usage;
+                }
+      }
+      options->minK = atoi(util_optarg);
+      break;
+    case 'k':
+      for (i = 0; i < strlen(util_optarg); i++) {
+                if (!isdigit((int)util_optarg[i])) {
+                        goto usage;
+                }
+      }
+          options->maxK = atoi(util_optarg);
+          break;
+        case 'o':
+      options->cnfFileName = util_strsav(util_optarg);
+      break;    
+
+    default:
+      goto usage;
+  }
+}
+ if (options->minK > options->maxK){
+    (void) fprintf(vis_stderr, "** bmc error: value for -m option must not be greater than vlaue for -k option\n");    
+    goto usage;
+  }
+
+if (verbose) {
+  (void) fprintf(vis_stdout, "The _sat_debug command is under construction.\n");
+}
+ /* create SAT Solver input file */
+ if (options->cnfFileName == NIL(char)) {
+    options->satInFile = BmcCreateTmpFile(); 
+}
+ else {
+    options->satInFile = options->cnfFileName;
+ }
+
+/* create SAT Solver output file */
+options->satOutFile = BmcCreateTmpFile();
+if (options->satOutFile == NIL(char)){
+  BmcOptionFree(options);
+ (void) fprintf(vis_stdout, "The _sat_debug problem.\n");
+  return 1;
+}
+
+options->verbosityLevel =  1;
+//options->satSolver
+//options->clauses 
+
+ /*
+   * Read the network
+   */
+  network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
+  if (network == NIL(Ntk_Network_t)) {
+    (void) fprintf(vis_stdout, "** bmc error: No network\n");
+    BmcOptionFree(options);
+    return 1;
+  }
+  manager = Ntk_NetworkReadMAigManager(network);
+  if (manager == NIL(mAig_Manager_t)) {
+    (void) fprintf(vis_stdout, "** bmc error: run build_partition_maigs command first\n");
+    BmcOptionFree(options);
+    return 1;
+  }
+  /*
+    We need the bdd when building the transition relation of the automaton
+  */
+  if(options->inductiveStep !=0){
+    Fsm_Fsm_t *designFsm = NIL(Fsm_Fsm_t);
+ 
+    designFsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
+    if (designFsm == NIL(Fsm_Fsm_t)) {
+         (void) fprintf(vis_stdout, "The _sat_debug : Build FSM.\n");
+      return 1;
+    }
+  }
+
+ /*
+    Compute the cone of influence 
+        here a list of state variables (latches)
+  */
+        st_table        *CoiTable =  generateAllLatches(network);
+  /*
+      Generate clauses for each time frame.  This is the old way of generating
+      clauses in BMC.
+    */
+    st_table          *nodeToMvfAigTable = NIL(st_table);  /* node to mvfAig */
+        BmcCnfClauses_t   *cnfClauses = NIL(BmcCnfClauses_t);
+    FILE *cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0); 
+        /*
+    nodeToMvfAigTable maps each node to its multi-function And/Inv graph
+    */
+        nodeToMvfAigTable =
+        (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
+        assert(nodeToMvfAigTable != NIL(st_table));
+
+        if(verbose)
+        {       
+                (void) fprintf(vis_stdout, "------ node to mvfaig ----\n");
+                printLatch(nodeToMvfAigTable);
+                (void) fprintf(vis_stdout, "------      COI       ----\n");
+                printLatch(CoiTable);
+                (void) fprintf(vis_stdout, "--------------------------\n");
+    }
+    /*
+      Create a clause database
+     */
+    cnfClauses = BmcCnfClausesAlloc();
+    /*
+      Generate clauses for an initialized path of length k
+     */
+    BmcCnfGenerateClausesForPath(network, 0, options->maxK, BMC_INITIAL_STATES,
+                                 cnfClauses, nodeToMvfAigTable, CoiTable);
+         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));
+        
+    
+        BmcWriteClauses(manager, cnfFile, cnfClauses, options);
+fclose(cnfFile);
+BmcCnfClausesFree(cnfClauses);
+BmcOptionFree(options);
+return 0;
+  usage:
+  (void) fprintf(vis_stderr, "usage: _sat_debug [-h] [-v] [-k max length] [-m \
+  minimum length] [-o cnf_file]\n");
+  (void) fprintf(vis_stderr, "   -h\t\tprint the command usage\n");
+  (void) fprintf(vis_stderr, "   -v\t\tverbose\n");
+  (void) fprintf(vis_stderr, "   -m \tminimum length of counterexample to be checked (default is 0)\n");  
+  (void) fprintf(vis_stderr, "   -k \tmaximum length of counterexample to be checked (default is 1)\n");
+  (void) fprintf(vis_stderr, "   -o <cnf_file> contains CNF of the counterexample\n");  
+  return 1;             /* error exit */
+
+}
 /**Function********************************************************************
 

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

@@ -83 +83 @@
 /*---------------------------------------------------------------------------*/
 
-
+void printLatch(st_table* CoiTable);
+st_table * generateAllLatches(Ntk_Network_t * ntk);
 void mdd_GetState_Values(mdd_manager *mgr, mdd_t * top, FILE * f);
 EXTERN void Debug_Init(void);

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

@@ -1 @@
-CSRC += debug.c
+CSRC += debug.c debugUtilities.c
 HEADERS += debug.h debugInt.h
 

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

@@ -1 @@
-#include "Debug.h"
+#include "debug.h"
+void printLatch(st_table* CoiTable)
+{
+// COI contents
+   printf("*** COI ***\n");
+   st_generator    *stGen;
+   Ntk_Node_t * latch;
+   st_foreach_item(CoiTable, stGen, &latch, NULL) {
+        printf("%s\n",Ntk_NodeReadName(latch)); 
+  }
+}
+
+
+st_table * generateAllLatches(Ntk_Network_t * ntk)
+{
+    st_table        *CoiTable = st_init_table(st_ptrcmp, st_ptrhash);
+        lsGen           gen ;
+        Ntk_Node_t              *node;
+
+        Ntk_NetworkForEachNode(ntk,gen, node){
+                if (Ntk_NodeTestIsLatch(node)){
+                        st_insert(CoiTable, (char *) node, Ntk_NodeReadName(node));
+                }
+        }
+        return CoiTable;
+
+}
+
 
 void mdd_GetState_Values(