Skip to content

Commit 5ac8cc9

Browse files
eigoldeigold
committed
fixed one of the problems with conversion of verilog to internal repres. of ic3
1 parent 224d738 commit 5ac8cc9

File tree

10 files changed

+128
-34
lines changed

10 files changed

+128
-34
lines changed

‎src/ic3/c0ex.cc

Lines changed: 27 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -59,6 +59,9 @@ bool CompInfo::check_one_state_cex()
5959

6060
add_bad_states(Gen_sat);
6161

62+
// add constraints
63+
accept_constrs(Gen_sat);
64+
6265

6366
bool sat_form = check_sat1(Gen_sat);
6467
bool ok = true;
@@ -157,13 +160,34 @@ void CompInfo::add_neg_prop(SatSolver &Slvr)
157160
accept_new_clause(Slvr,C);
158161
} /* end of function add_neg_prop */
159162

160-
/*=====================================
163+
/*==================================
161164
162-
A D D _ B A D _ S T A T E S
165+
A D D _ B A D _ S T A T E S
163166
164-
====================================*/
167+
================================*/
165168
void CompInfo::add_bad_states(SatSolver &Slvr)
166169
{
167170
add_neg_prop(Slvr);
168171

169172
} /* end of function add_bad_states */
173+
174+
/*===================================
175+
176+
A C C E P T _ C O N S T R S
177+
178+
==================================*/
179+
void CompInfo::accept_constrs(SatSolver &Slvr)
180+
{
181+
for (size_t i=0; i < Constr_ilits.size(); i++) {
182+
CLAUSE U;
183+
U.push_back(Constr_ilits[i]);
184+
accept_new_clause(Slvr,U);
185+
}
186+
187+
SCUBE::iterator pnt;
188+
for (pnt = Constr_nilits.begin(); pnt != Constr_nilits.end(); pnt++) {
189+
CLAUSE U;
190+
U.push_back(*pnt);
191+
accept_new_clause(Slvr,U);
192+
}
193+
} /* end of function add_bad_states */

‎src/ic3/ebmc_ic3_interface.hh

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -43,7 +43,7 @@ public:
4343
void print_lit1(unsigned var,bool sign);
4444
void print_lit2(unsigned var,bool sign);
4545
void print_nodes();
46-
void print_var_map();
46+
void print_var_map(std::ostream &out);
4747
void form_orig_names();
4848
void form_neg_orig_name(CCUBE &Name,literalt &next_lit);
4949
bool form_orig_name(CCUBE &Name,literalt &lit,bool subtract = false);
@@ -58,6 +58,10 @@ public:
5858
void store_constraints(const std::string &fname);
5959
void read_constraints(const std::string &fname);
6060
void add_pseudo_inps(Circuit *N);
61+
void print_lit(std::ostream& out,literalt a);
62+
std::string print_string(const irep_idt &id);
63+
void add_verilog_conv_constrs();
64+
6165
protected:
6266
netlistt netlist;
6367

‎src/ic3/m1ain.cc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -80,9 +80,9 @@ int ic3_enginet::operator()()
8080
orig_names = false;
8181

8282
// print_nodes();
83-
// print_var_map();
83+
// print_var_map(std::cout);
8484
read_ebmc_input();
85-
//print_blif3("tst.blif",Ci.N);
85+
// print_blif3("tst.blif",Ci.N);
8686
if (cmdline.isset("aiger")) {
8787
printf("converting to aiger format\n");
8888
Ci.print_aiger_format();

‎src/ic3/m2ethods.hh

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -187,6 +187,7 @@ void print_files(char *root);
187187
int init_ind_cls();
188188
void form_nxt_cube(CUBE &Nxt_cube,CLAUSE &C);
189189
int push_on_the_fly(int last_ind,CLAUSE &C,char st_desc);
190+
void accept_constrs(SatSolver &Slvr);
190191
//
191192
// form CNF formulas
192193
void add_or_gate_cubes(DNF &F,int gate_ind,int shift);

‎src/ic3/r0ead_input.cc

Lines changed: 17 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -137,10 +137,6 @@ void ic3_enginet::form_inputs()
137137
} /* end of function form_inputs */
138138

139139

140-
141-
142-
143-
144140
/*=================================
145141
146142
F O R M _ T A B L E
@@ -189,10 +185,6 @@ void CompInfo::form_max_pres_svar() {
189185
max_pres_svar = max;
190186
} /* end of function form_max_pres_svar */
191187

192-
193-
194-
195-
196188
/*===================================
197189
198190
F O R M _ V A R _ N U M S
@@ -209,3 +201,20 @@ void CompInfo::form_var_nums()
209201
max_num_vars = max_num_vars0 + num_prop_vars; // we need to take into account
210202
// that property needs to be specified in two time frames
211203
} /* end of function form_var_nums */
204+
205+
/*================================================
206+
207+
A D D _ V E R I L O G _ C O N V _ C O N S T R S
208+
209+
================================================*/
210+
void ic3_enginet::add_verilog_conv_constrs()
211+
{
212+
213+
for(literalt lit : netlist.constraints) {
214+
if (lit.is_constant()) continue;
215+
std::cout << "constraint literal " << lit.get() << "\n";
216+
Ci.Init_clits.insert(lit.get());
217+
}
218+
219+
220+
} /* end of function add_verlig_conv_constrs */

‎src/ic3/r1ead_input.cc

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -63,6 +63,9 @@ void ic3_enginet::find_prop_lit()
6363

6464
if (prop_l.is_false()) Ci.const_flags = Ci.const_flags | 1;
6565
else if (prop_l.is_true()) Ci.const_flags = Ci.const_flags | 2;
66+
67+
// print_lit(std::cout,prop_l);
68+
// printf("\n");
6669

