From 5ac8cc95b778ded0ea01d261128ae433e402b30e Mon Sep 17 00:00:00 2001 From: eigold Date: Wed, 7 Jun 2017 19:19:16 -0400 Subject: [PATCH] fixed one of the problems with conversion of verilog to internal repres. of ic3 --- src/ic3/c0ex.cc | 30 ++++++++++-- src/ic3/ebmc_ic3_interface.hh | 6 ++- src/ic3/m1ain.cc | 4 +- src/ic3/m2ethods.hh | 1 + src/ic3/r0ead_input.cc | 25 ++++++---- src/ic3/r1ead_input.cc | 3 ++ src/ic3/r4ead_input.cc | 5 +- src/ic3/r6ead_input.cc | 1 + src/ic3/r7ead_input.cc | 86 +++++++++++++++++++++++++++-------- src/ic3/v0erify.cc | 1 + 10 files changed, 128 insertions(+), 34 deletions(-) diff --git a/src/ic3/c0ex.cc b/src/ic3/c0ex.cc index 0bb080017..de94ba292 100644 --- a/src/ic3/c0ex.cc +++ b/src/ic3/c0ex.cc @@ -59,6 +59,9 @@ bool CompInfo::check_one_state_cex() add_bad_states(Gen_sat); + // add constraints + accept_constrs(Gen_sat); + bool sat_form = check_sat1(Gen_sat); bool ok = true; @@ -157,13 +160,34 @@ void CompInfo::add_neg_prop(SatSolver &Slvr) accept_new_clause(Slvr,C); } /* end of function add_neg_prop */ -/*===================================== +/*================================== - A D D _ B A D _ S T A T E S + A D D _ B A D _ S T A T E S - ====================================*/ + ================================*/ void CompInfo::add_bad_states(SatSolver &Slvr) { add_neg_prop(Slvr); } /* end of function add_bad_states */ + +/*=================================== + + A C C E P T _ C O N S T R S + + ==================================*/ +void CompInfo::accept_constrs(SatSolver &Slvr) +{ + for (size_t i=0; i < Constr_ilits.size(); i++) { + CLAUSE U; + U.push_back(Constr_ilits[i]); + accept_new_clause(Slvr,U); + } + + SCUBE::iterator pnt; + for (pnt = Constr_nilits.begin(); pnt != Constr_nilits.end(); pnt++) { + CLAUSE U; + U.push_back(*pnt); + accept_new_clause(Slvr,U); + } +} /* end of function add_bad_states */ diff --git a/src/ic3/ebmc_ic3_interface.hh b/src/ic3/ebmc_ic3_interface.hh index ec48ef74a..11169996b 100644 --- a/src/ic3/ebmc_ic3_interface.hh +++ b/src/ic3/ebmc_ic3_interface.hh @@ -43,7 +43,7 @@ public: void print_lit1(unsigned var,bool sign); void print_lit2(unsigned var,bool sign); void print_nodes(); - void print_var_map(); + void print_var_map(std::ostream &out); void form_orig_names(); void form_neg_orig_name(CCUBE &Name,literalt &next_lit); bool form_orig_name(CCUBE &Name,literalt &lit,bool subtract = false); @@ -58,6 +58,10 @@ public: void store_constraints(const std::string &fname); void read_constraints(const std::string &fname); void add_pseudo_inps(Circuit *N); + void print_lit(std::ostream& out,literalt a); + std::string print_string(const irep_idt &id); + void add_verilog_conv_constrs(); + protected: netlistt netlist; diff --git a/src/ic3/m1ain.cc b/src/ic3/m1ain.cc index 1b6086748..65e2ba3ea 100644 --- a/src/ic3/m1ain.cc +++ b/src/ic3/m1ain.cc @@ -80,9 +80,9 @@ int ic3_enginet::operator()() orig_names = false; // print_nodes(); - // print_var_map(); + // print_var_map(std::cout); read_ebmc_input(); - //print_blif3("tst.blif",Ci.N); + // print_blif3("tst.blif",Ci.N); if (cmdline.isset("aiger")) { printf("converting to aiger format\n"); Ci.print_aiger_format(); diff --git a/src/ic3/m2ethods.hh b/src/ic3/m2ethods.hh index a8fec08b5..0473f4504 100644 --- a/src/ic3/m2ethods.hh +++ b/src/ic3/m2ethods.hh @@ -187,6 +187,7 @@ void print_files(char *root); int init_ind_cls(); void form_nxt_cube(CUBE &Nxt_cube,CLAUSE &C); int push_on_the_fly(int last_ind,CLAUSE &C,char st_desc); +void accept_constrs(SatSolver &Slvr); // // form CNF formulas void add_or_gate_cubes(DNF &F,int gate_ind,int shift); diff --git a/src/ic3/r0ead_input.cc b/src/ic3/r0ead_input.cc index 5a7fbae2d..767bf1a51 100644 --- a/src/ic3/r0ead_input.cc +++ b/src/ic3/r0ead_input.cc @@ -137,10 +137,6 @@ void ic3_enginet::form_inputs() } /* end of function form_inputs */ - - - - /*================================= F O R M _ T A B L E @@ -189,10 +185,6 @@ void CompInfo::form_max_pres_svar() { max_pres_svar = max; } /* end of function form_max_pres_svar */ - - - - /*=================================== F O R M _ V A R _ N U M S @@ -209,3 +201,20 @@ void CompInfo::form_var_nums() max_num_vars = max_num_vars0 + num_prop_vars; // we need to take into account // that property needs to be specified in two time frames } /* end of function form_var_nums */ + +/*================================================ + + A D D _ V E R I L O G _ C O N V _ C O N S T R S + + ================================================*/ +void ic3_enginet::add_verilog_conv_constrs() +{ + + for(literalt lit : netlist.constraints) { + if (lit.is_constant()) continue; + std::cout << "constraint literal " << lit.get() << "\n"; + Ci.Init_clits.insert(lit.get()); + } + + +} /* end of function add_verlig_conv_constrs */ diff --git a/src/ic3/r1ead_input.cc b/src/ic3/r1ead_input.cc index 39b2b9b02..a9633aef2 100644 --- a/src/ic3/r1ead_input.cc +++ b/src/ic3/r1ead_input.cc @@ -63,6 +63,9 @@ void ic3_enginet::find_prop_lit() if (prop_l.is_false()) Ci.const_flags = Ci.const_flags | 1; else if (prop_l.is_true()) Ci.const_flags = Ci.const_flags | 2; + + // print_lit(std::cout,prop_l); + // printf("\n"); } /* end of function find_prop_lit */ diff --git a/src/ic3/r4ead_input.cc b/src/ic3/r4ead_input.cc index 8a7a7a9cf..d9abcf276 100644 --- a/src/ic3/r4ead_input.cc +++ b/src/ic3/r4ead_input.cc @@ -21,6 +21,8 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com #include "m0ic3.hh" #include "ebmc_ic3_interface.hh" + + /*========================================= U P D _ G A T E _ C O N S T R S @@ -84,6 +86,7 @@ int CompInfo::upd_gate_constr_tbl(int lit,int gate_ind) void ic3_enginet::store_constraints(const std::string &fname) { + add_verilog_conv_constrs(); if (Ci.constr_flag == false) return; read_constraints(fname); @@ -241,7 +244,7 @@ void ic3_enginet::gen_ist_lits(bvt &Ist_lits) continue; if (var_num >= Nodes.size()) { p(); - printf("var_num = %d\n",var_num); + printf("var_num = %zd\n",var_num); printf("Nodes.size() = %zu\n",Nodes.size()); exit(100); } diff --git a/src/ic3/r6ead_input.cc b/src/ic3/r6ead_input.cc index 3c4bdb1cf..dc3175f34 100644 --- a/src/ic3/r6ead_input.cc +++ b/src/ic3/r6ead_input.cc @@ -152,6 +152,7 @@ void ic3_enginet::form_orig_names() void ic3_enginet::print_nodes() { + printf("\n----- Nodes ------\n"); aigt::nodest &Nodes = netlist.nodes; for (size_t i=0; i <= Nodes.size(); i++) { aigt::nodet &Nd = Nodes[i]; diff --git a/src/ic3/r7ead_input.cc b/src/ic3/r7ead_input.cc index e131d1263..8b53ec6b6 100644 --- a/src/ic3/r7ead_input.cc +++ b/src/ic3/r7ead_input.cc @@ -23,37 +23,85 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com #include #include "ebmc_ic3_interface.hh" + /*===================================== P R I N T _ V A R _ M A P - =====================================*/ -void ic3_enginet::print_var_map() + =====================================*/ +void ic3_enginet::print_var_map(std::ostream &out) { - var_mapt &vm = netlist.var_map; + printf("\n----- Var Map ------\n"); + var_mapt &vm = netlist.var_map; for(var_mapt::mapt::const_iterator it=vm.map.begin(); - it!=vm.map.end(); it++) { - const var_mapt::vart &var=it->second; - if (var.is_input()) printf("input: "); - else if (var.is_latch()) printf("latch: "); - else if (var.is_nondet()) printf("nondet: "); - else if (var.is_wire()) printf("wire:" ); - else assert(false); - - for (size_t j=0; j < var.bits.size(); j++) { - if (j > 0) printf(", "); - literalt lit =var.bits[j].current; - unsigned lit_val = lit.get(); - printf("[%zu] = %u",j,lit_val); + it!=vm.map.end(); it++) + { + const var_mapt::vart &var=it->second; + + for(std::size_t i=0; ifirst; + if(var.bits.size()!=1) out << "[" << i << "]"; + out << "="; + + literalt l_c=var.bits[i].current; + + if(l_c.is_true()) + out << "true"; + else if(l_c.is_false()) + out << "false"; + else + { + if(l_c.sign()) out << "!"; + out << l_c.var_no(); + } + + if(var.vartype==var_mapt::vart::vartypet::LATCH) + { + out << "->"; + + literalt l_n=var.bits[i].next; + + if(l_n.is_true()) + out << "true"; + else if(l_n.is_false()) + out << "false"; + else + { + if(l_n.sign()) out << "!"; + out << l_n.var_no(); + } + } + + out << " "; + + switch(var.vartype) + { + case var_mapt::vart::vartypet::INPUT: out << "(input)"; break; + case var_mapt::vart::vartypet::LATCH: out << "(latch)"; break; + case var_mapt::vart::vartypet::NONDET: out << "(nondet)"; break; + case var_mapt::vart::vartypet::WIRE: out << "(wire)"; break; + case var_mapt::vart::vartypet::OUTPUT:out << "(output)"; break; + case var_mapt::vart::vartypet::UNDEF: out << "(?)"; break; + } + + out << '\n'; + } } - printf("\n"); - } + + out << '\n' + << "Total no. of variable bits: " << vm.reverse_map.size() << '\n' + << "Total no. of latch bits: " << vm.latches.size() << '\n' + << "Total no. of nondet bits: " << vm.nondets.size() << '\n' + << "Total no. of input bits: " << vm.inputs.size() << '\n' + << "Total no. of output bits: " << vm.outputs.size() << '\n'; + -} /* end of function print_var_map */ + } /* end of function print_var_map */ /*========================================= A D D _ P S E U D O _ I N P S diff --git a/src/ic3/v0erify.cc b/src/ic3/v0erify.cc index 03f6947cb..0119292b0 100644 --- a/src/ic3/v0erify.cc +++ b/src/ic3/v0erify.cc @@ -161,6 +161,7 @@ bool CompInfo::ver_ini_states(CNF &H) accept_new_clauses(Gen_sat,Ist); + accept_constrs(Gen_sat); bool ok = ver_prop(); if (!ok) return(false);