From e30fb54324e8435ca9be48f067d76dc0cd8447a2 Mon Sep 17 00:00:00 2001 From: eigold Date: Sat, 3 Jun 2017 17:25:53 -0400 Subject: [PATCH] added code related to processing verilog files --- src/ic3/ebmc_ic3_interface.hh | 4 +++- src/ic3/r0ead_input.cc | 8 ++++--- src/ic3/r1ead_input.cc | 2 ++ src/ic3/r3ead_input.cc | 17 +++++++++++--- src/ic3/r4ead_input.cc | 43 +++++++++++++++++++++++++++++++---- src/ic3/r6ead_input.cc | 2 +- src/ic3/r7ead_input.cc | 35 ++++++++++++++++++++++++++++ src/ic3/seq_circ/a2dd_gate.cc | 1 + 8 files changed, 100 insertions(+), 12 deletions(-) diff --git a/src/ic3/ebmc_ic3_interface.hh b/src/ic3/ebmc_ic3_interface.hh index e082a56d9..9fb97e8e0 100644 --- a/src/ic3/ebmc_ic3_interface.hh +++ b/src/ic3/ebmc_ic3_interface.hh @@ -1,5 +1,6 @@ typedef std::vector GateNames; typedef std::map LatchVal; +typedef std::map 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; diff --git a/src/ic3/r0ead_input.cc b/src/ic3/r0ead_input.cc index e7703d050..5a7fbae2d 100644 --- a/src/ic3/r0ead_input.cc +++ b/src/ic3/r0ead_input.cc @@ -75,9 +75,9 @@ 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(); @@ -85,6 +85,7 @@ void ic3_enginet::form_circ_from_ebmc() 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); diff --git a/src/ic3/r1ead_input.cc b/src/ic3/r1ead_input.cc index 0563d6609..c604c29e0 100644 --- a/src/ic3/r1ead_input.cc +++ b/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); } } diff --git a/src/ic3/r3ead_input.cc b/src/ic3/r3ead_input.cc index 0b00cbec8..47280a929 100644 --- a/src/ic3/r3ead_input.cc +++ b/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); diff --git a/src/ic3/r4ead_input.cc b/src/ic3/r4ead_input.cc index e0b1039e5..8a7a7a9cf 100644 --- a/src/ic3/r4ead_input.cc +++ b/src/ic3/r4ead_input.cc @@ -165,16 +165,35 @@ 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); @@ -182,7 +201,14 @@ void ic3_enginet::ebmc_form_latches() 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; } diff --git a/src/ic3/r6ead_input.cc b/src/ic3/r6ead_input.cc index bd70aedd3..3c4bdb1cf 100644 --- a/src/ic3/r6ead_input.cc +++ b/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); diff --git a/src/ic3/r7ead_input.cc b/src/ic3/r7ead_input.cc index 61effcd10..706293268 100644 --- a/src/ic3/r7ead_input.cc +++ b/src/ic3/r7ead_input.cc @@ -23,6 +23,41 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com #include #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 diff --git a/src/ic3/seq_circ/a2dd_gate.cc b/src/ic3/seq_circ/a2dd_gate.cc index 13fd39477..43a0520d0 100644 --- a/src/ic3/seq_circ/a2dd_gate.cc +++ b/src/ic3/seq_circ/a2dd_gate.cc @@ -40,6 +40,7 @@ int assign_input_pin_number1(std::map &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 */