6770
} /* end of function find_prop_lit */
6871

‎src/ic3/r4ead_input.cc

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,8 @@ Author: Eugene Goldberg, [email protected]
2121
#include "m0ic3.hh"
2222

2323
#include "ebmc_ic3_interface.hh"
24+
25+
2426
/*=========================================
2527
2628
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)
8486
void ic3_enginet::store_constraints(const std::string &fname)
8587
{
8688

89+
add_verilog_conv_constrs();
8790
if (Ci.constr_flag == false) return;
8891

8992
read_constraints(fname);
@@ -241,7 +244,7 @@ void ic3_enginet::gen_ist_lits(bvt &Ist_lits)
241244
continue;
242245
if (var_num >= Nodes.size()) {
243246
p();
244-
printf("var_num = %d\n",var_num);
247+
printf("var_num = %zd\n",var_num);
245248
printf("Nodes.size() = %zu\n",Nodes.size());
246249
exit(100);
247250
}

‎src/ic3/r6ead_input.cc

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -152,6 +152,7 @@ void ic3_enginet::form_orig_names()
152152
void ic3_enginet::print_nodes()
153153
{
154154

155+
printf("\n----- Nodes ------\n");
155156
aigt::nodest &Nodes = netlist.nodes;
156157
for (size_t i=0; i <= Nodes.size(); i++) {
157158
aigt::nodet &Nd = Nodes[i];

‎src/ic3/r7ead_input.cc

Lines changed: 67 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -23,37 +23,85 @@ Author: Eugene Goldberg, [email protected]
2323
#include <ebmc/ebmc_base.h>
2424
#include "ebmc_ic3_interface.hh"
2525

26+
2627
/*=====================================
2728
2829
P R I N T _ V A R _ M A P
2930
30-
=====================================*/
31-
void ic3_enginet::print_var_map()
31+
=====================================*/
32+
void ic3_enginet::print_var_map(std::ostream &out)
3233
{
3334

3435

35-
var_mapt &vm = netlist.var_map;
36+
printf("\n----- Var Map ------\n");
3637

38+
var_mapt &vm = netlist.var_map;
3739
for(var_mapt::mapt::const_iterator it=vm.map.begin();
38-
it!=vm.map.end(); it++) {
39-
const var_mapt::vart &var=it->second;
40-
if (var.is_input()) printf("input: ");
41-
else if (var.is_latch()) printf("latch: ");
42-
else if (var.is_nondet()) printf("nondet: ");
43-
else if (var.is_wire()) printf("wire:" );
44-
else assert(false);
45-
46-
for (size_t j=0; j < var.bits.size(); j++) {
47-
if (j > 0) printf(", ");
48-
literalt lit =var.bits[j].current;
49-
unsigned lit_val = lit.get();
50-
printf("[%zu] = %u",j,lit_val);
40+
it!=vm.map.end(); it++)
41+
{
42+
const var_mapt::vart &var=it->second;
43+
44+
for(std::size_t i=0; i<var.bits.size(); i++)
45+
{
46+
out << " " << it->first;
47+
if(var.bits.size()!=1) out << "[" << i << "]";
48+
out << "=";
49+
50+
literalt l_c=var.bits[i].current;
51+
52+
if(l_c.is_true())
53+
out << "true";
54+
else if(l_c.is_false())
55+
out << "false";
56+
else
57+
{
58+
if(l_c.sign()) out << "!";
59+
out << l_c.var_no();
60+
}
61+
62+
if(var.vartype==var_mapt::vart::vartypet::LATCH)
63+
{
64+
out << "->";
65+
66+
literalt l_n=var.bits[i].next;
67+
68+
if(l_n.is_true())
69+
out << "true";
70+
else if(l_n.is_false())
71+
out << "false";
72+
else
73+
{
74+
if(l_n.sign()) out << "!";
75+
out << l_n.var_no();
76+
}
77+
}
78+
79+
out << " ";
80+
81+
switch(var.vartype)
82+
{
83+
case var_mapt::vart::vartypet::INPUT: out << "(input)"; break;
84+
case var_mapt::vart::vartypet::LATCH: out << "(latch)"; break;
85+
case var_mapt::vart::vartypet::NONDET: out << "(nondet)"; break;
86+
case var_mapt::vart::vartypet::WIRE: out << "(wire)"; break;
87+
case var_mapt::vart::vartypet::OUTPUT:out << "(output)"; break;
88+
case var_mapt::vart::vartypet::UNDEF: out << "(?)"; break;
89+
}
90+
91+
out << '\n';
92+
}
5193
}
52-
printf("\n");
53-
}
94+
95+
out << '\n'
96+
<< "Total no. of variable bits: " << vm.reverse_map.size() << '\n'
97+
<< "Total no. of latch bits: " << vm.latches.size() << '\n'
98+
<< "Total no. of nondet bits: " << vm.nondets.size() << '\n'
99+
<< "Total no. of input bits: " << vm.inputs.size() << '\n'
100+
<< "Total no. of output bits: " << vm.outputs.size() << '\n';
101+
54102

55103

56-
} /* end of function print_var_map */
104+
} /* end of function print_var_map */
57105
/*=========================================
58106
59107
A D D _ P S E U D O _ I N P S

‎src/ic3/v0erify.cc

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -161,6 +161,7 @@ bool CompInfo::ver_ini_states(CNF &H)
161161

162162
accept_new_clauses(Gen_sat,Ist);
163163

164+
accept_constrs(Gen_sat);
164165
bool ok = ver_prop();
165166
if (!ok) return(false);
166167

0 commit comments

Comments
 (0)