From e1cb500f44b37d46ba4828a57563ea04519abdb3 Mon Sep 17 00:00:00 2001 From: eigold Date: Mon, 29 May 2017 15:30:14 -0400 Subject: [PATCH] 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); }