From d0536103a91ac8abd4fd7f2fca0c157e06c1960c Mon Sep 17 00:00:00 2001 From: eigold Date: Wed, 24 May 2017 05:47:53 -0400 Subject: [PATCH 01/16] changed the way properties are named --- src/ebmc/ebmc_parse_options.cpp | 2 +- src/ebmc/ebmc_parse_options.h | 2 +- src/ic3/m0ic3.hh | 4 ++-- src/ic3/p1arameters.cc | 16 ++++++---------- src/ic3/r3ead_input.cc | 2 +- src/ic3/r6ead_input.cc | 27 +++++++++++++-------------- src/ic3/todo | 1 + 7 files changed, 25 insertions(+), 29 deletions(-) diff --git a/src/ebmc/ebmc_parse_options.cpp b/src/ebmc/ebmc_parse_options.cpp index fb88c8d13..6a221af18 100644 --- a/src/ebmc/ebmc_parse_options.cpp +++ b/src/ebmc/ebmc_parse_options.cpp @@ -262,7 +262,7 @@ void ebmc_parse_optionst::help() " --k-induction do k-induction with k=bound\n" " --bdd use (unbounded) BDD engine\n" " --ic3 [options] use IC3 engine with options described below\n" - " --prop check property number \n" + " --property check property number \n" " --constr use constraints specified in 'file.cnstr'\n" //" --interpolation use bit-level interpolants\n" //" --interpolation-word use word-level interpolants\n" diff --git a/src/ebmc/ebmc_parse_options.h b/src/ebmc/ebmc_parse_options.h index dfd3123d5..30a327f26 100644 --- a/src/ebmc/ebmc_parse_options.h +++ b/src/ebmc/ebmc_parse_options.h @@ -32,7 +32,7 @@ class ebmc_parse_optionst:public parse_options_baset "(reset):" "(version)(verilog-rtl)(verilog-netlist)" "(compute-interpolant)(interpolation)(interpolation-vmcai)" - "(ic3)(prop):(constr)(h)" + "(ic3)(property):(constr)(h)" "(interpolation-word)(interpolator):(bdd)" "(smt1)(smt2)(boolector)(z3)(cvc4)(yices)(mathsat)(prover)(lifter)" "(aig)(stop-induction)(stop-minimize)(start):(coverage)(naive)" diff --git a/src/ic3/m0ic3.hh b/src/ic3/m0ic3.hh index f96ca7466..2b1cc8d28 100644 --- a/src/ic3/m0ic3.hh +++ b/src/ic3/m0ic3.hh @@ -23,8 +23,8 @@ public: // generate CNF formulas. For every input gate and latch // Ordering[i] == i - size_t prop_ind; // specifies the index of the property to be checked - // to be implemented for the integrated version + std::string prop_name; // specifies the name of the property to be checked + CUBE Gate_to_var; // gate_to_var[gate_ind] gives the variable assigned to // the output of gate 'gate_ind' diff --git a/src/ic3/p1arameters.cc b/src/ic3/p1arameters.cc index 3d5f1ffb7..8ef0a3e2e 100644 --- a/src/ic3/p1arameters.cc +++ b/src/ic3/p1arameters.cc @@ -35,11 +35,9 @@ void ic3_enginet::read_parameters() exit(0); } - if (cmdline.isset("prop")) { - std::string sval = cmdline.get_value("prop"); - Ci.prop_ind = stoi(sval); - // assert(Ci.prop_ind >= 0); - } + if (cmdline.isset("property")) + Ci.prop_name = cmdline.get_value("property"); + if (cmdline.isset("constr")) Ci.constr_flag = true; @@ -55,10 +53,9 @@ void ic3_enginet::read_parameters() void ic3_enginet::print_header() { - printf("ebmc verilog_file --ic3 [--p | --prop N]\n"); - printf("p - print out information about available options\n"); - printf("prop N - check property number N (count starts with 0)\n"); - + printf("ebmc verilog_file --ic3 [--prop nm] [--constr]\n"); + printf("prop nm - check property with name 'nm'\n"); + printf("constr - use constraints listed in 'verilog_file.cnstr'\n"); } /* end of function print_header */ /*===================================== @@ -99,7 +96,6 @@ void CompInfo::init_parameters() max_rec_depth = 1; grl_heur = NO_JOINS; max_coi_depth = 10; - prop_ind = 0; constr_flag = false; } /* end of function init_parameters */ diff --git a/src/ic3/r3ead_input.cc b/src/ic3/r3ead_input.cc index a8d0d750e..e4dd77b32 100644 --- a/src/ic3/r3ead_input.cc +++ b/src/ic3/r3ead_input.cc @@ -219,7 +219,7 @@ void ic3_enginet::form_outp_buf(CDNF &Out_names) NEXT: char buff[MAX_NAME]; - sprintf(buff,"p%zu",Ci.prop_ind); + sprintf(buff,"%s",Ci.prop_name.c_str()); conv_to_vect(Pin_names[1],buff); Out_names.push_back(Pin_names[1]); diff --git a/src/ic3/r6ead_input.cc b/src/ic3/r6ead_input.cc index 4294ddb29..bd70aedd3 100644 --- a/src/ic3/r6ead_input.cc +++ b/src/ic3/r6ead_input.cc @@ -85,24 +85,23 @@ void ic3_enginet::read_constraints(const std::string &source_name) bool ic3_enginet::find_prop(propertyt &Prop) { - if (Ci.prop_ind >= properties.size()) { - std::cout << "file " << cmdline.args[0] << " specifies only "; - std::cout << properties.size() << " properties\n"; - exit(100); + assert(properties.size() > 0); + + if ((properties.size() == 1) && (Ci.prop_name.size() == 0)) { + Prop = properties.front(); + Ci.prop_name = id2string(Prop.name); + return(true); } - - for(const auto &p : properties) { - irep_idt Nm = p.name; - std::string Sn = short_name(Nm); - int ind = stoi(Sn); - assert(ind>0 && "Property Index must be greater than 0"); - size_t index=(size_t) ind; - if (index-1 == Ci.prop_ind) { + + for(const auto &p : properties) + if (p.status==propertyt::statust::UNKNOWN) { + assert(p.name == Ci.prop_name); Prop = p; return(true); } - //idx++; - } + + + return false; } /* end of function find_prop */ diff --git a/src/ic3/todo b/src/ic3/todo index c64e98d06..995e06035 100644 --- a/src/ic3/todo +++ b/src/ic3/todo @@ -3,6 +3,7 @@ Finishing integration with ebmc ===================== +*) Eliminate the bug in generating constrained formulas *) Add code freeing memory allocated by the Verilog reader after IC3 converted this information into its internal data From 1c49743b4636117ae69162bfb3bab6498a5f89d3 Mon Sep 17 00:00:00 2001 From: eigold Date: Wed, 24 May 2017 08:50:42 -0400 Subject: [PATCH 02/16] corrected regression tests --- regression/ebmc/ic3/exmp7/test.desc | 2 +- regression/ebmc/ic3/exmp8/test.desc | 2 +- regression/ebmc/ic3/exmp9/test.desc | 2 +- regression/ebmc/ic3/non_inductive1/test.desc | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/regression/ebmc/ic3/exmp7/test.desc b/regression/ebmc/ic3/exmp7/test.desc index 7b5cb874e..83e6e358f 100644 --- a/regression/ebmc/ic3/exmp7/test.desc +++ b/regression/ebmc/ic3/exmp7/test.desc @@ -1,6 +1,6 @@ CORE bobmiterbm1multi.sv ---ic3 --prop 1032 +--ic3 --property bobmiterbm1multi.property.1033 ^property HOLDS ^verification is ok -- diff --git a/regression/ebmc/ic3/exmp8/test.desc b/regression/ebmc/ic3/exmp8/test.desc index 960ae2f44..f7ac65a33 100644 --- a/regression/ebmc/ic3/exmp8/test.desc +++ b/regression/ebmc/ic3/exmp8/test.desc @@ -1,6 +1,6 @@ CORE bobmiterbm1multi.sv ---ic3 --prop 1079 +--ic3 --property bobmiterbm1multi.property.1080 ^property FAILED ^verification is ok -- diff --git a/regression/ebmc/ic3/exmp9/test.desc b/regression/ebmc/ic3/exmp9/test.desc index 56fcdb081..afcf7297b 100644 --- a/regression/ebmc/ic3/exmp9/test.desc +++ b/regression/ebmc/ic3/exmp9/test.desc @@ -1,6 +1,6 @@ CORE sm98a7multi.sv ---ic3 --prop 1 --constr +--ic3 --property sm98a7multi.property.2 --constr ^property FAILED ^verification is ok -- diff --git a/regression/ebmc/ic3/non_inductive1/test.desc b/regression/ebmc/ic3/non_inductive1/test.desc index a289ecd21..b9e04d1c8 100644 --- a/regression/ebmc/ic3/non_inductive1/test.desc +++ b/regression/ebmc/ic3/non_inductive1/test.desc @@ -1,6 +1,6 @@ CORE non_inductive.sv ---ic3 --prop 0 +--ic3 --property main.property.p0 ^property HOLDS$ ^verification is ok -- From 3429c8c11bb41af67fa88e743fdf6a3b0d5148ba Mon Sep 17 00:00:00 2001 From: eigold Date: Wed, 24 May 2017 15:29:16 -0400 Subject: [PATCH 03/16] added scripts and other files to be used for testing new code --- src/ebmc/pproc_all.bat | 63 +++++++++++++++++++++++++++ src/ebmc/r1esults_multi/exmps11 | 6 +++ src/ebmc/r1esults_multi/multi_prop.pl | 52 ++++++++++++++++++++++ src/ebmc/r1esults_multi/rpnt.txt | 17 ++++++++ src/ebmc/r1esults_multi/sngl_call.bat | 6 +++ src/ebmc/r2esults_multi/exmps12 | 4 ++ src/ebmc/r2esults_multi/multi_prop.pl | 52 ++++++++++++++++++++++ src/ebmc/r2esults_multi/rpnt.txt | 15 +++++++ src/ebmc/r2esults_multi/sngl_call.bat | 12 +++++ src/ebmc/rregr_testing.bat | 12 +++++ 10 files changed, 239 insertions(+) create mode 100755 src/ebmc/pproc_all.bat create mode 100644 src/ebmc/r1esults_multi/exmps11 create mode 100755 src/ebmc/r1esults_multi/multi_prop.pl create mode 100644 src/ebmc/r1esults_multi/rpnt.txt create mode 100755 src/ebmc/r1esults_multi/sngl_call.bat create mode 100644 src/ebmc/r2esults_multi/exmps12 create mode 100755 src/ebmc/r2esults_multi/multi_prop.pl create mode 100644 src/ebmc/r2esults_multi/rpnt.txt create mode 100755 src/ebmc/r2esults_multi/sngl_call.bat create mode 100755 src/ebmc/rregr_testing.bat diff --git a/src/ebmc/pproc_all.bat b/src/ebmc/pproc_all.bat new file mode 100755 index 000000000..2b5af593f --- /dev/null +++ b/src/ebmc/pproc_all.bat @@ -0,0 +1,63 @@ +# +limit cputime 65 +limit vmemoryuse 2800 megabytes +set bench_dir = /home/eugene/e0xamples/hwmcc10 + +rrm -rf r0esults/$1.prot + +foreach file (`cat $1`) + +printf "--------------\n" +printf "$file ::\n" + + +ccp $bench_dir/$file.aig r0esults +cd r0esults +ba2ver $file.aig $file.sv + +printf "%s: " $file >> $1.prot +time ../ebmc $file.sv --ic3 >& $file.prt +set stat_var = $status +if ($stat_var >= 100) then +printf "unconventional termination\n" >> $1.prot +cd .. +continue +endif +if ($stat_var > 10) then +@ stat_var0 = $stat_var - 10 +else +@ stat_var0 = $stat_var +endif +if ($stat_var0 == 0) then +printf "unsolved\n" +else if ($stat_var0 == 1) then +printf "$file result: bug is found\n" +printf "bug is found" >> $1.prot +if ($stat_var > 10) then +printf " : verification failed\n" >> $1.prot +else +printf "\n" >> $1.prot +endif +else if ($stat_var0 == 2) then +printf "$file result: fixed point is reached\n" +printf "property holds" >> $1.prot +if ($stat_var > 10) then +printf " : verification failed\n" >> $1.prot +else +printf "\n" >> $1.prot +endif +else if ($stat_var0 == 3) then +printf "not finished\n" >> $1.prot +printf "$file result: time exceeded\n" +else if ($stat_var0 == 4) then +printf "not finished\n" >> $1.prot +printf "$file result: memory exceeded\n" +else printf "not finished\n" >> $1.prot +endif +rrm -f $file.aig +rrm -f $file.sv +#r1em.bat $file +cd .. +end + + diff --git a/src/ebmc/r1esults_multi/exmps11 b/src/ebmc/r1esults_multi/exmps11 new file mode 100644 index 000000000..4b46b0eae --- /dev/null +++ b/src/ebmc/r1esults_multi/exmps11 @@ -0,0 +1,6 @@ +mentorbm1 1 2 9 +sm98a7multi 3 +sm98tcas16multi 1 2 +sm98tcas16tmulti 2 4 6 +sm98tcasmulti 1 2 5 6 +sm98tcastmulti 2 4 5 6 diff --git a/src/ebmc/r1esults_multi/multi_prop.pl b/src/ebmc/r1esults_multi/multi_prop.pl new file mode 100755 index 000000000..fb9c62710 --- /dev/null +++ b/src/ebmc/r1esults_multi/multi_prop.pl @@ -0,0 +1,52 @@ +#!/usr/bin/perl + +if ($#ARGV == -1) { + printf("multi_prop.pl exmps\n"); + exit(0); +} + + +qx(rm -f res.txt); +qx(rm -f *.prot); + +$exmp_path = "/home/eugene/e0xamples/hwmcc11/multi"; + +(my $fname) = @ARGV; + +$time_limit = 800; + +open EXMPS,"< $fname" or die "failed to open file $fname\n"; + +while () { + chomp($_); + $exmp = $_; + + @words = split / /,$exmp; + + # print "@words"; + + $name = $words[0]; + + printf "$name\n"; + + qx(cp $exmp_path/$name.aig .); + qx(ba2ver $name.aig $name.sv pa); + + + $i = 0; + foreach (@words) { + $i++; + if ($i == 1) {next;} + printf(" prop. $_\n"); + qx(sngl_call.bat $time_limit $name $_); + } + +# printf("%s\n",$num_prop); + + qx(rm -f $name.aig $name.sv $name.sv.cnstr); +} + +close EXMPS; + +$answer = qx(diff -s res.txt rpnt.txt); +printf "$answer"; diff --git a/src/ebmc/r1esults_multi/rpnt.txt b/src/ebmc/r1esults_multi/rpnt.txt new file mode 100644 index 000000000..4dabfe10d --- /dev/null +++ b/src/ebmc/r1esults_multi/rpnt.txt @@ -0,0 +1,17 @@ +exmp mentorbm1 prop. 1 property HOLDS +exmp mentorbm1 prop. 2 property HOLDS +exmp mentorbm1 prop. 9 property HOLDS +exmp sm98a7multi prop. 3 property FAILED +exmp sm98tcas16multi prop. 1 property FAILED +exmp sm98tcas16multi prop. 2 property HOLDS +exmp sm98tcas16tmulti prop. 2 property HOLDS +exmp sm98tcas16tmulti prop. 4 property FAILED +exmp sm98tcas16tmulti prop. 6 property FAILED +exmp sm98tcasmulti prop. 1 property FAILED +exmp sm98tcasmulti prop. 2 property HOLDS +exmp sm98tcasmulti prop. 5 property FAILED +exmp sm98tcasmulti prop. 6 property FAILED +exmp sm98tcastmulti prop. 2 property HOLDS +exmp sm98tcastmulti prop. 4 property FAILED +exmp sm98tcastmulti prop. 5 property FAILED +exmp sm98tcastmulti prop. 6 property FAILED diff --git a/src/ebmc/r1esults_multi/sngl_call.bat b/src/ebmc/r1esults_multi/sngl_call.bat new file mode 100755 index 000000000..4524c11bd --- /dev/null +++ b/src/ebmc/r1esults_multi/sngl_call.bat @@ -0,0 +1,6 @@ +#!/usr/bin/tcsh +limit cputime $1 +#printf "$1 $2 $3\n" > $2_p$3.prot +printf "exmp $2 prop. $3 " >> res.txt +../ebmc $2.sv --ic3 --constr --property $2.property.$3 > $2_p$3.prot +grep property $2_p$3.prot >> res.txt diff --git a/src/ebmc/r2esults_multi/exmps12 b/src/ebmc/r2esults_multi/exmps12 new file mode 100644 index 000000000..131935b78 --- /dev/null +++ b/src/ebmc/r2esults_multi/exmps12 @@ -0,0 +1,4 @@ +mentorbm1 4 +6s110 1015 1036 1037 1229 1528 1529 493 844 845 850 851 +6s135 17 101 +6s141 11 diff --git a/src/ebmc/r2esults_multi/multi_prop.pl b/src/ebmc/r2esults_multi/multi_prop.pl new file mode 100755 index 000000000..161f52467 --- /dev/null +++ b/src/ebmc/r2esults_multi/multi_prop.pl @@ -0,0 +1,52 @@ +#!/usr/bin/perl + +if ($#ARGV == -1) { + printf("multi_prop.pl exmps\n"); + exit(0); +} + + +qx(rm -f res.txt); +qx(rm -f *.prot *.prt); + +$exmp_path = "/home/eugene/e0xamples/hwmcc12/multi"; + +(my $fname) = @ARGV; + +$time_limit = 600; + +open EXMPS,"< $fname" or die "failed to open file $fname\n"; + +while () { + chomp($_); + $exmp = $_; + + @words = split / /,$exmp; + + # print "@words"; + + $name = $words[0]; + + printf "$name\n"; + + qx(cp $exmp_path/$name.aig .); + qx(ba2ver $name.aig $name.sv pa m); + + + $i = 0; + foreach (@words) { + $i++; + if ($i == 1) {next;} + printf(" prop. $_\n"); + qx(sngl_call.bat $time_limit $name $_); + } + +# printf("%s\n",$num_prop); + + qx(rm -f $name.aig $name.sv $name.sv.cnstr); +} + +close EXMPS; + +$answer = qx(diff -s res.txt rpnt.txt); +printf "$answer"; diff --git a/src/ebmc/r2esults_multi/rpnt.txt b/src/ebmc/r2esults_multi/rpnt.txt new file mode 100644 index 000000000..f44bfe256 --- /dev/null +++ b/src/ebmc/r2esults_multi/rpnt.txt @@ -0,0 +1,15 @@ +exmp mentorbm1 prop. 4 no constr: property FAILED, with constr: property HOLDS +exmp 6s110 prop. 1015 no constr: property FAILED, with constr: property HOLDS +exmp 6s110 prop. 1036 no constr: property FAILED, with constr: property HOLDS +exmp 6s110 prop. 1037 no constr: property FAILED, with constr: property HOLDS +exmp 6s110 prop. 1229 no constr: property FAILED, with constr: property HOLDS +exmp 6s110 prop. 1528 no constr: property FAILED, with constr: property HOLDS +exmp 6s110 prop. 1529 no constr: property FAILED, with constr: property HOLDS +exmp 6s110 prop. 493 no constr: property FAILED, with constr: property HOLDS +exmp 6s110 prop. 844 no constr: property FAILED, with constr: property HOLDS +exmp 6s110 prop. 845 no constr: property FAILED, with constr: property HOLDS +exmp 6s110 prop. 850 no constr: property FAILED, with constr: property HOLDS +exmp 6s110 prop. 851 no constr: property FAILED, with constr: property HOLDS +exmp 6s135 prop. 17 no constr: property FAILED, with constr: property HOLDS +exmp 6s135 prop. 101 no constr: property FAILED, with constr: property HOLDS +exmp 6s141 prop. 11 no constr: property FAILED, with constr: property HOLDS diff --git a/src/ebmc/r2esults_multi/sngl_call.bat b/src/ebmc/r2esults_multi/sngl_call.bat new file mode 100755 index 000000000..7cb8dc40c --- /dev/null +++ b/src/ebmc/r2esults_multi/sngl_call.bat @@ -0,0 +1,12 @@ +#!/usr/bin/tcsh +limit cputime $1 +#printf "$1 $2 $3\n" > $2_p$3.prot +printf "exmp $2 prop. $3 " >> res.txt + +../ebmc $2.sv --ic3 --property main.property.$3 > $2_p$3.prot +../ebmc $2.sv --ic3 --property main.property.$3 --constr > $2_p$3.prt + +printf "no constr: " >> res.txt +grep property $2_p$3.prot | tr -d '\n' >> res.txt +printf ", with constr: " >> res.txt +grep property $2_p$3.prt >> res.txt diff --git a/src/ebmc/rregr_testing.bat b/src/ebmc/rregr_testing.bat new file mode 100755 index 000000000..dbd6401bf --- /dev/null +++ b/src/ebmc/rregr_testing.bat @@ -0,0 +1,12 @@ +# +rrm -f $1/*.prot +rrm -f $1/ *.prt +pproc_all.bat b1uggy.solved +pproc_all.bat corr.solved +pproc_all.bat u5nsolved +cd r0esults +diff -s b1uggy.solved.prot b1uggy.solved.rpnt +diff -s corr.solved.prot corr.solved.rpnt +diff -s u5nsolved.prot u5nsolved.rpnt +cd .. + From a4811b0ac64f9fe97268a02ee72eec330d98492d Mon Sep 17 00:00:00 2001 From: eigold Date: Wed, 24 May 2017 19:23:09 -0400 Subject: [PATCH 04/16] removed a bug affecting verification problems with constraints --- src/ic3/build_prob/g0en_cnf.cc | 4 ++-- src/ic3/build_prob/g2en_cnf.cc | 4 +++- src/ic3/build_prob/g3en_cnf.cc | 6 +++--- 3 files changed, 8 insertions(+), 6 deletions(-) diff --git a/src/ic3/build_prob/g0en_cnf.cc b/src/ic3/build_prob/g0en_cnf.cc index 47066943f..e6ad322b0 100755 --- a/src/ic3/build_prob/g0en_cnf.cc +++ b/src/ic3/build_prob/g0en_cnf.cc @@ -86,8 +86,8 @@ void CompInfo::gen_out_fun(DNF &H,int shift,bool short_version) if (G.gate_type == INPUT) continue; if (G.gate_type == LATCH) continue; // skip the gates that are not part of the output function - if (G.flags.output_function == 0) - if (G.flags.fun_constr == 0) continue; + if (G.flags.output_function == 0) + if ((G.flags.fun_constr == 0) && (G.flags.tran_constr == 0)) if (short_version) // skip the gates that are shared by transition relation and out function if (G.flags.transition) continue; diff --git a/src/ic3/build_prob/g2en_cnf.cc b/src/ic3/build_prob/g2en_cnf.cc index 5ba8c75b9..fcc3f7c47 100644 --- a/src/ic3/build_prob/g2en_cnf.cc +++ b/src/ic3/build_prob/g2en_cnf.cc @@ -202,7 +202,9 @@ void CompInfo::set_constr_flag() bool tran_flag,fun_flag; gen_constr_coi(Gates,tran_flag,fun_flag,Stack); - assert(tran_flag || fun_flag); + tran_flag = true; + fun_flag = true; + mark_constr_gates(Gates,tran_flag,fun_flag); if (tran_flag) Constr_gates[gate_ind].tran_coi = 1; else Constr_gates[gate_ind].tran_coi = 0; diff --git a/src/ic3/build_prob/g3en_cnf.cc b/src/ic3/build_prob/g3en_cnf.cc index 9585ef1ae..159c4ac1c 100644 --- a/src/ic3/build_prob/g3en_cnf.cc +++ b/src/ic3/build_prob/g3en_cnf.cc @@ -66,10 +66,10 @@ void CompInfo::gen_constr_coi(CUBE &Gates,bool &tran_flag,bool &fun_flag, fun_flag = true; skip = true; } - if (G.flags.transition > 0) { + + if (G.flags.transition > 0) tran_flag = true; - skip = true; - } + if (skip) continue; Gates.push_back(gate_ind); From e2acc11abaa35d91be22720331beae595e2e226f Mon Sep 17 00:00:00 2001 From: eigold Date: Wed, 24 May 2017 20:04:46 -0400 Subject: [PATCH 05/16] removed the performance bug caused by insufficient liftingof CTG states --- src/ic3/c2tg.cc | 18 ++++++++++++++++++ src/ic3/e5xclude_state.cc | 13 +++++++------ src/ic3/m2ethods.hh | 1 + 3 files changed, 26 insertions(+), 6 deletions(-) diff --git a/src/ic3/c2tg.cc b/src/ic3/c2tg.cc index a85b210a6..db890f8d0 100644 --- a/src/ic3/c2tg.cc +++ b/src/ic3/c2tg.cc @@ -78,3 +78,21 @@ int CompInfo::latest_succ_tf_ind(int tf_ind,CLAUSE &C) return(tf_lind); } /* end of function latest_succ_tf_ind */ + +/*======================================= + + F O R M _ N X T _ C U B E + + =====================================*/ +void CompInfo::form_nxt_cube(CUBE &Nxt_cube,CLAUSE &C) +{ + + for (size_t i=0;i < C.size(); i++) { + int var_ind = abs(C[i])-1; + int nxt_var_ind = Pres_to_next[var_ind]; + assert(nxt_var_ind >=0); + int lit = (C[i] > 0)?-(nxt_var_ind+1):(nxt_var_ind+1); + Nxt_cube.push_back(lit); + } + +} /* end of function form_nxt_cube */ diff --git a/src/ic3/e5xclude_state.cc b/src/ic3/e5xclude_state.cc index edf7f2cf6..875160118 100644 --- a/src/ic3/e5xclude_state.cc +++ b/src/ic3/e5xclude_state.cc @@ -159,12 +159,13 @@ bool CompInfo::find_ind_subclause_ctg(CLAUSE &C,int curr_tf,CLAUSE &C0, release_lit(Slvr,~act_lit); CUBE Ctg_cube; - bool succ; - if ((ctg_cnt < max_ctg_cnt) && (rec_depth < max_rec_depth)) { - CUBE Nxt_cube; - use_coi_to_drop_svars(Nxt_cube,Nxt_st,tf_lind-curr_tf-1); - lift_ctg_state(Ctg_cube,Ctg_st,Inps,Nxt_cube); + CUBE Nxt_cube; + form_nxt_cube(Nxt_cube,C); + + lift_ctg_state(Ctg_cube,Ctg_st,Inps,Nxt_cube); + bool cond = (ctg_cnt < max_ctg_cnt) && (rec_depth < max_rec_depth); + if (cond && (curr_tf > 1)) { ctg_cnt++; tot_ctg_cnt++; succ = exclude_ctg(Ctg_cube,curr_tf,rec_depth); @@ -173,7 +174,7 @@ bool CompInfo::find_ind_subclause_ctg(CLAUSE &C,int curr_tf,CLAUSE &C0, continue; } } - // else Ctg_cube = Ctg_st; + bool ok; ok = adjust_clause2(C,Ctg_cube,Failed_lits); diff --git a/src/ic3/m2ethods.hh b/src/ic3/m2ethods.hh index e2c933630..a372db461 100644 --- a/src/ic3/m2ethods.hh +++ b/src/ic3/m2ethods.hh @@ -185,6 +185,7 @@ void add_last_cube(DNF &F); void form_property_gates(CUBE &Gates); void print_files(char *root); int init_ind_cls(); +void form_nxt_cube(CUBE &Nxt_cube,CLAUSE &C); // // form CNF formulas From 174b0267f1c712c517fce2a4726903cf45dcba79 Mon Sep 17 00:00:00 2001 From: eigold Date: Thu, 25 May 2017 14:42:48 -0400 Subject: [PATCH 06/16] made more changes --- src/ebmc/ebmc_parse_options.cpp | 6 ++-- src/ebmc/ebmc_parse_options.h | 2 +- src/ic3/aux_types.hh | 20 ++++++++--- src/ic3/e1xclude_state.cc | 21 ++++++------ src/ic3/e3xclude_state.cc | 13 ++----- src/ic3/e4xclude_state.cc | 3 ++ src/ic3/m0ic3.hh | 5 ++- src/ic3/p1arameters.cc | 7 ++-- src/ic3/s3tat.cc | 8 +---- src/ic3/ttodo | 60 +++++++++++++++++++++++++++++++++ 10 files changed, 106 insertions(+), 39 deletions(-) create mode 100644 src/ic3/ttodo diff --git a/src/ebmc/ebmc_parse_options.cpp b/src/ebmc/ebmc_parse_options.cpp index 6a221af18..29fdc70e0 100644 --- a/src/ebmc/ebmc_parse_options.cpp +++ b/src/ebmc/ebmc_parse_options.cpp @@ -262,8 +262,10 @@ void ebmc_parse_optionst::help() " --k-induction do k-induction with k=bound\n" " --bdd use (unbounded) BDD engine\n" " --ic3 [options] use IC3 engine with options described below\n" - " --property check property number \n" - " --constr use constraints specified in 'file.cnstr'\n" + " --property check property named \n" + " --constr use constraints specified in 'file.cnstr'\n" + " --help print out help information\n" + " --new-mode new mode is switched on\n" //" --interpolation use bit-level interpolants\n" //" --interpolation-word use word-level interpolants\n" //" --diameter perform recurrence diameter test\n" diff --git a/src/ebmc/ebmc_parse_options.h b/src/ebmc/ebmc_parse_options.h index 30a327f26..1415a3489 100644 --- a/src/ebmc/ebmc_parse_options.h +++ b/src/ebmc/ebmc_parse_options.h @@ -32,7 +32,7 @@ class ebmc_parse_optionst:public parse_options_baset "(reset):" "(version)(verilog-rtl)(verilog-netlist)" "(compute-interpolant)(interpolation)(interpolation-vmcai)" - "(ic3)(property):(constr)(h)" + "(ic3)(property):(constr)(h)(new-mode)" "(interpolation-word)(interpolator):(bdd)" "(smt1)(smt2)(boolector)(z3)(cvc4)(yices)(mathsat)(prover)(lifter)" "(aig)(stop-induction)(stop-minimize)(start):(coverage)(naive)" diff --git a/src/ic3/aux_types.hh b/src/ic3/aux_types.hh index 7cf160a6e..c3d97aaac 100644 --- a/src/ic3/aux_types.hh +++ b/src/ic3/aux_types.hh @@ -98,27 +98,39 @@ struct OblTableElem { typedef std::vector OblTable; + // // PrQueue // struct PqElem { - int tf_ind; // time frame index + int tf_ind; // time frame index, the same value as in OblTableElem + int dist; // the same value as in OblTableElem int tbl_ind; // index of this element in 'Obl_table' + int sort_mode; // specifies the sorting mode }; -class pq_compare -{ +class pq_compare { public: bool operator() (PqElem &A, PqElem &B) { - return (A.tf_ind > B.tf_ind); + if (A.tf_ind > B.tf_ind) return(true); + if (A.tf_ind < B.tf_ind) return(false); + if (A.dist > B.dist) return(true); + if (A.sort_mode == 0) return(false); + if (A.sort_mode == 1) { + if (A.tbl_ind > B.tbl_ind) return(true); + else return(false);} + assert(A.sort_mode == 2); + if (A.tbl_ind < B.tbl_ind) return(true); + else return(false); } }; typedef std::priority_queue, pq_compare> PrQueue; + // // ClauseInfo // diff --git a/src/ic3/e1xclude_state.cc b/src/ic3/e1xclude_state.cc index 05fb3417a..f3c9c576e 100644 --- a/src/ic3/e1xclude_state.cc +++ b/src/ic3/e1xclude_state.cc @@ -44,35 +44,34 @@ void CompInfo::exclude_state_cube(CNF &G,int &min_tf,CUBE &St0_cube,CUBE &Inps0) printf("Pr_queue.size() = %d\n",(int) Pr_queue.size()); } - int obl_tf = Pr_queue.top().tf_ind; + int curr_tf = Pr_queue.top().tf_ind; int tbl_ind = Pr_queue.top().tbl_ind; if (verbose > 1) - printf("obl_tf = %d, tbl_ind = %d, min_tf = %d\n",obl_tf,tbl_ind, min_tf); + printf("curr_tf = %d, tbl_ind = %d, min_tf = %d\n",curr_tf,tbl_ind, min_tf); CUBE St_cube = Obl_table[tbl_ind].St_cb; char st_descr = Obl_table[tbl_ind].st_descr; - if (obl_tf == 0) + if (curr_tf == 0) if (cont_init_states(St_cube)) return; int dist = Obl_table[tbl_ind].dist; int st_ind = tf_lind + 1 - dist; - - curr_tf = obl_tf; + int succ_ind = Obl_table[tbl_ind].succ_ind; - bool ok = oblig_is_active(obl_tf+1,St_cube); + bool ok = oblig_is_active(curr_tf+1,St_cube); if (!ok) { if (st_descr == OLD_STATE) triv_old_st_cnt++; Pr_queue.pop(); - if (succ_ind < 0) form_res_cnf(G,obl_tf+1,St_cube); + if (succ_ind < 0) form_res_cnf(G,curr_tf+1,St_cube); continue;} - if (obl_tf < min_tf) min_tf = obl_tf; + if (curr_tf < min_tf) min_tf = curr_tf; @@ -87,10 +86,10 @@ void CompInfo::exclude_state_cube(CNF &G,int &min_tf,CUBE &St0_cube,CUBE &Inps0) std::cout << C << std::endl; } - - if (obl_tf + 2 < tf_lind + 1) { + int tf_ind1 = curr_tf+1; + if (tf_ind1 < tf_lind) { CUBE Inps = Obl_table[tbl_ind].Inp_assgn; - add_new_elem(St_cube,Inps,obl_tf+2,dist,succ_ind,OLD_STATE); + add_new_elem(St_cube,Inps,tf_ind1+1,dist,succ_ind,OLD_STATE); } diff --git a/src/ic3/e3xclude_state.cc b/src/ic3/e3xclude_state.cc index 64da1ef54..dfdb59630 100644 --- a/src/ic3/e3xclude_state.cc +++ b/src/ic3/e3xclude_state.cc @@ -32,7 +32,6 @@ void CompInfo::incr_short(CLAUSE &C,CLAUSE &C0,int curr_tf, } - SatSolver &Slvr = Time_frames[curr_tf].Slvr; int impr_count = 0; C = C0; if (C.size() == 1) return; @@ -71,17 +70,11 @@ void CompInfo::incr_short(CLAUSE &C,CLAUSE &C0,int curr_tf, CLAUSE C1; - if ((ctg_flag == false) || (curr_tf == 0)) { - if (grl_heur == NO_JOINS) - ok = triv_ind_cls_proc(C1,Curr,curr_tf); - else { - assert(grl_heur == WITH_JOINS); - ok = find_ind_subclause_cti(C1,Slvr,Curr,st_descr); - } - } + if ((ctg_flag == false) || (curr_tf == 0)) + ok = triv_ind_cls_proc(C1,Curr,curr_tf); else ok = find_ind_subclause_ctg(C1,curr_tf,Curr,st_descr, - rec_depth,Failed_lits); + rec_depth,Failed_lits); if (!ok) { diff --git a/src/ic3/e4xclude_state.cc b/src/ic3/e4xclude_state.cc index 66464c41f..e468db34c 100644 --- a/src/ic3/e4xclude_state.cc +++ b/src/ic3/e4xclude_state.cc @@ -163,6 +163,9 @@ void CompInfo::add_new_elem(CUBE &St_cube,CUBE &Inp_assgn, PqElem El1; El1.tf_ind = tf_ind; El1.tbl_ind = Obl_table.size()-1; + El1.dist = dist; + El1.sort_mode = 1; + Pr_queue.push(El1); } /* end of function add_new_elem */ diff --git a/src/ic3/m0ic3.hh b/src/ic3/m0ic3.hh index 2b1cc8d28..1911794b3 100644 --- a/src/ic3/m0ic3.hh +++ b/src/ic3/m0ic3.hh @@ -161,7 +161,10 @@ public: // --------------- Parameters controlling algorithm's behavior - + + bool standard_mode; // if true, the algorithm simulates Bradley's version + // of ic3 published in 2013 + bool print_inv_flag; // if true, the invariant found by the program // (if any) is printed out char print_cex_flag; // 0 - counterexample (cex) is not printed out, diff --git a/src/ic3/p1arameters.cc b/src/ic3/p1arameters.cc index 8ef0a3e2e..1c536e27b 100644 --- a/src/ic3/p1arameters.cc +++ b/src/ic3/p1arameters.cc @@ -43,6 +43,8 @@ void ic3_enginet::read_parameters() Ci.constr_flag = true; + if (cmdline.isset("new-mode")) + Ci.standard_mode = false; } /* end of function read_parameters */ /*============================== @@ -86,7 +88,6 @@ void CompInfo::init_parameters() lift_sort_mode = FULL_SORT; ind_cls_sort_mode = FULL_SORT; gate_sort_mode = INPS_FIRST; - // gate_sort_mode = INIT_SORT; multiplier = 1.05; factor = 1.; max_act_val = 10000.; @@ -94,9 +95,9 @@ void CompInfo::init_parameters() ctg_flag = true; max_ctg_cnt = 3; max_rec_depth = 1; - grl_heur = NO_JOINS; max_coi_depth = 10; constr_flag = false; - + standard_mode = true; + } /* end of function init_parameters */ diff --git a/src/ic3/s3tat.cc b/src/ic3/s3tat.cc index d30d17dd4..33dc90a07 100644 --- a/src/ic3/s3tat.cc +++ b/src/ic3/s3tat.cc @@ -102,13 +102,7 @@ void CompInfo::print_flags() printf("ctg_flag = %d\n",ctg_flag); printf("constr_flag = %d\n",constr_flag); - // print state of generalization heuristic - printf("generalization heuristic = "); - if (grl_heur == NO_JOINS) printf("NO_JOINS\n"); - else { - assert(grl_heur == WITH_JOINS); - printf("WITH_JOINS\n"); - } + diff --git a/src/ic3/ttodo b/src/ic3/ttodo new file mode 100644 index 000000000..b5f751ce2 --- /dev/null +++ b/src/ic3/ttodo @@ -0,0 +1,60 @@ +===================== + + T O D O + +===================== +*) add code to the procedures affected by + the value of 'standard_mode' + + +) set_long_param("min_cls",0); + +) set_short_param2("act_upd_mode",BRAD_ACT_UPD); + +) set_long_param("comp_short",0); + + +) set_long_param("brad_obl",1); + +) set_long_param("act_obl",0); + +) set_long_param("sort_mode",1); + +) set_long_param("dyn_push",1); + +) set_long_param("mult_tried",0); + +*) add 'standard_mode' field + +*) add parameter --new_mode + +*) modify pushing for trivial time frames + +*) add parameter --stat + +*) add perl script that checks all the properties in a straightforward way + +*) remove grl_heur flag and the related code + +*) remove all the extra files I have added (scripts and so on) + + + +*) add code freeing memory allocated by the Verilog reader after IC3 + converted this information into its internal data + structure. (Keeping this memory is too expensive for large + examples.) + +================= + + D O N E + +================= +*) get rid of 'prop_ind' +*) modify 'find_prop' +*) replace '--prop' with '--property' +*) modify regression tests +*) eliminate the bug in generating constrained formulas +*) remove the performance bug caused by insufficient lifting + of CTG-states +*) add code to the procedures affected by + the value of 'standard_mode' +*) remove 'tf_ind' from 'exclude_state_cube' +*) update the way obligations are sorted + in the priority queue +*) add code updating the fields of an element + of priorty queue below + dist; + sort_mode; \ No newline at end of file From b4475c304d246a78345e2abf3ba621789bc8bc32 Mon Sep 17 00:00:00 2001 From: eigold Date: Thu, 25 May 2017 19:24:08 -0400 Subject: [PATCH 07/16] made more changes --- src/ic3/aux_types.hh | 5 ++++- src/ic3/e1xclude_state.cc | 4 +++- src/ic3/e2xclude_state.cc | 1 + src/ic3/m0ic3.hh | 4 ++-- src/ic3/m2ethods.hh | 2 +- src/ic3/next_time_frame.cc | 8 ++++++-- src/ic3/p2ush_clauses_forward.cc | 4 +++- src/ic3/s1tat.cc | 6 ++++-- src/ic3/s2horten_clause.cc | 3 ++- src/ic3/ttodo | 21 ++++++++++++++------- src/ic3/u1til.cc | 6 +++++- 11 files changed, 45 insertions(+), 19 deletions(-) diff --git a/src/ic3/aux_types.hh b/src/ic3/aux_types.hh index c3d97aaac..1b781ed03 100644 --- a/src/ic3/aux_types.hh +++ b/src/ic3/aux_types.hh @@ -184,7 +184,10 @@ struct TimeFrame int num_rcnt_ctis; // number of Cti-s generated in the current time frame // when processing the latest time frame - + + int num_seen_cls; // number of new cti or ctg clauses that are already in formula F + int num_redund_cls; // number of new cti/ctg clauses that are already in formula F + // and cannot be added to any time frame }; diff --git a/src/ic3/e1xclude_state.cc b/src/ic3/e1xclude_state.cc index f3c9c576e..ccc03bb5c 100644 --- a/src/ic3/e1xclude_state.cc +++ b/src/ic3/e1xclude_state.cc @@ -62,7 +62,9 @@ void CompInfo::exclude_state_cube(CNF &G,int &min_tf,CUBE &St0_cube,CUBE &Inps0) int succ_ind = Obl_table[tbl_ind].succ_ind; - bool ok = oblig_is_active(curr_tf+1,St_cube); + bool ok = true; + if (standard_mode) + ok = oblig_is_active(curr_tf+1,St_cube); if (!ok) { if (st_descr == OLD_STATE) triv_old_st_cnt++; diff --git a/src/ic3/e2xclude_state.cc b/src/ic3/e2xclude_state.cc index edc90188a..ba1242c7f 100644 --- a/src/ic3/e2xclude_state.cc +++ b/src/ic3/e2xclude_state.cc @@ -69,6 +69,7 @@ bool CompInfo::find_ind_subclause_cti(CLAUSE &C,SatSolver &Slvr, } // inductive clause is not found yet + if (standard_mode) return(false); CUBE St; extr_cut_assgns1(St,Pres_svars,Slvr); diff --git a/src/ic3/m0ic3.hh b/src/ic3/m0ic3.hh index 1911794b3..681bb1bcc 100644 --- a/src/ic3/m0ic3.hh +++ b/src/ic3/m0ic3.hh @@ -397,8 +397,8 @@ const int RAND_SORT = 3; const char OLD_STATE = 0; const char NEW_STATE = 1; const char ROOT_STATE = 2; -const char PUSH_STATE = 3; -const char CTG_STATE = 4; +const char CTG_STATE = 3; +const char PUSH_STATE = 4; const char UNKNOWN_STATE = 5; // values of 'grl_heur' diff --git a/src/ic3/m2ethods.hh b/src/ic3/m2ethods.hh index a372db461..75dac037f 100644 --- a/src/ic3/m2ethods.hh +++ b/src/ic3/m2ethods.hh @@ -9,7 +9,7 @@ void form_short_property(); void form_bad_states(); void form_bad_states0(CNF &Bstates); void exclude_state_cube(CNF &G,int &min_tf,CUBE &St,CUBE &Inps); -void push_clauses_forward(); +void push_clauses_forward(bool triv_time_frame); void init_time_frame_solver(int tf_ind); void init_bst_sat_solver(); void init_lbs_sat_solver(); diff --git a/src/ic3/next_time_frame.cc b/src/ic3/next_time_frame.cc index 05cb44b3a..8c2f93ac8 100644 --- a/src/ic3/next_time_frame.cc +++ b/src/ic3/next_time_frame.cc @@ -44,13 +44,15 @@ int CompInfo::next_time_frame() add_time_frame(); empty_cnts(); init_bst_sat_solver(); - + + bool triv_time_frame = true; while (true) { bool sat_form = check_sat1(Bst_sat); if (sat_form == false) { ret_val = 2; break;} + triv_time_frame = false; CUBE Nst,St,Inps; extr_cut_assgns1(Nst,Next_svars,Bst_sat); extr_next_inps(Inps,Bst_sat); @@ -99,7 +101,7 @@ int CompInfo::next_time_frame() if (rem_subsumed_flag) rem_redund_clauses(); simplify_tf_solvers(); Lgs_sat.Mst->simplify(); - push_clauses_forward(); + push_clauses_forward(triv_time_frame); if (inv_ind >= 0) return(0); @@ -143,6 +145,8 @@ void CompInfo::add_time_frame() Tf.tot_num_ctis = 0; Tf.num_rcnt_ctis = 0; Tf.num_bnd_cls = 0; + Tf.num_seen_cls = 0; + Tf.num_redund_cls = 0; Time_frames.push_back(Tf); diff --git a/src/ic3/p2ush_clauses_forward.cc b/src/ic3/p2ush_clauses_forward.cc index 4e4171b16..428c7b8ae 100644 --- a/src/ic3/p2ush_clauses_forward.cc +++ b/src/ic3/p2ush_clauses_forward.cc @@ -21,7 +21,7 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com P U S H _ C L A U S E S _ F O R W A R D ===========================================*/ -void CompInfo::push_clauses_forward() +void CompInfo::push_clauses_forward(bool triv_time_frame) { if (verbose == 0) { printf("%*c",3,' '); @@ -32,6 +32,8 @@ void CompInfo::push_clauses_forward() assert(tf_lind>=0 && (size_t) tf_lind < Time_frames.size()); init_fields(); + + if (triv_time_frame) min_tf = tf_lind; for (size_t i=min_tf; i <= (size_t) tf_lind; i++) { CUBE Pushed; CUBE &Clauses = Time_frames[i].Clauses; diff --git a/src/ic3/s1tat.cc b/src/ic3/s1tat.cc index 52bb415ab..963141de9 100644 --- a/src/ic3/s1tat.cc +++ b/src/ic3/s1tat.cc @@ -130,14 +130,15 @@ void CompInfo::print_time_frame_stat() printf("finished time frame number %d\n",(int) Time_frames.size()-1); } + TimeFrame &Tf = Time_frames[tf_lind]; if (verbose > 0) printf("new derived clauses Bnd[%d]=%d, Bnd[%d]=%d\n",tf_lind, - Time_frames[tf_lind].num_bnd_cls,tf_lind+1, + Tf.num_bnd_cls,tf_lind+1, Time_frames[tf_lind+1].num_bnd_cls); if (verbose > 0) { - printf("num_pbs-s: %d\n",Time_frames[tf_lind].num_pbss); + printf("num_pbs-s: %d\n",Tf.num_pbss); printf("Cti-s:\n"); int count = 0; @@ -158,6 +159,7 @@ void CompInfo::print_time_frame_stat() if (verbose > 0) my_printf("F.size() = %m, num. inact. clauses = %m\n",(int) F.size(), num_inact_cls); + printf("num. seen (redund) cls = %d (%d)\n",Tf.num_seen_cls,Tf.num_redund_cls); } /* end of function print_time_frame_stat*/ diff --git a/src/ic3/s2horten_clause.cc b/src/ic3/s2horten_clause.cc index fad864f3d..899687fb1 100644 --- a/src/ic3/s2horten_clause.cc +++ b/src/ic3/s2horten_clause.cc @@ -27,8 +27,9 @@ void CompInfo::shorten_clause(CLAUSE &C,int curr_tf,CLAUSE &C0,char st_descr, assert(curr_tf>=0 && (size_t) curr_tf < Time_frames.size()); CLAUSE B0 = C0; - + while (true) { + if (standard_mode) break; if (B0.size() < 10) break; CLAUSE B; compos_short(B,B0,curr_tf,st_descr); diff --git a/src/ic3/ttodo b/src/ic3/ttodo index b5f751ce2..1dc7d1a37 100644 --- a/src/ic3/ttodo +++ b/src/ic3/ttodo @@ -6,19 +6,18 @@ *) add code to the procedures affected by the value of 'standard_mode' - +) set_long_param("min_cls",0); + +) set_short_param2("act_upd_mode",BRAD_ACT_UPD); - +) set_long_param("comp_short",0); + +) set_long_param("brad_obl",1); +) set_long_param("act_obl",0); - +) set_long_param("sort_mode",1); +) set_long_param("dyn_push",1); +) set_long_param("mult_tried",0); *) add 'standard_mode' field -*) add parameter --new_mode + *) modify pushing for trivial time frames @@ -52,9 +51,17 @@ *) add code to the procedures affected by the value of 'standard_mode' *) remove 'tf_ind' from 'exclude_state_cube' -*) update the way obligations are sorted - in the priority queue *) add code updating the fields of an element of priorty queue below dist; - sort_mode; \ No newline at end of file + sort_mode; +*) add parameter --new_mode + +*) update the way obligations are sorted + in the priority queue + +) set_long_param("comp_short",0); + +) set_long_param("sort_mode",1); + +) set_long_param("min_cls",0); + + + diff --git a/src/ic3/u1til.cc b/src/ic3/u1til.cc index f486ee59a..47ed70f97 100644 --- a/src/ic3/u1til.cc +++ b/src/ic3/u1til.cc @@ -36,10 +36,14 @@ void CompInfo::add_fclause1(CLAUSE &C,int last_ind,char st_descr) int prev_tf_ind = -1; if (Clause_table.find(C) != Clause_table.end()) { + TimeFrame &Tf = Time_frames[tf_lind]; + if (st_descr <= CTG_STATE) Tf.num_seen_cls++; clause_ind1 = Clause_table[C]; prev_tf_ind = Clause_info[clause_ind1].span; - if (update_fclause(clause_ind1,last_ind) == false) + if (update_fclause(clause_ind1,last_ind) == false) { + if (st_descr <= CTG_STATE) Tf.num_redund_cls++; return; + } goto NEXT; } From 2bb57d6a3e9380c4f154ebe79d90d47edd10378f Mon Sep 17 00:00:00 2001 From: eigold Date: Fri, 26 May 2017 05:45:52 -0400 Subject: [PATCH 08/16] made more changes --- src/ic3/e1xclude_state.cc | 4 ++-- src/ic3/e3xclude_state.cc | 11 +++++++++-- src/ic3/e4xclude_state.cc | 2 +- src/ic3/s3tat.cc | 2 +- src/ic3/ttodo | 11 +++++------ 5 files changed, 18 insertions(+), 12 deletions(-) diff --git a/src/ic3/e1xclude_state.cc b/src/ic3/e1xclude_state.cc index ccc03bb5c..b47ffc590 100644 --- a/src/ic3/e1xclude_state.cc +++ b/src/ic3/e1xclude_state.cc @@ -63,8 +63,8 @@ void CompInfo::exclude_state_cube(CNF &G,int &min_tf,CUBE &St0_cube,CUBE &Inps0) int succ_ind = Obl_table[tbl_ind].succ_ind; bool ok = true; - if (standard_mode) - ok = oblig_is_active(curr_tf+1,St_cube); + + ok = oblig_is_active(curr_tf+1,St_cube); if (!ok) { if (st_descr == OLD_STATE) triv_old_st_cnt++; diff --git a/src/ic3/e3xclude_state.cc b/src/ic3/e3xclude_state.cc index dfdb59630..11c2b3237 100644 --- a/src/ic3/e3xclude_state.cc +++ b/src/ic3/e3xclude_state.cc @@ -45,12 +45,13 @@ void CompInfo::incr_short(CLAUSE &C,CLAUSE &C0,int curr_tf, if (C0.size() < max_tries) max_tries = C0.size(); size_t num_tries = 0; - + size_t loc_failed = 0; + while (true) { if (num_tries > max_tries) return; - if (Curr.size() <= Tried.size()) + if (Curr.size() <= loc_failed) return; int lit = pick_lit_to_remove(Curr,Tried,curr_tf); @@ -64,6 +65,7 @@ void CompInfo::incr_short(CLAUSE &C,CLAUSE &C0,int curr_tf, if (!ok) { Curr.push_back(lit); num_tries++; + loc_failed++; if (ctg_flag) Failed_lits.insert(lit); continue; } @@ -79,6 +81,7 @@ void CompInfo::incr_short(CLAUSE &C,CLAUSE &C0,int curr_tf, if (!ok) { failed_impr++; + loc_failed++; if (ctg_flag) Failed_lits.insert(lit); Curr.push_back(lit); num_tries++; @@ -92,6 +95,10 @@ void CompInfo::incr_short(CLAUSE &C,CLAUSE &C0,int curr_tf, if (C.size() == 1) return; Curr = C1; num_tries = 0; + if (!standard_mode) { + Tried.clear(); + loc_failed = 0; + } Tried.clear(); if (C1.size() < max_tries) max_tries = C1.size(); } diff --git a/src/ic3/e4xclude_state.cc b/src/ic3/e4xclude_state.cc index e468db34c..ee84b0f1d 100644 --- a/src/ic3/e4xclude_state.cc +++ b/src/ic3/e4xclude_state.cc @@ -119,7 +119,7 @@ bool CompInfo::cont_init_states(CUBE &St_cube) { bool CompInfo::oblig_is_active(int tf_ind,CUBE &St_cube) { - if (tf_ind > tf_lind) return(false); + if ((size_t) tf_ind >= Time_frames.size()) return(false); SatSolver &Slvr = Time_frames[tf_ind].Slvr; diff --git a/src/ic3/s3tat.cc b/src/ic3/s3tat.cc index 33dc90a07..5f74f1052 100644 --- a/src/ic3/s3tat.cc +++ b/src/ic3/s3tat.cc @@ -101,7 +101,7 @@ void CompInfo::print_flags() printf("selector = %d\n",selector); printf("ctg_flag = %d\n",ctg_flag); printf("constr_flag = %d\n",constr_flag); - + printf("standard_mode = %d\n",standard_mode); diff --git a/src/ic3/ttodo b/src/ic3/ttodo index 1dc7d1a37..8ff9469e3 100644 --- a/src/ic3/ttodo +++ b/src/ic3/ttodo @@ -11,11 +11,10 @@ +) set_long_param("brad_obl",1); - +) set_long_param("act_obl",0); +) set_long_param("dyn_push",1); - +) set_long_param("mult_tried",0); -*) add 'standard_mode' field + + @@ -56,12 +55,12 @@ dist; sort_mode; *) add parameter --new_mode +*) add 'standard_mode' field *) update the way obligations are sorted in the priority queue +) set_long_param("comp_short",0); +) set_long_param("sort_mode",1); +) set_long_param("min_cls",0); - - - + +) set_long_param("act_obl",0); + +) set_long_param("mult_tried",0); \ No newline at end of file From bb705b67c4840391e0794a4877ec83c50acbd448 Mon Sep 17 00:00:00 2001 From: eigold Date: Fri, 26 May 2017 08:19:22 -0400 Subject: [PATCH 09/16] almost finished patching code for the standard mode --- src/ebmc/r2esults_multi/sngl_call.bat | 6 ++--- src/ic3/e1xclude_state.cc | 37 ++++++++++++++++----------- src/ic3/m2ethods.hh | 2 +- src/ic3/ttodo | 7 ++--- src/ic3/u3til.cc | 14 ++++++++++ 5 files changed, 44 insertions(+), 22 deletions(-) diff --git a/src/ebmc/r2esults_multi/sngl_call.bat b/src/ebmc/r2esults_multi/sngl_call.bat index 7cb8dc40c..858eff0bf 100755 --- a/src/ebmc/r2esults_multi/sngl_call.bat +++ b/src/ebmc/r2esults_multi/sngl_call.bat @@ -3,10 +3,10 @@ limit cputime $1 #printf "$1 $2 $3\n" > $2_p$3.prot printf "exmp $2 prop. $3 " >> res.txt -../ebmc $2.sv --ic3 --property main.property.$3 > $2_p$3.prot +#../ebmc $2.sv --ic3 --property main.property.$3 > $2_p$3.prot ../ebmc $2.sv --ic3 --property main.property.$3 --constr > $2_p$3.prt -printf "no constr: " >> res.txt -grep property $2_p$3.prot | tr -d '\n' >> res.txt +#printf "no constr: " >> res.txt +#grep property $2_p$3.prot | tr -d '\n' >> res.txt printf ", with constr: " >> res.txt grep property $2_p$3.prt >> res.txt diff --git a/src/ic3/e1xclude_state.cc b/src/ic3/e1xclude_state.cc index b47ffc590..697746d60 100644 --- a/src/ic3/e1xclude_state.cc +++ b/src/ic3/e1xclude_state.cc @@ -61,10 +61,8 @@ void CompInfo::exclude_state_cube(CNF &G,int &min_tf,CUBE &St0_cube,CUBE &Inps0) int st_ind = tf_lind + 1 - dist; int succ_ind = Obl_table[tbl_ind].succ_ind; - - bool ok = true; - ok = oblig_is_active(curr_tf+1,St_cube); + bool ok = oblig_is_active(curr_tf+1,St_cube); if (!ok) { if (st_descr == OLD_STATE) triv_old_st_cnt++; @@ -88,21 +86,30 @@ void CompInfo::exclude_state_cube(CNF &G,int &min_tf,CUBE &St0_cube,CUBE &Inps0) std::cout << C << std::endl; } + if (succ_ind == -1) + G.push_back(C); + + // the set of obligations is not empty yet + int tf_ind1 = curr_tf+1; - if (tf_ind1 < tf_lind) { - CUBE Inps = Obl_table[tbl_ind].Inp_assgn; - add_new_elem(St_cube,Inps,tf_ind1+1,dist,succ_ind,OLD_STATE); + + if (standard_mode) + tf_ind1 = push_on_the_fly(curr_tf+1,C,st_descr); + + add_fclause1(C,tf_ind1,st_descr); + + if (standard_mode) { + if (tf_ind1 <= tf_lind) { + CUBE Inps = Obl_table[tbl_ind].Inp_assgn; + add_new_elem(St_cube,Inps,tf_ind1,dist,succ_ind,OLD_STATE); + } } + else + if (tf_ind1 < tf_lind) { + CUBE Inps = Obl_table[tbl_ind].Inp_assgn; + add_new_elem(St_cube,Inps,tf_ind1+1,dist,succ_ind,OLD_STATE); + } - - if (succ_ind == -1) { - G.push_back(C); - add_fclause1(C,curr_tf+1,st_descr); - continue; - } - - // the set of obligations is not empty yet - add_fclause1(C,curr_tf+1,st_descr); continue; } diff --git a/src/ic3/m2ethods.hh b/src/ic3/m2ethods.hh index 75dac037f..15e9dc1db 100644 --- a/src/ic3/m2ethods.hh +++ b/src/ic3/m2ethods.hh @@ -186,7 +186,7 @@ void form_property_gates(CUBE &Gates); 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); // // form CNF formulas void add_or_gate_cubes(DNF &F,int gate_ind,int shift); diff --git a/src/ic3/ttodo b/src/ic3/ttodo index 8ff9469e3..a79158ede 100644 --- a/src/ic3/ttodo +++ b/src/ic3/ttodo @@ -10,8 +10,7 @@ +) set_short_param2("act_upd_mode",BRAD_ACT_UPD); - +) set_long_param("brad_obl",1); - +) set_long_param("dyn_push",1); + @@ -63,4 +62,6 @@ +) set_long_param("sort_mode",1); +) set_long_param("min_cls",0); +) set_long_param("act_obl",0); - +) set_long_param("mult_tried",0); \ No newline at end of file + +) set_long_param("mult_tried",0); + +) set_long_param("brad_obl",1); + +) set_long_param("dyn_push",1); \ No newline at end of file diff --git a/src/ic3/u3til.cc b/src/ic3/u3til.cc index 769d10d77..51f63bcba 100644 --- a/src/ic3/u3til.cc +++ b/src/ic3/u3til.cc @@ -184,3 +184,17 @@ void CompInfo::full_sort(CLAUSE &C1,CLAUSE &C, std::vector &V) { } /* end of function full_sort */ +/*=================================== + + P U S H _ O N _ T H E _ F L Y + + =================================*/ +int CompInfo::push_on_the_fly(int last_ind,CLAUSE &C,char st_desc) +{ + + int tf_ind = latest_succ_tf_ind(last_ind,C); + if (tf_ind < 0) tf_ind = last_ind-1; + + return(tf_ind+1); + +} /* end of function push_on_the_fly */ From 03593fa6e2dfa0e7e089c440bc3eca490243392e Mon Sep 17 00:00:00 2001 From: eigold Date: Fri, 26 May 2017 14:15:53 -0400 Subject: [PATCH 10/16] added code for ctg_state lifting that ignores constraints --- src/ic3/c5tg.cc | 7 +++++-- src/ic3/l0ift_states.cc | 19 ++++++++++++------- src/ic3/m2ethods.hh | 2 +- 3 files changed, 18 insertions(+), 10 deletions(-) diff --git a/src/ic3/c5tg.cc b/src/ic3/c5tg.cc index 599c8c7a4..1db309f4b 100644 --- a/src/ic3/c5tg.cc +++ b/src/ic3/c5tg.cc @@ -81,8 +81,11 @@ void CompInfo::lift_ctg_state(CUBE &Ctg_cube,CUBE &Ctg_st,CUBE &Inps, add_assumps1(Assmps,Inps); - Mlit act_lit; - add_cls_excl_st_cube(act_lit,Lgs_sat,Nst_cube); + Mlit act_lit; + if (standard_mode) + add_cls_excl_st_cube(act_lit,Lgs_sat,Nst_cube,false); + else + add_cls_excl_st_cube(act_lit,Lgs_sat,Nst_cube,true); Assmps.push(act_lit); add_assumps2(Assmps,Ctg_st); diff --git a/src/ic3/l0ift_states.cc b/src/ic3/l0ift_states.cc index 517c78150..f3e2a374c 100644 --- a/src/ic3/l0ift_states.cc +++ b/src/ic3/l0ift_states.cc @@ -42,7 +42,7 @@ void CompInfo::lift_good_state(CUBE &Gst_cube,CUBE &Prs_st, Mlit act_lit; - add_cls_excl_st_cube(act_lit,Lgs_sat,Nst_cube); + add_cls_excl_st_cube(act_lit,Lgs_sat,Nst_cube,true); Assmps.push(act_lit); @@ -139,7 +139,7 @@ void CompInfo::gen_state_cube(CUBE &St_cube,CUBE &St,SatSolver &Slvr) A D D _ C L S _ E X C L _ S T _ C U B E ===========================================*/ -void CompInfo::add_cls_excl_st_cube(Mlit &act_lit,SatSolver &Slvr,CUBE &St) +void CompInfo::add_cls_excl_st_cube(Mlit &act_lit,SatSolver &Slvr,CUBE &St,bool add_cnstr_lits) { CLAUSE C; act_lit = IctMinisat::mkLit(Slvr.Mst->newVar(),false); @@ -155,12 +155,17 @@ void CompInfo::add_cls_excl_st_cube(Mlit &act_lit,SatSolver &Slvr,CUBE &St) // add literals constraining internal variables - for (size_t i=0; i < Tr_coi_lits.size(); i++) { - int lit = Tr_coi_lits[i]; - int var_ind = abs(lit)-1; - assert (Var_info[var_ind].type == INTERN); - C.push_back(-lit); + if (add_cnstr_lits) { + SCUBE::iterator pnt; + for (pnt = Constr_nilits.begin(); pnt != Constr_nilits.end(); pnt++) { + int lit = *pnt; + int var_ind = abs(lit)-1; + if (Var_info[var_ind].type != INTERN) continue; + C.push_back(-lit); + } } + + accept_new_clause(Slvr,C); diff --git a/src/ic3/m2ethods.hh b/src/ic3/m2ethods.hh index 15e9dc1db..c8f0cc01d 100644 --- a/src/ic3/m2ethods.hh +++ b/src/ic3/m2ethods.hh @@ -128,7 +128,7 @@ bool check_sat2(SatSolver &Slvr,MvecLits &Assmps); void add_negated_assumps1(MvecLits &Assmps,CLAUSE &C); void add_negated_assumps2(MvecLits &Assmps,CLAUSE &C,bool sort); void gen_assump_clause(CLAUSE &C,SatSolver &Slvr,MvecLits &Assmps); -void add_cls_excl_st_cube(Mlit &act_lit,SatSolver &Slvr,CUBE &St); +void add_cls_excl_st_cube(Mlit &act_lit,SatSolver &Slvr,CUBE &St,bool add_cnstr_lits); void add_temp_clause(Mlit &act_lit,SatSolver &Slvr,CLAUSE &C); void simplify_tf_solvers(); void print_tf_assgns(int tf_ind); From 84fa05eec719d91e1e1e9fad1321085969e6eb91 Mon Sep 17 00:00:00 2001 From: eigold Date: Fri, 26 May 2017 19:40:17 -0400 Subject: [PATCH 11/16] adding a usefule script --- src/ebmc/r2esults_multi/run_ic3.pl | 70 ++++++++++++++++++++++++++++++ 1 file changed, 70 insertions(+) create mode 100755 src/ebmc/r2esults_multi/run_ic3.pl diff --git a/src/ebmc/r2esults_multi/run_ic3.pl b/src/ebmc/r2esults_multi/run_ic3.pl new file mode 100755 index 000000000..a9af4b1a1 --- /dev/null +++ b/src/ebmc/r2esults_multi/run_ic3.pl @@ -0,0 +1,70 @@ +#!/usr/bin/perl + +if ($#ARGV == -1) { + printf("run_ic3.pl exmps\n"); + exit(0); +} + + +qx(rm -f res.txt); +qx(rm -f *.prt); + +$exmp_path = "/home/eugene/e0xamples/hwmcc12/multi"; + +(my $fname) = @ARGV; + +$time_limit = 800; + +open EXMPS,"< $fname" or die "failed to open file $fname\n"; + +while () { + chomp($_); + $exmp = $_; + + @words = split / /,$exmp; + + # print "@words"; + + $name = $words[0]; + + printf "$name\n"; + + qx(cp $exmp_path/$name.aig .); + + + $i = 0; + foreach (@words) { + $i++; + if ($i == 1) {next;} + printf(" prop. $_\n"); + $ind = $_ - 1; + $prot_name = $name . _p . $_; + + + $pid = fork(); + die if not defined $pid; + if ($pid > 0) { +# printf "%d\n",$pid; + eval { + local $SIG{ALRM} = sub {kill 9, -$pid; die "alarm\n"}; + alarm 1000; + waitpid($pid, 0); + alarm 0; + }; + } + elsif ($pid == 0) { + setpgrp(0,0); + exec("iic3 < $name.aig -s $ind > $prot_name.prt"); + exit(0); + } + + } + +# printf("%s\n",$num_prop); + + qx(rm -f $name.aig); +} + +close EXMPS; + + From 26026710defdd915d23bf8b0dad0bf5e73e60e57 Mon Sep 17 00:00:00 2001 From: eigold Date: Sat, 27 May 2017 15:47:35 -0400 Subject: [PATCH 12/16] added an option to conver a verilog description into a aiger file --- src/ebmc/ebmc_parse_options.cpp | 4 +- src/ebmc/ebmc_parse_options.h | 2 +- src/ic3/Makefile | 3 +- src/ic3/m0ic3.hh | 5 +- src/ic3/m1ain.cc | 6 + src/ic3/m2ethods.hh | 18 ++- src/ic3/m4y_aiger_print.cc | 239 ++++++++++++++++++++++++++++++++ src/ic3/m5y_aiger_print.cc | 196 ++++++++++++++++++++++++++ src/ic3/r3ead_input.cc | 30 ++-- src/ic3/seq_circ/ccircuit.hh | 1 + src/ic3/ttodo | 20 +-- 11 files changed, 500 insertions(+), 24 deletions(-) create mode 100644 src/ic3/m4y_aiger_print.cc create mode 100644 src/ic3/m5y_aiger_print.cc diff --git a/src/ebmc/ebmc_parse_options.cpp b/src/ebmc/ebmc_parse_options.cpp index 29fdc70e0..eb81aeb26 100644 --- a/src/ebmc/ebmc_parse_options.cpp +++ b/src/ebmc/ebmc_parse_options.cpp @@ -264,8 +264,10 @@ void ebmc_parse_optionst::help() " --ic3 [options] use IC3 engine with options described below\n" " --property check property named \n" " --constr use constraints specified in 'file.cnstr'\n" - " --help print out help information\n" + " --h print out help information\n" " --new-mode new mode is switched on\n" + " --aiger print out the instance in aiger format\n" + //" --interpolation use bit-level interpolants\n" //" --interpolation-word use word-level interpolants\n" //" --diameter perform recurrence diameter test\n" diff --git a/src/ebmc/ebmc_parse_options.h b/src/ebmc/ebmc_parse_options.h index 1415a3489..12b5da456 100644 --- a/src/ebmc/ebmc_parse_options.h +++ b/src/ebmc/ebmc_parse_options.h @@ -32,7 +32,7 @@ class ebmc_parse_optionst:public parse_options_baset "(reset):" "(version)(verilog-rtl)(verilog-netlist)" "(compute-interpolant)(interpolation)(interpolation-vmcai)" - "(ic3)(property):(constr)(h)(new-mode)" + "(ic3)(property):(constr)(h)(new-mode)(aiger)" "(interpolation-word)(interpolator):(bdd)" "(smt1)(smt2)(boolector)(z3)(cvc4)(yices)(mathsat)(prover)(lifter)" "(aig)(stop-induction)(stop-minimize)(start):(coverage)(naive)" diff --git a/src/ic3/Makefile b/src/ic3/Makefile index 04a541e89..4e637cc5f 100644 --- a/src/ic3/Makefile +++ b/src/ic3/Makefile @@ -30,7 +30,8 @@ SEQ_CIRC = $(OBJ_DIR)/p1rint_blif.o $(OBJ_DIR)/p2rint_blif.o $(OBJ_DIR)/finish_g $(OBJ_DIR)/circuit.o $(OBJ_DIR)/a4dd_spec_buffs.o $(OBJ_DIR)/a5dd_spec_buffs.o \ $(OBJ_DIR)/l0ast_touch.o $(OBJ_DIR)/l1ast_touch.o -OBJ_ROOT = $(OBJ_DIR)/r7ead_input.o $(OBJ_DIR)/r6ead_input.o \ +OBJ_ROOT = $(OBJ_DIR)/m5y_aiger_print.o \ + $(OBJ_DIR)/m4y_aiger_print.o $(OBJ_DIR)/r7ead_input.o $(OBJ_DIR)/r6ead_input.o \ $(OBJ_DIR)/g2ate_ord.o $(OBJ_DIR)/i4nit_sat_solvers.o $(OBJ_DIR)/l1ift_states.o \ $(OBJ_DIR)/r5ead_input.o $(OBJ_DIR)/r4ead_input.o $(OBJ_DIR)/c4oi.o \ $(OBJ_DIR)/c5tg.o $(OBJ_DIR)/c2tg.o $(OBJ_DIR)/r3ead_input.o \ diff --git a/src/ic3/m0ic3.hh b/src/ic3/m0ic3.hh index 681bb1bcc..e6a31e385 100644 --- a/src/ic3/m0ic3.hh +++ b/src/ic3/m0ic3.hh @@ -24,7 +24,9 @@ public: // Ordering[i] == i std::string prop_name; // specifies the name of the property to be checked - + bool const_true_prop; // if 'true', the property is a constant 'true' + bool const_false_prop; // if true, the property is a constant 'false' + CUBE Gate_to_var; // gate_to_var[gate_ind] gives the variable assigned to // the output of gate 'gate_ind' @@ -263,6 +265,7 @@ public: void form_consts(Circuit *N); void form_constr_lits(); void add_constrs(); + void print_aiger_format(); protected: diff --git a/src/ic3/m1ain.cc b/src/ic3/m1ain.cc index e9b5bcb03..d37334d08 100644 --- a/src/ic3/m1ain.cc +++ b/src/ic3/m1ain.cc @@ -81,6 +81,12 @@ int ic3_enginet::operator()() read_ebmc_input(); + if (cmdline.isset("aiger")) { + printf("converting to aiger format\n"); + Ci.print_aiger_format(); + exit(0); + } + // printf("Constr_gates.size() = %d\n",Ci.Constr_gates.size()); return(Ci.run_ic3()); diff --git a/src/ic3/m2ethods.hh b/src/ic3/m2ethods.hh index c8f0cc01d..a8fec08b5 100644 --- a/src/ic3/m2ethods.hh +++ b/src/ic3/m2ethods.hh @@ -206,5 +206,19 @@ void gate_sort_inps_first(); void gate_sort_outs_first(); void rand_gate_order(); void print_gate_sort_mode(); - - +// +// related to printing out circuit in aiger format +void check_circuit(int &num_buffs,int &num_consts); +void print_aiger_header(FILE *fp,int max_var,int num_gates); +void print_aiger_inps(FILE *fp); +void print_aiger_latches(FILE *fp); +int find_aiger_lit1(int gate_ind,char polarity); +int find_aiger_lit2(int gate_ind,char polarity); +void print_aiger_gates(FILE *fp,DNF &Gates); +void add_aiger_and_gate(DNF &Gates,int gate_ind); +void add_aiger_buffer(DNF &Gates,int gate_ind); +void print_aiger_output(FILE *fp,DNF &Gates,int out_ind); +int form_aiger_gates(DNF &Gates); +void add_triplet(DNF &Gates,int olit,int lit0,int lit1); +int find_max_aiger_var(DNF &Gates); +void print_aiger_constrs(FILE *fp); diff --git a/src/ic3/m4y_aiger_print.cc b/src/ic3/m4y_aiger_print.cc new file mode 100644 index 000000000..7e9e9a181 --- /dev/null +++ b/src/ic3/m4y_aiger_print.cc @@ -0,0 +1,239 @@ +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include + +#include + +#include "minisat/core/Solver.h" +#include "minisat/simp/SimpSolver.h" + + +using namespace std; +#include "dnf_io.hh" +#include "ccircuit.hh" +#include "m0ic3.hh" + +/*==================================== + + P R I N T _ A I G E R _ F O R M A T + + ====================================*/ +void CompInfo::print_aiger_format() +{ + + int num_consts; + int num_buffs; + check_circuit(num_buffs,num_consts); + // printf("num_buffs = %d\n",num_buffs); + assert(num_consts <= 2); + string full_name; + assert(strlen(out_file) > 0); + full_name = out_file; + full_name += ".aag"; + + FILE *fp = fopen(full_name.c_str(),"w"); + assert(fp!= NULL); + + DNF Gates; + int out_ind = form_aiger_gates(Gates); + + int max_var = find_max_aiger_var(Gates); + print_aiger_header(fp,max_var,Gates.size()); + print_aiger_inps(fp); + print_aiger_latches(fp); + print_aiger_output(fp,Gates,out_ind); + print_aiger_constrs(fp); + print_aiger_gates(fp,Gates); + fclose(fp); +} /* end of function print_aiger_format */ + +/*======================================= + + F O R M _ A I G E R _ G A T E S + + =======================================*/ +int CompInfo::form_aiger_gates(DNF &Gates) +{ + + int ind = -1; + assert(N->Outputs.size() == 1); + size_t out_gate_ind = N->Outputs[0]; + for (size_t i=0; i < N->Gate_list.size(); i++) { + Gate &G = N->Gate_list[i]; + if (G.gate_type == INPUT) continue; + if (G.gate_type == LATCH) continue; + if (G.func_type == CONST) continue; + assert(G.ninputs <= 2); + if (i == out_gate_ind) + ind = Gates.size(); + if (G.func_type == AND) { + add_aiger_and_gate(Gates,i); + continue; + } + assert(G.func_type == BUFFER); + add_aiger_buffer(Gates,i); + } + assert(ind >= 0); + return(ind); + +} /* end of function form_aiger_gates */ +/*================================= + + F I N D _ A I G E R _ L I T 1 + + ================================*/ +int CompInfo::find_aiger_lit1(int gate_ind,char polarity) +{ + + Gate &G = N->get_gate(gate_ind); + + if (G.func_type == CONST) { + if (G.F.size() > 0) return(1); + else { + assert(F.size() == 0); + return(0); + } + } + + int lit = (gate_ind+1) << 1; + if (polarity) return(lit+1); + else return(lit); + +} /* end of function find_aiger_lit1 */ + +/*================================= + + F I N D _ A I G E R _ L I T 2 + + ================================*/ +int CompInfo::find_aiger_lit2(int gate_ind,char polarity) +{ + + + int lit = (gate_ind+1) << 1; + if (polarity) return(lit+1); + else return(lit); + +} /* end of function find_aiger_lit2 */ + +/*======================================== + + P R I N T _ A I G E R _ L A T C H E S + + ======================================*/ +void CompInfo::print_aiger_latches(FILE *fp) +{ + + for (size_t i=0; i < N->Latches.size(); i++) { + int gate_ind = N->Latches[i]; + int lit = (gate_ind+1) << 1; + fprintf(fp,"%d ",lit); + Gate &G = N->get_gate(gate_ind); + assert(G.Fanin_list.size() == 1); + int next_lit = find_aiger_lit1(G.Fanin_list[0],0); + fprintf(fp,"%d ",next_lit); + if (G.init_value == 2) { + fprintf(fp,"%d\n",lit); + continue;} + assert((G.init_value == 0) || (G.init_value == 1)); + fprintf(fp,"%d\n",G.init_value); + } + +} /* end of function print_aiger_latches */ + + +/*======================================== + + P R I N T _ A I G E R _ I N P S + + ======================================*/ +void CompInfo::print_aiger_inps(FILE *fp) +{ + + for (size_t i=0; i < N->Inputs.size(); i++) { + int gate_ind = N->Inputs[i]; + fprintf(fp,"%d\n",(gate_ind+1)<<1); + } + +} /* end of function print_aiger_inps */ + + +/*======================================== + + P R I N T _ A I G E R _ H E A D E R + + ======================================*/ +void CompInfo::print_aiger_header(FILE *fp,int max_var,int num_gates) +{ + + fprintf(fp,"aag "); + + fprintf(fp,"%d ",max_var); + fprintf(fp,"%d ",N->ninputs); + fprintf(fp,"%d ",N->nlatches); + fprintf(fp,"1 "); + fprintf(fp,"%d",num_gates); + if (Constr_gates.size() == 0) fprintf(fp,"\n"); + else fprintf(fp," 0 %d\n",(int) Constr_gates.size()); +} /* end of function print_aiger_header*/ + + + + +/*============================== + + C H E C K _ C I R C U I T + + ===============================*/ +void CompInfo::check_circuit(int &num_buffs,int &num_consts) +{ + + num_consts = 0; + num_buffs = 0; + for (size_t i=0; i < N->Gate_list.size(); i++) { + Gate &G = N->Gate_list[i]; + if (G.gate_type == INPUT) continue; + if (G.gate_type == LATCH) continue; + assert(G.gate_type == GATE); + bool cond = (G.func_type == AND); + cond |= (G.func_type == BUFFER); + cond |= (G.func_type == CONST); + if (!cond) { + p(); + print_func_type(G); + exit(100); + } + + if (G.func_type == CONST) num_consts++; + if (G.func_type == BUFFER) num_buffs++; + + if (G.ninputs != 2) { + bool cond = (i == N->Gate_list.size()-2); + cond |= (G.func_type == BUFFER); + cond |= (G.func_type == CONST); + if (!cond) { + p(); + printf("i = %d\n",i); + printf("N->Gate_list.size() = %d\n",(int) N->Gate_list.size()); + printf("G.ninputs = %d\n",G.ninputs); + exit(100); + } + } + } + +} /* end of function check_circuit */ diff --git a/src/ic3/m5y_aiger_print.cc b/src/ic3/m5y_aiger_print.cc new file mode 100644 index 000000000..bef3621c4 --- /dev/null +++ b/src/ic3/m5y_aiger_print.cc @@ -0,0 +1,196 @@ +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include + +#include + +#include "minisat/core/Solver.h" +#include "minisat/simp/SimpSolver.h" + +using namespace std; +#include "dnf_io.hh" +#include "ccircuit.hh" +#include "m0ic3.hh" + +/*=========================================== + + P R I N T _ A I G E R _ C O N S T R S + + ============================================*/ +void CompInfo::print_aiger_constrs(FILE *fp) +{ + + ConstrGates::iterator pnt; + + for (pnt = Constr_gates.begin(); pnt!= Constr_gates.end(); pnt++) { + int gate_ind = pnt->first; + char neg_lit = pnt->second.neg_lit; + int lit = find_aiger_lit2(gate_ind,neg_lit); + fprintf(fp,"%d\n",lit); + } +} /* end of function print_aiger_constrs */ + +/*============================================ + + P R I N T _ A I G E R _ G A T E S + + ==========================================*/ +void CompInfo::print_aiger_gates(FILE *fp,DNF &Gates) +{ + + for (size_t i=0; i < Gates.size(); i++) { + CUBE &C = Gates[i]; + assert(C.size() == 3); + fprintf(fp,"%d %d %d\n",C[0],C[1],C[2]); + } + +} /* end of function print_aiger_gates */ + +/*=============================== + + A D D _ T R I P L E T + + ==============================*/ +void CompInfo::add_triplet(DNF &Gates,int olit,int lit0,int lit1) +{ + + CUBE C; + C.push_back(olit); C.push_back(lit0); C.push_back(lit1); + Gates.push_back(C); + +} /* end of function add_triplet */ + + + +/*========================================= + + F I N D _ M A X _ A I G E R _ V A R + + =========================================*/ +int CompInfo::find_max_aiger_var(DNF &Gates) +{ + + int max_lit = -1; + for (size_t i=0; i < Gates.size(); i++) { + CUBE &C = Gates[i]; + for (size_t j=0; j < C.size(); j++) + if (C[j] > max_lit) max_lit = C[j]; + } + + assert(max_lit >= 0); + if (max_lit & 1) max_lit--; + return(max_lit >> 1); +} /* end of function find_max_aiger_var */ + + + +/*========================================== + + P R I N T _ A I G E R _ O U T P U T + + ==========================================*/ +void CompInfo::print_aiger_output(FILE *fp,DNF &Gates,int out_ind) +{ + CUBE &C = Gates[out_ind]; + assert(C.size() == 3); + int lit = C[0]; + + if (const_true_prop) { // make sure that the output is always 0 + assert(C[1] == C[2]); + if (C[1] == 1) lit++; // negate the conjunction of constants 1 + } + + if (const_false_prop) { // make sure that the output is always 1 + if ((C[1] == 0) || (C[2] == 0)) // at least one of the inputs is 0 + lit++; + } + fprintf(fp,"%d\n",lit); +} /* end of function print_aiger_output */ + +/*============================================= + + A D D _ A I G E R _ A N D _ G A T E + + ============================================*/ +void CompInfo::add_aiger_and_gate(DNF &Gates,int gate_ind) +{ + + Gate &G = N->get_gate(gate_ind); + assert(G.Polarity.back() == 0); + int olit = find_aiger_lit1(gate_ind,0); + int lit0 = find_aiger_lit1(G.Fanin_list[0],G.Polarity[0]); + int lit1 = find_aiger_lit1(G.Fanin_list[1],G.Polarity[1]); + + add_triplet(Gates,olit,lit0,lit1); + + +} /* end of function add_aiger_and_gate */ + +/*============================================= + + A D D _ A I G E R _ B U F F E R + + ============================================*/ +void CompInfo::add_aiger_buffer(DNF &Gates,int gate_ind) +{ + + Gate &G = N->get_gate(gate_ind); + assert(G.Polarity.back() == 0); + int olit = find_aiger_lit1(gate_ind,0); + int ilit = find_aiger_lit1(G.Fanin_list[0],G.Polarity[0]); + + add_triplet(Gates,olit,ilit,ilit); + +} /* end of function add_aiger_buffer */ + +/*================================= + + P R I N T _ F U N C _ T Y P E + + ================================*/ +void print_func_type(Gate &G) +{ + + switch (G.func_type) { + case CONST: + printf("CONST"); + break; + case BUFFER: + printf("BUFFER"); + break; + case AND: + printf("AND"); + break; + case OR: + printf("OR"); + break; + case TRUTH_TABLE: + printf("TRUTH_TABLE"); + break; + case COMPLEX: + printf("COMPLEX"); + break; + default: + printf("wrong value of func_type\n"); + exit(100); + } + + printf("\n"); + +} /* end of function print_func_type */ + diff --git a/src/ic3/r3ead_input.cc b/src/ic3/r3ead_input.cc index e4dd77b32..0b00cbec8 100644 --- a/src/ic3/r3ead_input.cc +++ b/src/ic3/r3ead_input.cc @@ -185,9 +185,19 @@ void ic3_enginet::form_gates() void ic3_enginet::form_outp_buf(CDNF &Out_names) { - int olit = prop_l.get(); - if (prop_l.is_constant() == 0) - if (prop_l.sign()) olit--; + + unsigned olit = prop_l.get(); + + Ci.const_false_prop = false; + Ci.const_true_prop = false; + + if (prop_l.is_constant() == 0) + if (prop_l.sign()) + olit--; + + + + assert(Ci.Inps.find(olit) == Ci.Inps.end()); @@ -200,13 +210,15 @@ void ic3_enginet::form_outp_buf(CDNF &Out_names) Pin_names.push_back(Dummy); char Buff[MAX_NAME]; if (prop_l.is_false()) { - sprintf(Buff,"c0"); - conv_to_vect(Pin_names[0],Buff); - goto NEXT; } + Ci.const_false_prop = true; + sprintf(Buff,"c0"); + conv_to_vect(Pin_names[0],Buff); + goto NEXT; } if (prop_l.is_true()) { - sprintf(Buff,"c1"); - conv_to_vect(Pin_names[0],Buff); - goto NEXT; + Ci.const_true_prop = true; + sprintf(Buff,"c1"); + conv_to_vect(Pin_names[0],Buff); + goto NEXT; } if (orig_names) diff --git a/src/ic3/seq_circ/ccircuit.hh b/src/ic3/seq_circ/ccircuit.hh index f676bea29..d037a6748 100644 --- a/src/ic3/seq_circ/ccircuit.hh +++ b/src/ic3/seq_circ/ccircuit.hh @@ -196,6 +196,7 @@ void my_printf(char *format,...); void remove_unobserv_gates(Circuit *N); void print_header1(Circuit *N); void print_names2(Circuit *N,CUBE &gates); +void print_func_type(Gate &G); #include "more_fun_prot.hh" diff --git a/src/ic3/ttodo b/src/ic3/ttodo index a79158ede..210500342 100644 --- a/src/ic3/ttodo +++ b/src/ic3/ttodo @@ -3,6 +3,11 @@ T O D O ===================== +*) polish the header part of 'm4y_aiger_print.cc + and 'm5y_aiger_print.cc' (take into account + Matthias' PR) + + *) add code to the procedures affected by the value of 'standard_mode' @@ -13,18 +18,10 @@ - - - - -*) modify pushing for trivial time frames - *) add parameter --stat *) add perl script that checks all the properties in a straightforward way -*) remove grl_heur flag and the related code - *) remove all the extra files I have added (scripts and so on) @@ -64,4 +61,9 @@ +) set_long_param("act_obl",0); +) set_long_param("mult_tried",0); +) set_long_param("brad_obl",1); - +) set_long_param("dyn_push",1); \ No newline at end of file + +) set_long_param("dyn_push",1); +*) modify pushing for trivial time frames +*) remove grl_heur flag and the related code +*) remove add_final_gates +*) add option to print out the circuit in + the aiger format \ No newline at end of file From e1cb500f44b37d46ba4828a57563ea04519abdb3 Mon Sep 17 00:00:00 2001 From: eigold Date: Mon, 29 May 2017 15:30:14 -0400 Subject: [PATCH 13/16] polished the version of ic3_bugs branch before submitting PR --- regression/ebmc/ic3/exmp1/test.desc | 4 +- regression/ebmc/ic3/exmp2/test.desc | 4 +- regression/ebmc/ic3/exmp3/test.desc | 4 +- regression/ebmc/ic3/exmp4/test.desc | 4 +- regression/ebmc/ic3/exmp5/test.desc | 4 +- regression/ebmc/ic3/exmp6/test.desc | 4 +- regression/ebmc/ic3/exmp7/test.desc | 4 +- regression/ebmc/ic3/exmp8/test.desc | 4 +- regression/ebmc/ic3/exmp9/test.desc | 4 +- regression/ebmc/ic3/non_inductive1/test.desc | 3 +- src/ebmc/pproc_all.bat | 63 ------------------ src/ebmc/r1esults_multi/exmps11 | 6 -- src/ebmc/r1esults_multi/multi_prop.pl | 52 --------------- src/ebmc/r1esults_multi/rpnt.txt | 17 ----- src/ebmc/r1esults_multi/sngl_call.bat | 6 -- src/ebmc/r2esults_multi/exmps12 | 4 -- src/ebmc/r2esults_multi/multi_prop.pl | 52 --------------- src/ebmc/r2esults_multi/rpnt.txt | 15 ----- src/ebmc/r2esults_multi/run_ic3.pl | 70 -------------------- src/ebmc/r2esults_multi/sngl_call.bat | 12 ---- src/ebmc/rregr_testing.bat | 12 ---- src/ic3/README | 6 +- src/ic3/e2xclude_state.cc | 2 +- src/ic3/l0ift_states.cc | 3 +- src/ic3/m4y_aiger_print.cc | 28 +++----- src/ic3/m5y_aiger_print.cc | 24 +++---- src/ic3/p2ush_clauses_forward.cc | 2 +- src/ic3/s1tat.cc | 3 +- src/ic3/todo | 21 +++--- src/ic3/ttodo | 69 ------------------- src/ic3/v0erify.cc | 8 +-- src/ic3/v1erify.cc | 6 +- 32 files changed, 63 insertions(+), 457 deletions(-) delete mode 100755 src/ebmc/pproc_all.bat delete mode 100644 src/ebmc/r1esults_multi/exmps11 delete mode 100755 src/ebmc/r1esults_multi/multi_prop.pl delete mode 100644 src/ebmc/r1esults_multi/rpnt.txt delete mode 100755 src/ebmc/r1esults_multi/sngl_call.bat delete mode 100644 src/ebmc/r2esults_multi/exmps12 delete mode 100755 src/ebmc/r2esults_multi/multi_prop.pl delete mode 100644 src/ebmc/r2esults_multi/rpnt.txt delete mode 100755 src/ebmc/r2esults_multi/run_ic3.pl delete mode 100755 src/ebmc/r2esults_multi/sngl_call.bat delete mode 100755 src/ebmc/rregr_testing.bat delete mode 100644 src/ic3/ttodo diff --git a/regression/ebmc/ic3/exmp1/test.desc b/regression/ebmc/ic3/exmp1/test.desc index 5b1c18842..dce1ecb36 100644 --- a/regression/ebmc/ic3/exmp1/test.desc +++ b/regression/ebmc/ic3/exmp1/test.desc @@ -2,6 +2,6 @@ CORE pdtvispeterson.sv --ic3 ^property HOLDS -^verification is ok +^inductive invariant verification is ok -- -^verification failed +^inductive invariant verification failed diff --git a/regression/ebmc/ic3/exmp2/test.desc b/regression/ebmc/ic3/exmp2/test.desc index 6a9e58e91..6fbd5915a 100644 --- a/regression/ebmc/ic3/exmp2/test.desc +++ b/regression/ebmc/ic3/exmp2/test.desc @@ -2,6 +2,6 @@ CORE bobcount.sv --ic3 ^property HOLDS -^verification is ok +^inductive invariant verification is ok -- -^verification failed +^inductive invariant verification failed diff --git a/regression/ebmc/ic3/exmp3/test.desc b/regression/ebmc/ic3/exmp3/test.desc index be741a611..c0d5ce9d8 100644 --- a/regression/ebmc/ic3/exmp3/test.desc +++ b/regression/ebmc/ic3/exmp3/test.desc @@ -2,6 +2,6 @@ CORE viseisenberg.sv --ic3 ^property FAILED -^verification is ok +^cex verification is ok -- -^verification failed +^cex verification failed diff --git a/regression/ebmc/ic3/exmp4/test.desc b/regression/ebmc/ic3/exmp4/test.desc index f3efd98e9..5eabfd3f1 100644 --- a/regression/ebmc/ic3/exmp4/test.desc +++ b/regression/ebmc/ic3/exmp4/test.desc @@ -2,6 +2,6 @@ CORE visbakery.sv --ic3 ^property FAILED -^verification is ok +^cex verification is ok -- -^verification failed +^cex verification failed diff --git a/regression/ebmc/ic3/exmp5/test.desc b/regression/ebmc/ic3/exmp5/test.desc index f78158b8e..6802810bd 100644 --- a/regression/ebmc/ic3/exmp5/test.desc +++ b/regression/ebmc/ic3/exmp5/test.desc @@ -2,6 +2,6 @@ CORE ringp0.sv --ic3 ^property FAILED -^verification is ok +^cex verification is ok -- -^verification failed +^cex verification failed diff --git a/regression/ebmc/ic3/exmp6/test.desc b/regression/ebmc/ic3/exmp6/test.desc index 0c98ae529..3e54ad980 100644 --- a/regression/ebmc/ic3/exmp6/test.desc +++ b/regression/ebmc/ic3/exmp6/test.desc @@ -2,6 +2,6 @@ CORE eijks208o.sv --ic3 ^property HOLDS -^verification is ok +^inductive invariant verification is ok -- -^verification failed +^inductive invariant verification failed diff --git a/regression/ebmc/ic3/exmp7/test.desc b/regression/ebmc/ic3/exmp7/test.desc index 83e6e358f..7934594c4 100644 --- a/regression/ebmc/ic3/exmp7/test.desc +++ b/regression/ebmc/ic3/exmp7/test.desc @@ -2,6 +2,6 @@ CORE bobmiterbm1multi.sv --ic3 --property bobmiterbm1multi.property.1033 ^property HOLDS -^verification is ok +^inductive invariant verification is ok -- -^verification failed +^inductive invariant verification failed diff --git a/regression/ebmc/ic3/exmp8/test.desc b/regression/ebmc/ic3/exmp8/test.desc index f7ac65a33..65d962e4b 100644 --- a/regression/ebmc/ic3/exmp8/test.desc +++ b/regression/ebmc/ic3/exmp8/test.desc @@ -2,6 +2,6 @@ CORE bobmiterbm1multi.sv --ic3 --property bobmiterbm1multi.property.1080 ^property FAILED -^verification is ok +^cex verification is ok -- -^verification failed +^cex verification failed diff --git a/regression/ebmc/ic3/exmp9/test.desc b/regression/ebmc/ic3/exmp9/test.desc index afcf7297b..cf94b9c03 100644 --- a/regression/ebmc/ic3/exmp9/test.desc +++ b/regression/ebmc/ic3/exmp9/test.desc @@ -2,6 +2,6 @@ CORE sm98a7multi.sv --ic3 --property sm98a7multi.property.2 --constr ^property FAILED -^verification is ok +^cex verification is ok -- -^verification failed +^cex verification failed diff --git a/regression/ebmc/ic3/non_inductive1/test.desc b/regression/ebmc/ic3/non_inductive1/test.desc index b9e04d1c8..6a37b38ca 100644 --- a/regression/ebmc/ic3/non_inductive1/test.desc +++ b/regression/ebmc/ic3/non_inductive1/test.desc @@ -2,5 +2,6 @@ CORE non_inductive.sv --ic3 --property main.property.p0 ^property HOLDS$ -^verification is ok +^inductive invariant verification is ok -- +^inductive invariant verification failed diff --git a/src/ebmc/pproc_all.bat b/src/ebmc/pproc_all.bat deleted file mode 100755 index 2b5af593f..000000000 --- a/src/ebmc/pproc_all.bat +++ /dev/null @@ -1,63 +0,0 @@ -# -limit cputime 65 -limit vmemoryuse 2800 megabytes -set bench_dir = /home/eugene/e0xamples/hwmcc10 - -rrm -rf r0esults/$1.prot - -foreach file (`cat $1`) - -printf "--------------\n" -printf "$file ::\n" - - -ccp $bench_dir/$file.aig r0esults -cd r0esults -ba2ver $file.aig $file.sv - -printf "%s: " $file >> $1.prot -time ../ebmc $file.sv --ic3 >& $file.prt -set stat_var = $status -if ($stat_var >= 100) then -printf "unconventional termination\n" >> $1.prot -cd .. -continue -endif -if ($stat_var > 10) then -@ stat_var0 = $stat_var - 10 -else -@ stat_var0 = $stat_var -endif -if ($stat_var0 == 0) then -printf "unsolved\n" -else if ($stat_var0 == 1) then -printf "$file result: bug is found\n" -printf "bug is found" >> $1.prot -if ($stat_var > 10) then -printf " : verification failed\n" >> $1.prot -else -printf "\n" >> $1.prot -endif -else if ($stat_var0 == 2) then -printf "$file result: fixed point is reached\n" -printf "property holds" >> $1.prot -if ($stat_var > 10) then -printf " : verification failed\n" >> $1.prot -else -printf "\n" >> $1.prot -endif -else if ($stat_var0 == 3) then -printf "not finished\n" >> $1.prot -printf "$file result: time exceeded\n" -else if ($stat_var0 == 4) then -printf "not finished\n" >> $1.prot -printf "$file result: memory exceeded\n" -else printf "not finished\n" >> $1.prot -endif -rrm -f $file.aig -rrm -f $file.sv -#r1em.bat $file -cd .. -end - - diff --git a/src/ebmc/r1esults_multi/exmps11 b/src/ebmc/r1esults_multi/exmps11 deleted file mode 100644 index 4b46b0eae..000000000 --- a/src/ebmc/r1esults_multi/exmps11 +++ /dev/null @@ -1,6 +0,0 @@ -mentorbm1 1 2 9 -sm98a7multi 3 -sm98tcas16multi 1 2 -sm98tcas16tmulti 2 4 6 -sm98tcasmulti 1 2 5 6 -sm98tcastmulti 2 4 5 6 diff --git a/src/ebmc/r1esults_multi/multi_prop.pl b/src/ebmc/r1esults_multi/multi_prop.pl deleted file mode 100755 index fb9c62710..000000000 --- a/src/ebmc/r1esults_multi/multi_prop.pl +++ /dev/null @@ -1,52 +0,0 @@ -#!/usr/bin/perl - -if ($#ARGV == -1) { - printf("multi_prop.pl exmps\n"); - exit(0); -} - - -qx(rm -f res.txt); -qx(rm -f *.prot); - -$exmp_path = "/home/eugene/e0xamples/hwmcc11/multi"; - -(my $fname) = @ARGV; - -$time_limit = 800; - -open EXMPS,"< $fname" or die "failed to open file $fname\n"; - -while () { - chomp($_); - $exmp = $_; - - @words = split / /,$exmp; - - # print "@words"; - - $name = $words[0]; - - printf "$name\n"; - - qx(cp $exmp_path/$name.aig .); - qx(ba2ver $name.aig $name.sv pa); - - - $i = 0; - foreach (@words) { - $i++; - if ($i == 1) {next;} - printf(" prop. $_\n"); - qx(sngl_call.bat $time_limit $name $_); - } - -# printf("%s\n",$num_prop); - - qx(rm -f $name.aig $name.sv $name.sv.cnstr); -} - -close EXMPS; - -$answer = qx(diff -s res.txt rpnt.txt); -printf "$answer"; diff --git a/src/ebmc/r1esults_multi/rpnt.txt b/src/ebmc/r1esults_multi/rpnt.txt deleted file mode 100644 index 4dabfe10d..000000000 --- a/src/ebmc/r1esults_multi/rpnt.txt +++ /dev/null @@ -1,17 +0,0 @@ -exmp mentorbm1 prop. 1 property HOLDS -exmp mentorbm1 prop. 2 property HOLDS -exmp mentorbm1 prop. 9 property HOLDS -exmp sm98a7multi prop. 3 property FAILED -exmp sm98tcas16multi prop. 1 property FAILED -exmp sm98tcas16multi prop. 2 property HOLDS -exmp sm98tcas16tmulti prop. 2 property HOLDS -exmp sm98tcas16tmulti prop. 4 property FAILED -exmp sm98tcas16tmulti prop. 6 property FAILED -exmp sm98tcasmulti prop. 1 property FAILED -exmp sm98tcasmulti prop. 2 property HOLDS -exmp sm98tcasmulti prop. 5 property FAILED -exmp sm98tcasmulti prop. 6 property FAILED -exmp sm98tcastmulti prop. 2 property HOLDS -exmp sm98tcastmulti prop. 4 property FAILED -exmp sm98tcastmulti prop. 5 property FAILED -exmp sm98tcastmulti prop. 6 property FAILED diff --git a/src/ebmc/r1esults_multi/sngl_call.bat b/src/ebmc/r1esults_multi/sngl_call.bat deleted file mode 100755 index 4524c11bd..000000000 --- a/src/ebmc/r1esults_multi/sngl_call.bat +++ /dev/null @@ -1,6 +0,0 @@ -#!/usr/bin/tcsh -limit cputime $1 -#printf "$1 $2 $3\n" > $2_p$3.prot -printf "exmp $2 prop. $3 " >> res.txt -../ebmc $2.sv --ic3 --constr --property $2.property.$3 > $2_p$3.prot -grep property $2_p$3.prot >> res.txt diff --git a/src/ebmc/r2esults_multi/exmps12 b/src/ebmc/r2esults_multi/exmps12 deleted file mode 100644 index 131935b78..000000000 --- a/src/ebmc/r2esults_multi/exmps12 +++ /dev/null @@ -1,4 +0,0 @@ -mentorbm1 4 -6s110 1015 1036 1037 1229 1528 1529 493 844 845 850 851 -6s135 17 101 -6s141 11 diff --git a/src/ebmc/r2esults_multi/multi_prop.pl b/src/ebmc/r2esults_multi/multi_prop.pl deleted file mode 100755 index 161f52467..000000000 --- a/src/ebmc/r2esults_multi/multi_prop.pl +++ /dev/null @@ -1,52 +0,0 @@ -#!/usr/bin/perl - -if ($#ARGV == -1) { - printf("multi_prop.pl exmps\n"); - exit(0); -} - - -qx(rm -f res.txt); -qx(rm -f *.prot *.prt); - -$exmp_path = "/home/eugene/e0xamples/hwmcc12/multi"; - -(my $fname) = @ARGV; - -$time_limit = 600; - -open EXMPS,"< $fname" or die "failed to open file $fname\n"; - -while () { - chomp($_); - $exmp = $_; - - @words = split / /,$exmp; - - # print "@words"; - - $name = $words[0]; - - printf "$name\n"; - - qx(cp $exmp_path/$name.aig .); - qx(ba2ver $name.aig $name.sv pa m); - - - $i = 0; - foreach (@words) { - $i++; - if ($i == 1) {next;} - printf(" prop. $_\n"); - qx(sngl_call.bat $time_limit $name $_); - } - -# printf("%s\n",$num_prop); - - qx(rm -f $name.aig $name.sv $name.sv.cnstr); -} - -close EXMPS; - -$answer = qx(diff -s res.txt rpnt.txt); -printf "$answer"; diff --git a/src/ebmc/r2esults_multi/rpnt.txt b/src/ebmc/r2esults_multi/rpnt.txt deleted file mode 100644 index f44bfe256..000000000 --- a/src/ebmc/r2esults_multi/rpnt.txt +++ /dev/null @@ -1,15 +0,0 @@ -exmp mentorbm1 prop. 4 no constr: property FAILED, with constr: property HOLDS -exmp 6s110 prop. 1015 no constr: property FAILED, with constr: property HOLDS -exmp 6s110 prop. 1036 no constr: property FAILED, with constr: property HOLDS -exmp 6s110 prop. 1037 no constr: property FAILED, with constr: property HOLDS -exmp 6s110 prop. 1229 no constr: property FAILED, with constr: property HOLDS -exmp 6s110 prop. 1528 no constr: property FAILED, with constr: property HOLDS -exmp 6s110 prop. 1529 no constr: property FAILED, with constr: property HOLDS -exmp 6s110 prop. 493 no constr: property FAILED, with constr: property HOLDS -exmp 6s110 prop. 844 no constr: property FAILED, with constr: property HOLDS -exmp 6s110 prop. 845 no constr: property FAILED, with constr: property HOLDS -exmp 6s110 prop. 850 no constr: property FAILED, with constr: property HOLDS -exmp 6s110 prop. 851 no constr: property FAILED, with constr: property HOLDS -exmp 6s135 prop. 17 no constr: property FAILED, with constr: property HOLDS -exmp 6s135 prop. 101 no constr: property FAILED, with constr: property HOLDS -exmp 6s141 prop. 11 no constr: property FAILED, with constr: property HOLDS diff --git a/src/ebmc/r2esults_multi/run_ic3.pl b/src/ebmc/r2esults_multi/run_ic3.pl deleted file mode 100755 index a9af4b1a1..000000000 --- a/src/ebmc/r2esults_multi/run_ic3.pl +++ /dev/null @@ -1,70 +0,0 @@ -#!/usr/bin/perl - -if ($#ARGV == -1) { - printf("run_ic3.pl exmps\n"); - exit(0); -} - - -qx(rm -f res.txt); -qx(rm -f *.prt); - -$exmp_path = "/home/eugene/e0xamples/hwmcc12/multi"; - -(my $fname) = @ARGV; - -$time_limit = 800; - -open EXMPS,"< $fname" or die "failed to open file $fname\n"; - -while () { - chomp($_); - $exmp = $_; - - @words = split / /,$exmp; - - # print "@words"; - - $name = $words[0]; - - printf "$name\n"; - - qx(cp $exmp_path/$name.aig .); - - - $i = 0; - foreach (@words) { - $i++; - if ($i == 1) {next;} - printf(" prop. $_\n"); - $ind = $_ - 1; - $prot_name = $name . _p . $_; - - - $pid = fork(); - die if not defined $pid; - if ($pid > 0) { -# printf "%d\n",$pid; - eval { - local $SIG{ALRM} = sub {kill 9, -$pid; die "alarm\n"}; - alarm 1000; - waitpid($pid, 0); - alarm 0; - }; - } - elsif ($pid == 0) { - setpgrp(0,0); - exec("iic3 < $name.aig -s $ind > $prot_name.prt"); - exit(0); - } - - } - -# printf("%s\n",$num_prop); - - qx(rm -f $name.aig); -} - -close EXMPS; - - diff --git a/src/ebmc/r2esults_multi/sngl_call.bat b/src/ebmc/r2esults_multi/sngl_call.bat deleted file mode 100755 index 858eff0bf..000000000 --- a/src/ebmc/r2esults_multi/sngl_call.bat +++ /dev/null @@ -1,12 +0,0 @@ -#!/usr/bin/tcsh -limit cputime $1 -#printf "$1 $2 $3\n" > $2_p$3.prot -printf "exmp $2 prop. $3 " >> res.txt - -#../ebmc $2.sv --ic3 --property main.property.$3 > $2_p$3.prot -../ebmc $2.sv --ic3 --property main.property.$3 --constr > $2_p$3.prt - -#printf "no constr: " >> res.txt -#grep property $2_p$3.prot | tr -d '\n' >> res.txt -printf ", with constr: " >> res.txt -grep property $2_p$3.prt >> res.txt diff --git a/src/ebmc/rregr_testing.bat b/src/ebmc/rregr_testing.bat deleted file mode 100755 index dbd6401bf..000000000 --- a/src/ebmc/rregr_testing.bat +++ /dev/null @@ -1,12 +0,0 @@ -# -rrm -f $1/*.prot -rrm -f $1/ *.prt -pproc_all.bat b1uggy.solved -pproc_all.bat corr.solved -pproc_all.bat u5nsolved -cd r0esults -diff -s b1uggy.solved.prot b1uggy.solved.rpnt -diff -s corr.solved.prot corr.solved.rpnt -diff -s u5nsolved.prot u5nsolved.rpnt -cd .. - diff --git a/src/ic3/README b/src/ic3/README index 26cb931fa..4ae33869f 100644 --- a/src/ic3/README +++ b/src/ic3/README @@ -2,12 +2,8 @@ a variation of Aaron Bradley's IC3. It is incorporated into ebmc. To invoke IC3, run - ebmc verilog_file --ic3 + ebmc verilog_file --ic3 [options] -*) Integration is not over yet. This current version is missing two - features that has been implemented in the stand-alone version. - The current version assumes that the input verilog file specifies - only one property and has no constraints. diff --git a/src/ic3/e2xclude_state.cc b/src/ic3/e2xclude_state.cc index ba1242c7f..ae2639a2a 100644 --- a/src/ic3/e2xclude_state.cc +++ b/src/ic3/e2xclude_state.cc @@ -152,7 +152,7 @@ void CompInfo::adjust_clause1(CLAUSE &C,CUBE &St) printf("%*c",9,' '); printf("expand_clause\n"); } - htable_lits.change_marker(); // increment or reset the hash table marker + htable_lits.change_marker(); htable_lits.started_using(); int marker = htable_lits.marker; diff --git a/src/ic3/l0ift_states.cc b/src/ic3/l0ift_states.cc index f3e2a374c..fafe53a1e 100644 --- a/src/ic3/l0ift_states.cc +++ b/src/ic3/l0ift_states.cc @@ -139,7 +139,8 @@ void CompInfo::gen_state_cube(CUBE &St_cube,CUBE &St,SatSolver &Slvr) A D D _ C L S _ E X C L _ S T _ C U B E ===========================================*/ -void CompInfo::add_cls_excl_st_cube(Mlit &act_lit,SatSolver &Slvr,CUBE &St,bool add_cnstr_lits) +void CompInfo::add_cls_excl_st_cube(Mlit &act_lit,SatSolver &Slvr,CUBE &St, + bool add_cnstr_lits) { CLAUSE C; act_lit = IctMinisat::mkLit(Slvr.Mst->newVar(),false); diff --git a/src/ic3/m4y_aiger_print.cc b/src/ic3/m4y_aiger_print.cc index 7e9e9a181..57ca654fe 100644 --- a/src/ic3/m4y_aiger_print.cc +++ b/src/ic3/m4y_aiger_print.cc @@ -1,29 +1,22 @@ -#include -#include -#include +/****************************************************** + +Module: Printing circuit in text version of aiger format + (Part 1) + +Author: Eugene Goldberg, eu.goldberg@gmail.com + +******************************************************/ #include #include #include -#include -#include -#include -#include -#include #include -#include -#include -#include -#include -#include -#include +#include #include #include "minisat/core/Solver.h" #include "minisat/simp/SimpSolver.h" - -using namespace std; #include "dnf_io.hh" #include "ccircuit.hh" #include "m0ic3.hh" @@ -39,9 +32,8 @@ void CompInfo::print_aiger_format() int num_consts; int num_buffs; check_circuit(num_buffs,num_consts); - // printf("num_buffs = %d\n",num_buffs); assert(num_consts <= 2); - string full_name; + std::string full_name; assert(strlen(out_file) > 0); full_name = out_file; full_name += ".aag"; diff --git a/src/ic3/m5y_aiger_print.cc b/src/ic3/m5y_aiger_print.cc index bef3621c4..1387f7cef 100644 --- a/src/ic3/m5y_aiger_print.cc +++ b/src/ic3/m5y_aiger_print.cc @@ -1,28 +1,22 @@ -#include -#include -#include +/****************************************************** + +Module: Printing circuit in text version of aiger format + (Part 2) + +Author: Eugene Goldberg, eu.goldberg@gmail.com + +******************************************************/ #include #include #include -#include -#include -#include -#include -#include #include -#include -#include -#include -#include -#include -#include +#include #include #include "minisat/core/Solver.h" #include "minisat/simp/SimpSolver.h" -using namespace std; #include "dnf_io.hh" #include "ccircuit.hh" #include "m0ic3.hh" diff --git a/src/ic3/p2ush_clauses_forward.cc b/src/ic3/p2ush_clauses_forward.cc index 428c7b8ae..84a0688a3 100644 --- a/src/ic3/p2ush_clauses_forward.cc +++ b/src/ic3/p2ush_clauses_forward.cc @@ -69,7 +69,7 @@ void CompInfo::push_clauses_forward(bool triv_time_frame) add_copies(i,C); continue;} } - else // C.size() == F[clause_ind.size() + else // C.size() == F[clause_ind].size() if (Clause_info[clause_ind].span < i) continue; diff --git a/src/ic3/s1tat.cc b/src/ic3/s1tat.cc index 963141de9..d73cc7c61 100644 --- a/src/ic3/s1tat.cc +++ b/src/ic3/s1tat.cc @@ -159,7 +159,8 @@ void CompInfo::print_time_frame_stat() if (verbose > 0) my_printf("F.size() = %m, num. inact. clauses = %m\n",(int) F.size(), num_inact_cls); - printf("num. seen (redund) cls = %d (%d)\n",Tf.num_seen_cls,Tf.num_redund_cls); + // printf("num. seen (redund) cls = %d (%d)\n",Tf.num_seen_cls, + // Tf.num_redund_cls); } /* end of function print_time_frame_stat*/ diff --git a/src/ic3/todo b/src/ic3/todo index 995e06035..3d414f4d8 100644 --- a/src/ic3/todo +++ b/src/ic3/todo @@ -3,8 +3,6 @@ Finishing integration with ebmc ===================== -*) Eliminate the bug in generating constrained formulas - *) Add code freeing memory allocated by the Verilog reader after IC3 converted this information into its internal data structure. (Keeping this memory is too expensive for large @@ -22,8 +20,6 @@ Changes of the current implementation to finish a time frame, average size of inductive clauses, averages size of cubes generalizing bad states etc) -*) Optimize the procedure of building the longest inductive clause for - the case of designs with a large number of latches *) Implement actual removal of subsumed clauses (currently they are just marked and ignored by the algorithm) @@ -33,18 +29,21 @@ Changes of the current implementation Improvements of the basic algorithm ==================================== -*) Write a perl script meant for efficiently checking multiple - properties. The idea is to check properties one by one re-using - information found when proving (or disproving) previous properties. +*) Implement a version of IC3 that combines property strengthening and + property relaxation. Combining strenthening and relation allows one + to "emulate" an algorithm that employs depth-first search. -*) Implement the version of IC3 that fixes the problem with - convergence rate (by computing reachability of good states breaking - induction) *) Implement a "dual" IC3 where one over-approximates the set of states from which a bad state is reachable in j transitions (rather than the set of states reachable in j transitions from initial states). -*) Implement a version of IC3 where one employs depth-first search +*) Implement the version of IC3 that fixes the problem with + convergence rate (by computing reachability of good states breaking + induction) + + + + diff --git a/src/ic3/ttodo b/src/ic3/ttodo deleted file mode 100644 index 210500342..000000000 --- a/src/ic3/ttodo +++ /dev/null @@ -1,69 +0,0 @@ -===================== - - T O D O - -===================== -*) polish the header part of 'm4y_aiger_print.cc - and 'm5y_aiger_print.cc' (take into account - Matthias' PR) - - -*) add code to the procedures affected by - the value of 'standard_mode' - - - +) set_short_param2("act_upd_mode",BRAD_ACT_UPD); - - - - - -*) add parameter --stat - -*) add perl script that checks all the properties in a straightforward way - -*) remove all the extra files I have added (scripts and so on) - - - -*) add code freeing memory allocated by the Verilog reader after IC3 - converted this information into its internal data - structure. (Keeping this memory is too expensive for large - examples.) - -================= - - D O N E - -================= -*) get rid of 'prop_ind' -*) modify 'find_prop' -*) replace '--prop' with '--property' -*) modify regression tests -*) eliminate the bug in generating constrained formulas -*) remove the performance bug caused by insufficient lifting - of CTG-states -*) add code to the procedures affected by - the value of 'standard_mode' -*) remove 'tf_ind' from 'exclude_state_cube' -*) add code updating the fields of an element - of priorty queue below - dist; - sort_mode; -*) add parameter --new_mode -*) add 'standard_mode' field - -*) update the way obligations are sorted - in the priority queue - +) set_long_param("comp_short",0); - +) set_long_param("sort_mode",1); - +) set_long_param("min_cls",0); - +) set_long_param("act_obl",0); - +) set_long_param("mult_tried",0); - +) set_long_param("brad_obl",1); - +) set_long_param("dyn_push",1); -*) modify pushing for trivial time frames -*) remove grl_heur flag and the related code -*) remove add_final_gates -*) add option to print out the circuit in - the aiger format \ No newline at end of file diff --git a/src/ic3/v0erify.cc b/src/ic3/v0erify.cc index db204f337..03f6947cb 100644 --- a/src/ic3/v0erify.cc +++ b/src/ic3/v0erify.cc @@ -32,7 +32,7 @@ bool CompInfo::ver_trans_inv() if (!ok) return(false); ok = ver_invar(H,Old_nums); if (!ok) return(false); - printf("verification is ok\n"); + printf("inductive invariant verification is ok\n"); return(true); } /* end of function ver_trans_inv */ @@ -91,7 +91,7 @@ bool CompInfo::ver_ind_clauses2(CNF &H,CUBE &Old_nums) add_negated_assumps1(Assmps,C); bool sat_form = check_sat2(Gen_sat,Assmps); if (sat_form) { - printf("verification failed\n"); + printf("inductive invariant verification failed\n"); printf("Inv & T does not imply F'[%d]\n",Old_nums[i]); printf("F[%d]-> ",Old_nums[i]); std::cout << H[i] << std::endl; @@ -139,7 +139,7 @@ bool CompInfo::ver_prop() bool sat_form = check_sat1(Gen_sat); if (sat_form) { - printf("verification failed\n"); + printf("inductive invariant verification failed\n"); printf("Ist does not imply Prop\n"); return(false); } @@ -202,7 +202,7 @@ bool CompInfo::ver_ind_clauses1(CNF &H) bool sat_form = check_sat2(Gen_sat,Assmps); if (sat_form) { - printf("verification failed\n"); + printf("inductive invariant verification failed\n"); printf("clause F[%zu] excludes an initial state: ", i); std::cout << H[i] << std::endl; return(false); diff --git a/src/ic3/v1erify.cc b/src/ic3/v1erify.cc index 19c72718c..64a8c31d0 100644 --- a/src/ic3/v1erify.cc +++ b/src/ic3/v1erify.cc @@ -78,7 +78,7 @@ bool CompInfo::ver_cex() if (!ok) return(false); FINISH: - printf("verification is ok\n"); + printf("cex verification is ok\n"); return(true); } /* end of function ver_cex */ @@ -99,7 +99,7 @@ bool CompInfo::check_bad_state(CUBE &St) add_assumps1(Assmps,St); bool sat_form = check_sat2(Gen_sat,Assmps); if (sat_form == false) { - printf("verification failed\n"); + printf("cex verification failed\n"); printf("last state of Cex is a good one\n"); std::cout << "St-> " << St << std::endl; printf("sat_form = %d\n",sat_form); @@ -150,7 +150,7 @@ bool CompInfo::check_init_state(CUBE &St) bool sat_form = check_sat2(Gen_sat,Assmps); if (sat_form == false) { - printf("verification failed\n"); + printf("cex verification failed\n"); printf("Cex starts with a non-initial state\n"); return(false); } From 13f171dadc1b9e83495539227422911d54cc535d Mon Sep 17 00:00:00 2001 From: eigold Date: Sat, 3 Jun 2017 17:25:53 -0400 Subject: [PATCH 14/16] 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 */ From 224d738db56d4877ae6452aa500a7d731eda5f6c Mon Sep 17 00:00:00 2001 From: eigold Date: Mon, 5 Jun 2017 09:17:13 -0400 Subject: [PATCH 15/16] made the required %d->%zu replacements --- src/ic3/ebmc_ic3_interface.hh | 1 + src/ic3/m1ain.cc | 4 +++- src/ic3/m4y_aiger_print.cc | 10 +++++----- src/ic3/r1ead_input.cc | 3 +++ src/ic3/r3ead_input.cc | 5 ----- src/ic3/r7ead_input.cc | 31 +++++++++++++++++++++++++++++++ 6 files changed, 43 insertions(+), 11 deletions(-) diff --git a/src/ic3/ebmc_ic3_interface.hh b/src/ic3/ebmc_ic3_interface.hh index 9fb97e8e0..ec48ef74a 100644 --- a/src/ic3/ebmc_ic3_interface.hh +++ b/src/ic3/ebmc_ic3_interface.hh @@ -43,6 +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 form_orig_names(); void form_neg_orig_name(CCUBE &Name,literalt &next_lit); bool form_orig_name(CCUBE &Name,literalt &lit,bool subtract = false); diff --git a/src/ic3/m1ain.cc b/src/ic3/m1ain.cc index d37334d08..1b6086748 100644 --- a/src/ic3/m1ain.cc +++ b/src/ic3/m1ain.cc @@ -79,8 +79,10 @@ int ic3_enginet::operator()() const1 = false; orig_names = false; - + // print_nodes(); + // print_var_map(); read_ebmc_input(); + //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/m4y_aiger_print.cc b/src/ic3/m4y_aiger_print.cc index 57ca654fe..be2b2f660 100644 --- a/src/ic3/m4y_aiger_print.cc +++ b/src/ic3/m4y_aiger_print.cc @@ -176,8 +176,8 @@ void CompInfo::print_aiger_header(FILE *fp,int max_var,int num_gates) fprintf(fp,"aag "); fprintf(fp,"%d ",max_var); - fprintf(fp,"%d ",N->ninputs); - fprintf(fp,"%d ",N->nlatches); + fprintf(fp,"%zu ",N->ninputs); + fprintf(fp,"%zu ",N->nlatches); fprintf(fp,"1 "); fprintf(fp,"%d",num_gates); if (Constr_gates.size() == 0) fprintf(fp,"\n"); @@ -220,9 +220,9 @@ void CompInfo::check_circuit(int &num_buffs,int &num_consts) cond |= (G.func_type == CONST); if (!cond) { p(); - printf("i = %d\n",i); - printf("N->Gate_list.size() = %d\n",(int) N->Gate_list.size()); - printf("G.ninputs = %d\n",G.ninputs); + printf("i = %zu\n",i); + printf("N->Gate_list.size() = %zu\n", N->Gate_list.size()); + printf("G.ninputs = %zu\n",G.ninputs); exit(100); } } diff --git a/src/ic3/r1ead_input.cc b/src/ic3/r1ead_input.cc index c604c29e0..39b2b9b02 100644 --- a/src/ic3/r1ead_input.cc +++ b/src/ic3/r1ead_input.cc @@ -58,6 +58,9 @@ void ic3_enginet::find_prop_lit() prop_l=instantiate_convert(aig_prop, netlist.var_map, Oper, ns, get_message_handler()); + // int var_num = prop_l.var_no(); + // printf("var_num = %d\n",var_num); + 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; diff --git a/src/ic3/r3ead_input.cc b/src/ic3/r3ead_input.cc index 47280a929..5d08150e8 100644 --- a/src/ic3/r3ead_input.cc +++ b/src/ic3/r3ead_input.cc @@ -205,11 +205,6 @@ void ic3_enginet::form_outp_buf(CDNF &Out_names) if (prop_l.is_constant() == 0) if (prop_l.sign()) olit--; - - - - - assert(Ci.Inps.find(olit) == Ci.Inps.end()); bool latch = false; diff --git a/src/ic3/r7ead_input.cc b/src/ic3/r7ead_input.cc index 706293268..e131d1263 100644 --- a/src/ic3/r7ead_input.cc +++ b/src/ic3/r7ead_input.cc @@ -23,6 +23,37 @@ 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() +{ + + + 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); + } + printf("\n"); + } + + +} /* end of function print_var_map */ /*========================================= A D D _ P S E U D O _ I N P S From 5ac8cc95b778ded0ea01d261128ae433e402b30e Mon Sep 17 00:00:00 2001 From: eigold Date: Wed, 7 Jun 2017 19:19:16 -0400 Subject: [PATCH 16/16] 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);