added code related to processing verilog files

Author: eigold

src/ic3/ebmc_ic3_interface.hh

@@ -1,5 +1,6 @@
 typedef std::vector<std::string> GateNames;
 typedef std::map<int,int> LatchVal;
+typedef std::map<int,int> NondetVars;
 //
 class ic3_enginet:public ebmc_baset
 {
@@ -15,6 +16,7 @@ public:
   GateNames Gn;
   literalt prop_l;
   LatchVal Latch_val;
+  NondetVars Nondet_vars;
   bool const0,const1;
   bool orig_names;
 
@@ -54,7 +56,7 @@ public:
   void form_init_constr_lits();
   void store_constraints(const std::string &fname);
   void read_constraints(const std::string &fname);
-
+  void add_pseudo_inps(Circuit *N);
 protected:
   netlistt netlist;
 

src/ic3/r0ead_input.cc

@@ -75,16 +75,17 @@ void ic3_enginet::form_circ_from_ebmc()
   find_prop_lit();
 
   form_latched_gates();
- 
-  form_gates();
 
+  form_gates();
+ 
   CDNF Out_names;
   form_outp_buf(Out_names);
   form_invs();
   Ci.form_consts(N);
 
   add_spec_buffs(N);
 
+  add_pseudo_inps(N);
 
   fill_fanout_lists(N);
   assign_gate_type(N,Out_names,true);
@@ -115,7 +116,8 @@ void ic3_enginet::form_inputs()
     if (var.is_input() == false) continue;
     for (size_t j=0; j < var.bits.size(); j++) {  
       literalt lit =var.bits[j].current;
-      int lit_val = lit.get();    
+      int lit_val = lit.get();
+      //      printf("lit_val = %d\n",lit_val);
       CCUBE Name;
       if (orig_names) {
 	bool ok = form_orig_name(Name,lit);

src/ic3/r1ead_input.cc

@@ -105,6 +105,8 @@ void ic3_enginet::form_latched_gates()
       literalt lit =var.bits[j].current;
       int init_val = Latch_val[lit.var_no()];
       literalt next_lit = var.bits[j].next;
+      // int lit_val = next_lit.get();
+      // printf("next st. var: %d\n",lit_val);
       add_new_latch(Latches,init_val,lit,next_lit);
     }
   }

src/ic3/r3ead_input.cc

@@ -147,7 +147,11 @@ void ic3_enginet::form_gate_pin_names(CDNF &Pin_names,CUBE &Pol,
   literalt gt_lit(node_ind,false);
 
   add_gate_out_name(Pin_names[2],gt_lit,Pol);
-
+  // print_name1(Pin_names[2]);
+  // printf(": "); print_name1(Pin_names[0]);
+  // printf(" "); print_name1(Pin_names[1],true);
+  // printf(" Pin_names[0].size() = %d, Pin_names[1].size() = %d\n",(int) Pin_names[0].size(),
+  // 	 (int) Pin_names[1].size());
 } /* end of function from_gate_pin_names */
 
 /*===============================
@@ -160,10 +164,17 @@ void ic3_enginet::form_gates()
 
   Circuit *N = Ci.N;
   aigt::nodest &Nodes = netlist.nodes;
- 
+
   for (size_t i=0; i <  Nodes.size(); i++) {  
     aigt::nodet &Nd = Nodes[i];
-    if (Nd.is_var()) continue;
+    if (Nd.is_var()) {
+      // printf("skipping a var node\n");
+      // literalt gt_lit(i,false);
+      // unsigned lit_val = gt_lit.get();
+      // printf("lit_val = %u\n",lit_val);
+      // printf("i = %zu\n",i);
+      continue;
+    }
     CDNF Pin_names;
     CUBE Pol;    
     form_gate_pin_names(Pin_names,Pol,i);

src/ic3/r4ead_input.cc

@@ -165,24 +165,50 @@ void ic3_enginet::ebmc_form_latches()
 
   for(var_mapt::mapt::const_iterator it=vm.map.begin();
       it!=vm.map.end(); it++)    {
-    const var_mapt::vart &var=it->second; 
+    const var_mapt::vart &var=it->second;
+    
+    if (var.vartype ==var_mapt::vart::vartypet::NONDET) {
+      assert(var.bits.size() > 0);
+      int val = (var.bits.size() == 1)?1:2;
+      for (size_t i=0; i < var.bits.size(); i++) {
+	literalt lit = var.bits[i].current;
+	int var_num = lit.var_no();
+	Nondet_vars[var_num] = val;
+      }
+      continue;
+    }
+    
     if (var.vartype !=var_mapt::vart::vartypet::LATCH) 
       continue;
 
     for (size_t j=0; j < var.bits.size(); j++) {
       literalt lit =var.bits[j].current;
-      Latch_val[lit.var_no()] = 2; // set the value of the latch to a don't care     
+      int var_num = lit.var_no();
+      Latch_val[var_num] = 2; // set the value of the latch to a don't care
+      //      printf("latch val: %d\n",var_num);
     }
   }
 
+  if (Latch_val.size() == 0) {
+    printf("there are no latches\n");
+    //    printf("Nondet_vars.size() = %d\n",(int) Nondet_vars.size());
+    exit(100);
+  }
   // set initial values
   bvt Ist_lits;
   gen_ist_lits(Ist_lits);
 
   for (size_t i=0; i < Ist_lits.size(); i++) {
     literalt &lit = Ist_lits[i];
     int var_num = lit.var_no();
-    assert(Latch_val.find(var_num) != Latch_val.end());
+    if (Latch_val.find(var_num) == Latch_val.end()) {
+      p();
+      printf("Latch %d is not found\n",var_num);
+      printf("Latch_val.size() = %zu\n",Latch_val.size());
+      printf("Ist_lits.size() = %zu\n",Ist_lits.size());
+      printf("i = %zu\n",i);
+      exit(100);
+    }
     if (lit.sign()) Latch_val[var_num] = 0;
     else Latch_val[var_num] = 1;
   }
@@ -208,15 +234,24 @@ void ic3_enginet::gen_ist_lits(bvt &Ist_lits)
   while (stack.size() > 0) {
 
     literalt lit = stack.back();
+    assert(lit.is_constant() == false);
     size_t var_num = lit.var_no();
     stack.pop_back();
     if (Visited.find(lit) != Visited.end()) 
       continue;
-    assert(var_num < Nodes.size());
+    if (var_num >= Nodes.size()) {
+      p();
+      printf("var_num = %d\n",var_num);
+      printf("Nodes.size() = %zu\n",Nodes.size());
+      exit(100);
+    }
     aigt::nodet &Nd = Nodes[var_num];
 
     if (Nd.is_var()) {
       Ist_lits.push_back(lit);
+      // literalt gt_lit(var_num,false);
+      // unsigned lit_val = gt_lit.get();
+      // printf("init st: lit_val = %u\n",lit_val);
       continue;
     }
 

src/ic3/r6ead_input.cc

@@ -87,7 +87,7 @@ bool ic3_enginet::find_prop(propertyt &Prop)
 
   assert(properties.size() > 0);
 
-  if ((properties.size() == 1) && (Ci.prop_name.size() == 0)) {
+  if ((properties.size() >= 1) && (Ci.prop_name.size() == 0)) {
     Prop = properties.front();
     Ci.prop_name = id2string(Prop.name);
     return(true);

src/ic3/r7ead_input.cc

@@ -23,6 +23,41 @@ Author: Eugene Goldberg, [email protected]
 #include <ebmc/ebmc_base.h>
 #include "ebmc_ic3_interface.hh"
 
+/*=========================================
+
+        A D D _ P S E U D O _ I N P S
+
+  ==========================================*/
+void ic3_enginet::add_pseudo_inps(Circuit *N)
+{
+
+
+  GCUBE &Gate_list = N->Gate_list;
+  for (size_t i=0; i < Gate_list.size();i++) {
+    Gate &G=Gate_list[i];
+    if (G.flags.active) continue;
+    // printf("inactive gate: ");
+    // print_name1(G.Gate_name,true);
+
+    G.func_type = BUFFER;
+    G.gate_type = INPUT;
+    G.flags.active = 1; // mark this input as active 
+    G.flags.output = 0;
+    G.flags.transition = 0;
+    G.flags.output_function = 0;
+    G.flags.feeds_latch = 0;
+    G.level_from_inputs = 0; // set the topological level to 0
+    G.inp_feeds_latch = false;
+ 
+    //   Add it to the circuit
+   
+    N->Inputs.push_back(i);
+    N->ninputs++; // increment the number of inputs
+   
+  }
+
+} /*end of function add_pseudo_inps */
+
 /*=========================================
 
  F O R M _ I N I T _ C O N S T R _ L I T S

src/ic3/seq_circ/a2dd_gate.cc

@@ -40,6 +40,7 @@ int assign_input_pin_number1(std::map<CCUBE,int> &pin_list,
     pin_list[name] = pin_num;
     G.flags.active = 0;
     G.gate_type = UNDEFINED;
+    G.Gate_name = name;
     gate_list.push_back(G); // add one more gate 
   }
   else /* an 'old' pin */