Changeset 102 for vis_dev/vis-2.3/src/bmc

Timestamp:

Jul 19, 2012, 2:40:12 PM (12 years ago)

Author:

cecile

Message:

add write_cnf of design cmd

File:

• vis_dev/vis-2.3/src/bmc/bmcCmd.c (modified) (3 diffs)

vis_dev/vis-2.3/src/bmc/bmcCmd.c

@@ -48 +48 @@
 /*static*/ BmcOption_t * ParseBmcOptions(int argc, char **argv);
 static int CommandBmc(Hrc_Manager_t ** hmgr, int argc, char ** argv);
+static int CommandWriteCnf(Hrc_Manager_t ** hmgr, int argc, char ** argv);
 static void TimeOutHandle(void);
 static void DispatchBmcCommand(Ntk_Network_t *network, Ctlsp_Formula_t *ltlFormula, array_t *constraintArray, BmcOption_t *options);
@@ -74 +75 @@
   
   Cmd_CommandAdd("cnf_sat", CommandCnfSat, /* doesn't change network */  0); 
+  Cmd_CommandAdd("write_cnf", CommandWriteCnf, /* doesn't change network */  0); 
 }
 
@@ -1267 +1269 @@
 }/* CommandBddSat() */
 #endif
+
+
+int CommandWriteCnf(Hrc_Manager_t ** hmgr, int argc, char ** argv)
+{
+  Ntk_Network_t     *network;
+  bAig_Manager_t    *manager;
+  array_t           *formulaArray;
+  array_t           *LTLformulaArray;
+  char              * outFileName = NIL(char); 
+  char              * ltlFileName = NIL(char); 
+  FILE * ltlFile;
+  FILE * outFile;
+  int c,i;
+  int maxK = 0;
+  st_table          *allLatches;
+  BmcCnfClauses_t   *cnfClauses = NIL(BmcCnfClauses_t);
+
+
+  outFile = vis_stdout ; 
+  // Parse option
+  util_getopt_reset();
+  while ((c = util_getopt(argc, argv, "f:o:k:h")) != EOF) {
+    switch(c) {
+      case 'h':
+        goto usage;
+      case 'o' :
+        outFileName = strdup(util_optarg);
+    outFile = Cmd_FileOpen(outFileName, "w", NIL(char *), 0); 
+        break;
+      case 'f' :
+        ltlFileName = strdup(util_optarg);
+        break;
+    case 'k':
+      for (i = 0; i < strlen(util_optarg); i++) {
+        if (!isdigit((int)util_optarg[i])) {
+          goto usage;
+        }
+      }
+      maxK = atoi(util_optarg);
+      break;
+
+        break;
+      default:
+        goto usage;
+    }
+  }
+  network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
+  if (network == NIL(Ntk_Network_t)) {
+    (void) fprintf(vis_stdout, "** bmc error: No network\n");
+    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");
+    return 1;
+  }
+   
+    //    Create a clause database
+     
+    cnfClauses = BmcCnfClausesAlloc();
+    // Gnerate clauses for an initialized path of length k
+    // nodeToMvfAigTable Maps each node to its Multi-function And/Inv graph 
+     st_table* nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
+     assert(nodeToMvfAigTable != NIL(st_table));
+      allLatches = st_init_table(st_ptrcmp, st_ptrhash);
+
+     // Get all the latches of the network
+          lsGen           gen ;
+          Ntk_Node_t            *node;
+        Ntk_NetworkForEachNode(network,gen, node){
+                if (Ntk_NodeTestIsLatch(node)){
+                        st_insert(allLatches, (char *) node, (char *) 0);
+                }
+        }
+
+
+    BmcCnfGenerateClausesForPath(network, 0, maxK, BMC_INITIAL_STATES,
+                                 cnfClauses, nodeToMvfAigTable, allLatches);
+
+// If ltl file exists 
+ if(ltlFileName != NIL(char))
+  { 
+    ltlFile =  Cmd_FileOpen(ltlFileName, "r", NIL(char *), 0);
+  formulaArray  = Ctlsp_FileParseFormulaArray(ltlFile);
+  if (formulaArray == NIL(array_t)) {
+    (void) fprintf(vis_stderr,
+                   "** bmc error: error in parsing ltl Fromula from file\n");
+      return 1;
+   }
+    LTLformulaArray = Ctlsp_FormulaArrayConvertToLTL(formulaArray);
+    for (i = 0; i < array_n(LTLformulaArray); i++) { 
+    Ctlsp_Formula_t *ltlFormula     = array_fetch(Ctlsp_Formula_t *,
+                                                  LTLformulaArray, i);
+    BmcGenerateCnfForLtl(network, ltlFormula, 0, maxK, 0, cnfClauses);
+}
+  }
+
+
+// Write Clauses
+
+  st_generator *stGen;
+  char         *name;
+  int          cnfIndex,k;
+
+    st_foreach_item_int(cnfClauses->cnfIndexTable, stGen, &name, &cnfIndex) {
+    fprintf(outFile, "c %s %d\n",name, cnfIndex);
+  }
+  (void) fprintf(outFile, "p cnf %d %d\n", cnfClauses->cnfGlobalIndex-1,
+                 cnfClauses->noOfClauses);
+  if (cnfClauses->clauseArray != NIL(array_t)) {
+    for (i = 0; i < cnfClauses->nextIndex; i++) {
+      k = array_fetch(int, cnfClauses->clauseArray, i);
+      (void) fprintf(outFile, "%d%c", k, (k == 0) ? '\n' : ' ');
+    }
+  }
+ if(outFileName != NIL(char))
+   fclose(outFile);
+   
+   return 1;
+
+   usage:
+  (void) fprintf(vis_stderr, "usage: write_cnf [-h] [-f ltl file] [-o outfile] [k]\n");
+  (void) fprintf(vis_stderr, "   -h \tprint the command usage\n");
+  (void) fprintf(vis_stderr, "   -f <filename> \tto add a ltlfile\n");
+  (void) fprintf(vis_stderr, "   -o <filename> \twrite output in outputfile\n");
+  (void) fprintf(vis_stderr, "   -k <value> \tnumber of unroll steps\n");
+  return 1;
+  
+}