From 6130e39b18b5f53902e4eab14f6d5cdde5219563 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 1 Nov 2010 01:35:04 -0700 Subject: initial commit of public abc --- scripts/abc.rc | 332 ++++++++ scripts/abc_common.py | 1855 +++++++++++++++++++++++++++++++++++++++++++ scripts/bmc2.sh | 15 + scripts/bmc3.sh | 15 + scripts/dprove.sh | 15 + scripts/getch.py | 37 + scripts/new_abc_commands.py | 183 +++++ scripts/reachx_cmd.py | 111 +++ scripts/redirect.py | 94 +++ scripts/super_prove.sh | 15 + 10 files changed, 2672 insertions(+) create mode 100644 scripts/abc.rc create mode 100644 scripts/abc_common.py create mode 100644 scripts/bmc2.sh create mode 100644 scripts/bmc3.sh create mode 100644 scripts/dprove.sh create mode 100644 scripts/getch.py create mode 100644 scripts/new_abc_commands.py create mode 100644 scripts/reachx_cmd.py create mode 100644 scripts/redirect.py create mode 100644 scripts/super_prove.sh (limited to 'scripts') diff --git a/scripts/abc.rc b/scripts/abc.rc new file mode 100644 index 00000000..b7144f4a --- /dev/null +++ b/scripts/abc.rc @@ -0,0 +1,332 @@ +python new_abc_commands.py +python reachx_cmd.py +#python C:\Research\ABC\AIG\Python\reachx_cmd.py + +# global parameters +set check # checks intermediate networks +#set checkfio # prints warnings when fanins/fanouts are duplicated +set checkread # checks new networks after reading from file +set backup # saves backup networks retrived by "undo" and "recall" +set savesteps 1 # sets the maximum number of backup networks to save +set progressbar # display the progress bar + +# program names for internal calls +set dotwin dot.exe +set dotunix dot +set gsviewwin gsview32.exe +set gsviewunix gv +set siswin sis.exe +set sisunix sis +set mvsiswin mvsis.exe +set mvsisunix mvsis +set capowin MetaPl-Capo10.1-Win32.exe +set capounix MetaPl-Capo10.1 +set gnuplotwin wgnuplot.exe +set gnuplotunix gnuplot + +# standard aliases +alias b balance +alias cl cleanup +alias clp collapse +alias esd ext_seq_dcs +alias f fraig +alias fs fraig_sweep +alias fsto fraig_store +alias fres fraig_restore +alias ft fraig_trust +alias lp lutpack +alias pd print_dsd +alias pex print_exdc -d +alias pf print_factor +alias pfan print_fanio +alias pl print_level +alias pio print_io +alias pk print_kmap +alias ps print_stats +alias psu print_supp +alias psy print_symm +alias pun print_unate +alias q quit +alias r read +alias ra read_aiger +alias r3 retime -M 3 +alias r1 dretime +alias r2 retime -M 2 +alias r4 retime -M 4 +alias r5 retime -M 5 +alias r6 retime -M 6 +alias ren renode +alias rh read_hie +alias rl read_blif +alias rb read_bench +alias ret retime +alias rp read_pla +alias rt read_truth +alias rv read_verilog +alias rvl read_verlib +alias rsup read_super mcnc5_old.super +alias rlib read_library +alias rlibc read_library cadence.genlib +alias rw rewrite +alias rwz rewrite -z +alias rf refactor +alias rfz refactor -z +alias re restructure +alias rez restructure -z +alias rs resub +alias rsz resub -z +alias sa set autoexec ps +alias ua set autoexec +alias scl scleanup +alias sif if -s +alias so source -x +alias st strash +alias sw sweep +alias ssw ssweep +alias tr0 trace_start +alias tr1 trace_check +alias trt "r c.blif; st; tr0; b; tr1" +alias u undo +alias w write +alias wa write_aiger +alias wb write_bench +alias wc write_cnf +alias wh write_hie +alias wl write_blif +alias wp write_pla +alias wv write_verilog + +# standard scripts +alias share "b; multi; fx; b" +alias resyn "b; rw; rwz; b; rwz; b" +alias resyn2 "b; rw; rf; b; rw; rwz; b; rfz; rwz; b" +alias resyn2a "b; rw; b; rw; rwz; b; rwz; b" +alias resyn3 "b; rs; rs -K 6; b; rsz; rsz -K 6; b; rsz -K 5; b" +alias compress "b -l; rw -l; rwz -l; b -l; rwz -l; b -l" + +alias compress2 "b -l; rw -l; rf -l; b -l; rw -l; rwz -l; b -l; rfz -l; rwz -l; b -l" +alias choice "fraig_store; resyn; fraig_store; resyn2; fraig_store; fraig_restore" +alias choice2 "fraig_store; balance; fraig_store; resyn; fraig_store; resyn2; fraig_store; resyn2; fraig_store; fraig_restore" +alias rwsat "st; rw -l; b -l; rw -l; rf -l" +alias rwsat2 "st; rw -l; b -l; rw -l; rf -l; fraig; rw -l; b -l; rw -l; rf -l" +alias shake "st; ps; sat -C 5000; rw -l; ps; sat -C 5000; b -l; rf -l; ps; sat -C 5000; rfz -l; ps; sat -C 5000; rwz -l; ps; sat -C 5000; rfz -l; ps; sat -C 5000" + +alias snap fraig_store +alias unsnap fraig_restore +alias sv "wl temp" +alias usv "rl temp" +alias pli print_latch +alias cy "cycle -F 1" +alias im imfs +alias fx1 "fx -N 1" +alias el4 "eliminate -N 4" +alias if6 "if -K 6" +alias fr fretime -g +alias icb "ic -M 2 -B 10 -s" +alias cs "care_set " + +# resubstitution scripts for the IWLS paper +alias src_rw "st; rw -l; rwz -l; rwz -l" +alias src_rs "st; rs -K 6 -N 2 -l; rs -K 9 -N 2 -l; rs -K 12 -N 2 -l" +alias src_rws "st; rw -l; rs -K 6 -N 2 -l; rwz -l; rs -K 9 -N 2 -l; rwz -l; rs -K 12 -N 2 -l" +alias resyn2rs "b; rs -K 6; rw; rs -K 6 -N 2; rf; rs -K 8; b; rs -K 8 -N 2; rw; rs -K 10; rwz; rs -K 10 -N 2; b; rs -K 12; rfz; rs -K 12 -N 2; rwz; b" +alias compress2rs "b -l; rs -K 6 -l; rw -l; rs -K 6 -N 2 -l; rf -l; rs -K 8 -l; b -l; rs -K 8 -N 2 -l; rw -l; rs -K 10 -l; rwz -l; rs -K 10 -N 2 -l; b -l; rs -K 12 -l; rfz -l; rs -K 12 -N 2 -l; rwz -l; b -l" +alias c2 "ua; compress2rs; sa" +alias ic "indcut -v" +alias lp "lutpack" +alias c "ua; compress; sa" +alias c1 "ua; compress;b -l; rs -K 6 -l; rw -l; rs -K 6 -N 2 -l; rf -l; rs -K 8 -l; b -l; sa" +alias dr dretime +alias ds dsec -v +alias dp dprove -v + + +# experimental implementation of don't-cares +alias resyn2rsdc "b; rs -K 6 -F 2; rw; rs -K 6 -N 2 -F 2; rf; rs -K 8 -F 2; b; rs -K 8 -N 2 -F 2; rw; rs -K 10 -F 2; rwz; rs -K 10 -N 2 -F 2; b; rs -K 12 -F 2; rfz; rs -K 12 -N 2 -F 2; rwz; b" +alias compress2rsdc "b -l; rs -K 6 -F 2 -l; rw -l; rs -K 6 -N 2 -F 2 -l; rf -l; rs -K 8 -F 2 -l; b -l; rs -K 8 -N 2 -F 2 -l; rw -l; rs -K 10 -F 2 -l; rwz -l; rs -K 10 -N 2 -F 2 -l; b -l; rs -K 12 -F 2 -l; rfz -l; rs -K 12 -N 2 -F 2 -l; rwz -l; b -l" + +# minimizing for FF literals +alias fflitmin "compress2rs; ren; sop; ps -f" + +# temporaries +#alias t "rvl th/lib.v; rvv th/t2.v" +#alias t "so c/pure_sat/test.c" +#alias t "r c/14/csat_998.bench; st; ps" +#alias t0 "r res.blif; aig; mfs" +#alias t "r res2.blif; aig; mfs" + +#alias tt "r a/quip_opt/nut_001_opt.blif" +#alias ttb "wh a/quip_opt/nut_001_opt.blif 1.blif" +#alias ttv "wh a/quip_opt/nut_001_opt.blif 1.v" + +#alias reach "st; ps; compress2; ps; qrel; ps; compress2; ps; qreach -v; ps" + +alias qs1 "qvar -I 96 -u; ps; qbf -P 96" +alias qs2 "qvar -I 96 -u; qvar -I 97 -u; ps; qbf -P 96" +alias qs3 "qvar -I 96 -u; qvar -I 97 -u; qvar -I 98 -u; ps; qbf -P 96" +alias qs4 "qvar -I 96 -u; qvar -I 97 -u; qvar -I 98 -u; qvar -I 99 -u; ps; qbf -P 96" +alias qs5 "qvar -I 96 -u; qvar -I 97 -u; qvar -I 98 -u; qvar -I 99 -u; qvar -I 100 -u; ps; qbf -P 96" +alias qs6 "qvar -I 96 -u; qvar -I 97 -u; qvar -I 98 -u; qvar -I 99 -u; qvar -I 100 -u; qvar -I 101 -u; ps; qbf -P 96" +alias qs7 "qvar -I 96 -u; qvar -I 97 -u; qvar -I 98 -u; qvar -I 99 -u; qvar -I 100 -u; qvar -I 101 -u; qvar -I 102 -u; ps; qbf -P 96" +alias qs8 "qvar -I 96 -u; qvar -I 97 -u; qvar -I 98 -u; qvar -I 99 -u; qvar -I 100 -u; qvar -I 101 -u; qvar -I 102 -u; qvar -I 103 -u; ps; qbf -P 96" +alias qs9 "qvar -I 96 -u; qvar -I 97 -u; qvar -I 98 -u; qvar -I 99 -u; qvar -I 100 -u; qvar -I 101 -u; qvar -I 102 -u; qvar -I 103 -u; qvar -I 104 -u; ps; qbf -P 96" +alias qsA "qvar -I 96 -u; qvar -I 97 -u; qvar -I 98 -u; qvar -I 99 -u; qvar -I 100 -u; qvar -I 101 -u; qvar -I 102 -u; qvar -I 103 -u; qvar -I 104 -u; qvar -I 105 -u; ps; qbf -P 96" + +alias chnew "st; haig_start; resyn2; haig_use" +alias chnewrs "st; haig_start; resyn2rs; haig_use" + +alias stdsd "r test/6in.blif; st; ps; u; bdd; dsd -g; st; ps" +alias trec "rec_start; r c.blif; st; rec_add; rec_use" +alias trec4 "rec_start -K 4; r i10.blif; st; rec_add; rec_use" +alias trec5 "rec_start -K 5; r i10.blif; st; rec_add; rec_use" +alias trec6 "rec_start -K 6; r i10.blif; st; rec_add; rec_use" +alias trec7 "rec_start -K 7; r i10.blif; st; rec_add; rec_use" +alias trec8 "rec_start -K 8; r i10.blif; st; rec_add; rec_use" +alias trec10 "rec_start -K 10; r i10.blif; st; rec_add; rec_use" +alias trec12 "rec_start -K 12; r i10.blif; st; rec_add; rec_use" + +#alias tsh "r i10_if.blif; st; ps; u; sw; st; ps; cec" +alias tst4 "r i10_if4.blif; st; ps; r x/rec4_.blif; st; rec_start; r i10_if4.blif; st -r; ps; cec" +alias tst4n "r i10_if4.blif; st; ps; r 5npn/all_functions.aig; st; rec_start; r i10_if4.blif; st -r; ps; cec" +alias tst6 "r i10_if6.blif; st; ps; r x/rec6_16_.blif; st; rec_start; r i10_if6.blif; st -r; ps; cec" + +alias sn short_names + +alias inth "int -rv -C 25000 -N 10000" +alias inthh "int -rv -C 75000 -N 100" +alias a "alias " + +alias indh "ind -v -F 50 -C 10000" +alias indhu "ind -vu -F 25 -C 10000" +#alias reachx "reach -v -B 2000000 -F 20000" +alias dc2rs "ua; compress2rs; ps" + +alias ffx "ps;orpos;qua_ffix" +alias bfx "ps;orpos;qua_bfix" +alias era "&get;&era -mv;&put" + +#simulations +alias simh "sim -m -F 500 -W 15" +alias simhh "sim -m -F 2500 -W 3" +alias simdeep "sim -m -F 50000 -W 1" +alias simwide "sim -m -F 500 -W 255" + +#BMC's: +alias bmc2h "bmc2 -v -C 25000 -G 250000 -F 100" +alias bmc2hh "bmc2 -v -C 75000 -G 750000 -F 100" + + +#SIMPLIFICATIONS +alias scr "&get; &scorr; &put" +alias lcr "&get; &lcorr; &put" + +alias trm "logic;trim;st;ps" + +alias smp "ua;ps;scl;ps;rw;dr;lcorr;rw;dr;ps;scorr;ps;fraig;ps;dc2;dr;scorr -F 2;ps;dc2rs;w temp.aig" +alias smp1 "ua;ps;scl;ps;rw;dr;lcorr;rw;dr;ps;scorr;ps;fraig;ps;dc2;dr;ps;dc2rs;w temp.aig" +alias smpf "ua;ps;scl;lcr;ps;rw;dr;ps;scr;ps;dc2;&get;&scorr -F 2;&put;dr;ps;dc2;ps;w temp.aig" + + +alias &smp "ua;&get;&ps;&scl;&ps;&dc2;&put;dr;&get;&lcorr;&dc2;&put;dr;&get;&ps;&scorr;&ps;&fraig;&ps;&dc2;&put;dr;&get;&scorr -F 2;&ps;&dc2;&put;w temp.aig" + +alias smplite '&get;&scl;&dc2;&put;dr;&get;&lcorr;&dc2;&put;dr;&get;&scorr;&dc2;&put;dr;&get;&dc2;&put;ps;w temp.aig' + +alias &smp1 "ua;&get;&ps;&scl;&ps;&dc2;&put;dr;&get;&lcorr;&dc2;&put;dr;&get;&ps;&scorr;&ps;&fraig;&ps;&dc2;&put;dr;&get;&ps;&dc2;&put;w temp.aig" + +alias &smpf "ua;ps;rw;&get;&ps;&scl;&ps;&put;dr;&get;&ps;&lcorr;&ps;&dc2;&ps;&scorr;&ps;&put;rw;ps;w temp.aig" + +#for each output separately +alias simpk "dprove -vrcbkmiu -B 10 -D 1000" +alias simpkh "simpk -D 5000" +alias simpkf "simpk -D 10" + + +#ABSTRACTIONS + +#reparameterization +alias rpm "ps;&get;&reparam;&put;ps" + +#register abstraction +alias absh "abs -se -D 200000 -R 2; short_names" +alias abshx "abs -se -D 1000000; short_names" +alias absr "abs -ser -G 2000; short_names" +alias absp "abs -sep -G 2000; short_names" +alias absh1 "abs -se -D 200000 -R 1; short_names" + +#ABSTRACTION allowing continuation of register abstraction +alias absgo "&get; &abs_start -C 10000 -R 2; &ps; &w 1.aig; &abs_derive;&put; w gabs.aig" +alias absgof "&get; &abs_start -C 1000 -R 2; &ps; &w 1.aig; &abs_derive;&put; w gabs.aig" +alias absgoh "&get; &abs_start -C 200000 -R 2; &ps; &w 1.aig; &abs_derive;&put;w gabs.aig" + +#continuation after a cex is found +alias absc "&r 1.aig; &ps; &abs_refine; &w 1.aig; &ps; &abs_derive; &ps;&put; w gabs.aig" + +#PBA - proof based abstraction. continuation with cex is done with absc. +alias pbago "&get; &pba_start -vd -C 25000 -F 10; &ps; &w 1.aig; &abs_derive; &put; w gabs.aig" + +#SPECULATION +#initial speculation where equivalences are gathered. + +alias spechisysf "ua; &get; &equiv -s -W 512 -F 2000; &semi -v -F 50; &ps; &speci -F 1000 -C 25000; &srm -s; r gsrm.aig; &ps; &w gore.aig" + +alias spechisysfx "ua; &get; &equiv -s -W 512 -F 2000; &semi -v -F 50; &ps; &speci -F 10000 -C 200000; &srm -s; r gsrm.aig; &ps; &w gore.aig" + +alias spechisysff "ua; &get; &equiv -s -W 512 -F 2000; &semi -v -F 50; &ps; &speci -F 10000 -C 5000; &srm -s; r gsrm.aig; &ps; &w gore.aig" + +alias spechisysfq "ua; &get; &equiv -s -W 512 -F 2000; &semi -v -F 50; &ps; &speci -F 10000 -C 10; &srm -s; r gsrm.aig; &ps; &w gore.aig" + + +# CONTINUATION OF SPECULATION + +#BMC based: +alias spec "&r gore.aig;&srm -s;r gsrm.aig; bmc2 -v -F 100 -C 10000 -G 100000; &resim -m; &w gore.aig; &ps " + +alias spech "&r gore.aig;&srm -s;r gsrm.aig;smp;ps; bmc2 -v -F 100 -C 25000 -G 250000; &resim -m; &w gore.aig; &ps " + +alias spechh "&r gore.aig;&srm ;r gsrm.aig;smp;simpkf;smp;bmc2 -v -F 100 -C 200000; &resim -m; &w gore.aig; &ps " + +alias specheavy "&r gore.aig;&srm -s;r gsrm.aig; smp;simpk;smp;bmc2 -v -F 5000 -C 200000 -F 100; &resim -m; &w gore.aig; &ps" + + +#BDD based: +alias specb "&r gore.aig;&srm ;r gsrm.aig;smp;ps; reach -ov -B 1000000 -F 200000; &resim -m; &w gore.aig; &ps " + +alias specbb "&r gore.aig;&srm ;r gsrm.aig;smp;simpk -D 100;smp;ps; reach -ov -B 1000000 -F 200000; &resim -m; &w gore.aig; &ps " + + +#Interpolation based: +alias specint "&r gore.aig;&srm ;r gsrm.aig;inth;&resim -m; &w gore.aig; &ps" + +alias speck "&r gore.aig;&srm ;r gsrm.aig;simpk;&resim -m; &w gore.aig; &ps " + +alias speckf "&r gore.aig;&srm ;r gsrm.aig;simpk -D 100;&resim -m; &w gore.aig; &ps " + +alias specpk "&r gore.aig;&srm ;r gsrm.aig;simpkf;smp;ps; simpk ; &resim -m; &w gore.aig; &ps " + +alias specpkh "&r gore.aig;&srm ;r gsrm.aig;simpkf;smp;ps; simpkh ; &resim -m; &w gore.aig; &ps " + +alias specp "&r gore.aig;&srm ;r gsrm.aig;ps; dprove -rmficbu -B 10 -D 10; &resim -m; &w gore.aig; &ps " + +alias spece "&r gore.aig; &srm ;r gsrm.aig; smp; ps; &w gore.aig; &get; &era -m; &r gore.aig; &resim -m; &w gore.aig; &ps" + +#simulation based: +alias specs "&r gore.aig; &srm ; r gsrm.aig; sim -m -F 500 -W 15; &resim -m; &w gore.aig; &ps " + +alias specsh "&r gore.aig; &srm ; r gsrm.aig; sim -m -F 3500 -W 3; &resim -m; &w gore.aig;&ps " + +alias speci "&r gore.aig;&srm ;r gsrm.aig;int -tk -C 2000;&resim -m; &w gore.aig; &ps" + + + +alias %sa "set autoexec %ps" +alias %scr "%get;%st;%scorr;%put;st" + +alias sc "fold;w tempc.aig;unfold -s" +alias uc "r tempc.aig;unfold -s" +alias smpc "scl;rw;ps;scorr -c;ps;fraig;ps;compress2rs;ps" + + + + + + diff --git a/scripts/abc_common.py b/scripts/abc_common.py new file mode 100644 index 00000000..891a918b --- /dev/null +++ b/scripts/abc_common.py @@ -0,0 +1,1855 @@ +from pyabc import * +import redirect +import sys +import os +import time +import math +global G_C,G_T,latches_before_abs,latches_before_pba,n_pos_before,x_factor + +""" +The functions that are currently available from module _abc are: + +int n_ands(); +int n_pis(); +int n_pos(); +int n_latches(); +int n_bmc_frames(); +int prob_status(); 1 = unsat, 0 = sat, -1 = unsolved + +int run_command(char* cmd); + +bool has_comb_model(); +bool has_seq_model(); +bool is_true_cex(); +bool is_valid_cex(); + return 1 if the number of PIs in the current network and in the current counter-example are equal +int n_cex_pis(); + return the number of PIs in the current counter-example +int n_cex_regs(); + return the number of flops in the current counter-example +int cex_po(); + returns the zero-based output PO number that is SAT by cex +int cex_frame(); + return the zero-based frame number where the outputs is SAT +The last four APIs return -1, if the counter-example is not defined. +""" + +#global variables + +stackno_gabs = stackno_gore = stackno_greg= 0 +STATUS_UNKNOWN = -1 +STATUS_SAT = 0 +STATUS_UNSAT = 1 +RESULT = ('SAT' , 'SAT', 'UNSAT', 'UNDECIDED but reduced', 'UNDECIDED, no reduction', 'UNDCIDED but reduced' ) +Sat_reg = 0 +Sat_true = 1 +Unsat = 2 +Undecided_reduction = 3 +Undecided_no_reduction = 4 +Error = 5 +Restart = 6 +xfi = x_factor = 1 #set this to higher for larger problems or if you want to try harder during abstraction +max_bmc = -1 +last_time = 0 + +# Function definitions: +# simple functions: ________________________________________________________________________ +# set_globals, abc, q, x, has_any_model, is_sat, is_unsat, push, pop + +# ALIASES +def p(): + return prove() + +def ps(): + print_circuit_stats() + +def n_real_inputs(): + """This gives the number of 'real' inputs. This is determined by trimming away inputs that + have no connection to the logic. This is done by the ABC alias 'trm', which changes the current + circuit. In some applications we do not want to change the circuit, but just to know how may inputs + would go away if we did this. So the current circuit is saved and then restored afterwards.""" + abc('w %s_savetempreal.aig; logic; trim; st'%f_name) + n = n_pis() + abc('r %s_savetempreal.aig'%f_name) + return n + +def long(t): + if t<20: + t = t + else: + t = 20+(t-20)/3 + return max(10,t) + +def rif(): + """Not used""" + global f_name + print 'Type in the name of the aig file to be read in' + s = raw_input() + if s[-5:] == '.blif': + f_name = s[:-5] + else: + f_name = s + s = s+'.blif' + run_command(s) + x('st;constr -i') + print_circuit_stats() + a = n_ands() + f = max(1,30000/a) + f = min (f,16) + x('scorr -c -F %d'%f) + x('fold') + print_circuit_stats() + x('w %s_c.aig'%f_name) + +def abc(cmd): + abc_redirect_all(cmd) + + +def abc_redirect( cmd, dst = redirect.null_file, src = sys.stdout ): + """This is our main way of calling an ABC function. Redirect, means that we suppress any output from ABC""" + with redirect.redirect( dst, src ): + return run_command( cmd ) + + +def abc_redirect_all( cmd ): + """This is our main way of calling an ABC function. Redirect, means that we suppress any output from ABC, including error printouts""" + with redirect.redirect( redirect.null_file, sys.stdout ): + with redirect.redirect( redirect.null_file, sys.stderr ): + return run_command( cmd ) + +def set_globals(): + """This sets global parameters that are used to limit the resources used by all the operations + bmc, interpolation BDDs, abstract etc. There is a global factor 'x_factor' that can + control all of the various resource limiting parameters""" + global G_C,G_T,x_factor + nl=n_latches() + na=n_ands() + np = n_pis() + #G_C = min(500000,(3*na+500*(nl+np))) + G_C = x_factor * min(100000,(3*na+500*(nl+np))) + #G_T = min(250,G_C/2000) + G_T = x_factor * min(75,G_C/2000) + G_T = max(1,G_T) + #print('Global values: BMC conflicts = %d, Max time = %d sec.'%(G_C,G_T)) + +def a(): + """this puts the system into direct abc input mode""" + print "Entering ABC direct-input mode. Type q to quit ABC-mode" + n = 0 + while True: + print ' abc %d> '%n, + n = n+1 + s = raw_input() + if s == "q": + break + run_command(s) + +def set_fname(name): + """ Another way to set an f_name, but currently this is not used""" + global f_name + s = name + if s[-4:] == '.aig': + f_name = s[:-4] + else: + f_name = s + s = s+'.aig' + #read in file + run_command(s) + #print_circuit_stats() + +def read_file_quiet(fname=None): + """This is the main program used for reading in a new circuit. The global file name is stored (f_name) + Sometimes we want to know the initial starting name. The file name can have the .aig extension left off + and it will assume that the .aig extension is implied. This should not be used for .blif files. + Any time we want to process a new circuit, we should use this since otherwise we would not have the + correct f_name.""" + global max_bmc, f_name, d_name, initial_f_name, x_factor, init_initial_f_name + x_factor = 1 + max_bmc = -1 + + if fname is None: + print 'Type in the name of the aig file to be read in' + s = raw_input() + else: + s = fname + + if s[-4:] == '.aig': + f_name = s[:-4] + else: + f_name = s + s = s+'.aig' + + run_command(s) + initial_f_name = f_name + init_initial_f_name = f_name + +def read_file(): + read_file_quiet() + print_circuit_stats() + +def rf(): + read_file() + +##def read_file(): +## """This is the main program used for reading in a new circuit. The global file name is stored (f_name) +## Sometimes we want to know the initial starting name. The file name can have the .aig extension left off +## and it will assume that the .aig extension is implied. This should not be used for .blif files. +## Any time we want to process a new circuit, we should use this since otherwise we would not have the +## correct f_name.""" +## global max_bmc, f_name, d_name, initial_f_name, x_factor +## x_factor = 1 +## max_bmc = -1 +## print 'Type in the name of the aig file to be read in' +## s = raw_input() +## if s[-4:] == '.aig': +## f_name = s[:-4] +## else: +## f_name = s +## s = s+'.aig' +## run_command(s) +## initial_f_name = f_name +## print_circuit_stats() +## +##def rf(): +## """just an alias for read_file""" +## read_file() + +def write_file(s): + """this is the main method for writing the current circuit to an AIG file on disk. + It manages the name of the file, by giving an extension (s). The file name 'f_name' + keeps increasing as more extensions are written. A typical sequence is + name, name_smp, name_smp_abs, name_smp_abs_spec, name_smp_abs_spec_final""" + global f_name + """Writes out the current file as an aig file using f_name appended with argument""" + f_name = '%s_%s'%(f_name,s) + ss = '%s.aig'%(f_name) + print 'WRITING %s: '%ss, + print_circuit_stats() + abc('w '+ss) + +def wf(): + """Not used""" + print 'input type of file to be written' + s = raw_input() + write_file(s) + +def bmc_depth(): + """ Finds the number of BMC frames that the latest operation has used. The operation could be BMC, reachability + interpolation, abstract, speculate. max_bmc is continually increased. It reflects the maximum depth of any version of the circuit + including abstract ones, for which it is known that there is not cex out to that depth.""" + global max_bmc + b = n_bmc_frames() + max_bmc = max(b,max_bmc) + return max_bmc + +def set_max_bmc(b): + """ Keeps increasing max_bmc which is the maximum number of time frames for + which the current circuit is known to be UNSAT for""" + global max_bmc + max_bmc = max(b,max_bmc) + +def print_circuit_stats(): + """Stardard way of outputting statistice about the current circuit""" + global max_bmc + i = n_pis() + o = n_pos() + l = n_latches() + a = n_ands() + b = max(max_bmc,bmc_depth()) + c = cex_frame() + if b>= 0: + if c>=0: + print 'PIs = %d, POs = %d, FF = %d, ANDs = %d, max depth = %d, CEX depth = %d'%(i,o,l,a,b,c) + else: + print 'PIs = %d, POs = %d, FF = %d, ANDs = %d, max depth = %d'%(i,o,l,a,b) + else: + if c>=0: + print 'PIs = %d, POs = %d, FF = %d, ANDs = %d, CEX depth = %d'%(i,o,l,a,c) + else: + print 'PIs = %d, POs = %d, FF = %d, ANDs = %d'%(i,o,l,a) + +def q(): + exit() + +def x(s): + """execute an ABC command""" + print "RUNNING: ", s + run_command(s) + +def has_any_model(): + """ check if a satisfying assignment has been found""" + res = has_comb_model() or has_seq_model() + return res + +def is_unsat(): + if prob_status() == 1: + return True + else: + return False + +def is_sat(): + if prob_status() == 0: + return True + else: + return False + +def wc(file): + """writes so that costraints are preserved explicitly""" + abc('&get;&w %s'%file) + +def rc(file): + """reads so that if constraints are explicit, it will preserve them""" + abc('&r %s;&put'%file) + +##def push(file): +## """ saves .aig in stack_x""" +## global stackno_gabs, stackno_gsrm, stackno_greg +## if 'gabs' in file: +## snm = 'gabs' +## elif 'gsrm' in file: +## snm = 'gsrm' +## elif 'x' in file: +## snm = 'greg' +## else: +## print 'wrong file name' +## return +## print snm +## sn = 'stackno_%s'%snm +## print sn +## exec 'sn += sn' +## print sn, eval(sn) +## run_command("r %s.aig"%file) +## run_command("w %s_%d.aig"%(file,eval(sn))) +## +##def pop(file): +## """ reads top .aig in stack_1 and saves it in .aig""" +## global stackno_gabs, stackno_gsrm, stackno_greg +## if 'gabs' in file: +## sn = 'gabs' +## if 'gsrm' in file: +## sn = 'gsrm' +## if 'x' in file: +## sn = 'greg' +## else: +## print 'wrong file name' +## return +## run_command("r %s_%d.aig"%(file,eval(sn))) +## run_command("w %s.aig"%file) +## os.remove("%s_%d.aig"%(file,eval(sn))) +## exec 'sn = sn-1' +## # need to protect against wrong stack count + +def fast_int(n): + """This is used to eliminate easy-to-prove outputs. Arg n is conflict limit to be used + in the interpolation routine. Typically n = 1 or 10""" + n_po = n_pos() + abc('int -k -C %d'%n) + print 'Reduced POs from %d to %d'%(n_po,n_pos()) + +def refine_with_cex(): + """Refines the greg (which contains the original problem with the set of FF's that have been abstracted). + This generates a new abstraction (gabs) and modifies the greg file to reflect which regs are in the + current abstraction""" + global f_name + print 'CEX in frame %d for output %d'%(cex_frame(),cex_po()) + abc('&r %s_greg.aig; &abs_refine; &w %s_greg.aig'%(f_name,f_name)) + return + +def generate_abs(n): + """generates an abstracted model (gabs) from the greg file. The gabs file is automatically + generated in the & space by &abs_derive. We store it away using the f_name of the problem + being solved at the moment. The f_name keeps changing with an extension given by the latest + operation done - e.g. smp, abs, spec, final, group. """ + global f_name + #we have a cex and we use this generate a new gabs file + abc('&r %s_greg.aig; &abs_derive; &put; w %s_gabs.aig'%(f_name,f_name)) # do we still need the gabs file + if n == 1: + print 'New abstraction: ', + print_circuit_stats() + return + + +#more complex functions: ________________________________________________________ +#, abstract, pba, speculate, final_verify, dprove3 + + +def simplify(): + """Our standard simplification of logic routine. What it does depende on the problem size. + For large problems, we use the &methods which use a simple circuit based SAT solver. Also problem + size dictates the level of k-step induction done in 'scorr' The stongest simplification is done if + n_ands < 20000. Then it used the clause based solver and k-step induction where |k| depends + on the problem size """ + # set_globals() +## print 'simplify initial ', +## ps() + abc('w t.aig') + n=n_ands() + abc('scl') + if n > 30000: + abc('&get;&scl;&put') + n = n_ands() + if n < 100000: + abc("&dc2;&put;dr;&get;&lcorr;&dc2;&put;dr;&get;&scorr;&fraig;&dc2;&put;dr") + run_command('ps') + print '.', + n = n_ands() + if n<45000: + abc("&get;&scorr -F 2;&put;dc2rs") + print '.', + #ps() + else: + abc("dc2rs") + print '.', + #ps() + n = n_ands() + n = n_ands() + if n <= 30000: + print '.', + #ps() + if n > 15000: + abc("dc2rs") + print '.', + else: + abc("scorr -F 2;dc2rs") + print '.', + #ps() + n = max(1,n_ands()) + ps() + if n < 20000: + m = int(min( 60000/n, 16)) + #print 'm = %d'%m + if m >= 4: + j = 4 + while j <= m: + set_size() + #print 'j - %d'%j + abc('scl;dr;dc2;scorr -C 5000 -F %d'%j) + if check_size() == 1: + break + j = 2*j + #ps() + continue + print '.', + + +def iterate_simulation(latches_before): + """Subroutine of 'abstract' which does the refinement of the abstracted model, + using counterexamples found by simulation. Simulation is controlled by the amount + of memory it might use. At first wide but shallow simulation is done, bollowed by + successively more narrow but deeper simulation""" + global x_factor, f_name +## print 'RUNNING simulation iteratively' + f = 5 + w = 255 + for k in range(9): + f = min(f *2, 3500) + w = max(((w+1)/2)-1,1) + print '.', + abc('sim -m -F %d -W %d'%(f,w)) + if not is_sat(): + continue + while True: + refine_with_cex() + if is_sat(): + print 'cex failed to refine abstraction ' + return Sat_true + generate_abs(0) + latches_after = n_latches() + print 'Latches increased to %d'%latches_after + if latches_after >= .99*latches_before: + abc('r %s_savetempabs.aig'%f_name) + print "No reduction!." + return Undecided_no_reduction + abc('sim -m -F %d -W %d'%(f,w)) + if not is_sat(): + break + +def iterate_abstraction_refinement(latches_before,NBF): + """Subroutine of 'abstract' which does the refinement of the abstracted model, + using counterexamples found by BMC or BDD reachability""" + global x_factor, f_name + if NBF == -1: + F = 2000 + else: + F = 2*NBF + print '\nIterating BMC or BDD reachability' + reach_sw = 0 + always_reach = 0 + cexf = 0 + reach_failed = 0 + while True: + #print 'Generating problem abstraction' + generate_abs(1) + set_globals() + latches_after = n_latches() + if latches_after >= .98*latches_before: +## print 'No reduction' +## abc('r &s_savetemp.aig'%f_name) + break + ri = n_real_inputs() # No. of inputs after trm + nlri = n_latches()+ri + #reach_allowed = ((nlri<150) or (((cexf>250))&(nlri<300))) + reach_allowed = ((nlri<75) or (((cexf>250))&(nlri<300))) + t = max(1,G_T) + if not F == -1: + F = int(1.5*max_bmc) + if (((reach_allowed or (reach_sw ==1)) and not reach_failed)): + #cmd = 'reach -B 200000 -F 3500 -T %f'%t + #cmd = 'reachx -e %d -t %d'%(int(long(t)),max(10,int(t))) + cmd = 'reachx -t %d'%max(10,int(t)) + reach_sw = 1 + else: + reach_sw = 0 + cmd = 'bmc3 -C %d -T %f -F %d'%(G_C,t,F) + print 'RUNNING %s'%cmd + abc(cmd) + if prob_status() == 1: + print 'Reachability went to %d frames, '%n_bmc_frames() + print 'UNSAT' + return Unsat + cexf = cex_frame() + set_max_bmc(cexf -1) + if ((not is_sat()) and (reach_sw == 1)): + reach_failed = 1 # if ever reach failed, then we should not try it again on more refined models + if is_sat(): + set_max_bmc(cex_frame()-1) + refine_with_cex() # if cex can't refine, status is set to Sat_true + if is_sat(): + print 'cex did not refine. Implies true_sat' + return Sat_true + else: + print "No CEX found in %d frames"%n_bmc_frames() + if reach_sw == 0: + break + else: + continue + latches_after = n_latches() + if latches_after >= .98*latches_before: + abc('r %s_savetempabs.aig'%f_name) + print "No reduction!" + return Undecided_no_reduction + else: + print 'Latches reduced from %d to %d'%(latches_before, n_latches()) + return Undecided_reduction + + +def abstract(): + """ abstracts using N Een's method 3 - cex/proof based abstraction. The result is further refined using + simulation, BMC or BDD reachability""" + global G_C, G_T, latches_before_abs, x_factor + set_globals() + latches_before_abs = n_latches() + abc('w %s_savetempabs.aig'%f_name) + print 'Start: ', + print_circuit_stats() + c = 1.5*G_C + #c = 20000 + t = max(1,1.25*G_T) + method = 3 + if n_ands() > 100000: + method = 0 + s = min(max(3,c/30000),10) # stability between 3 and 10 + if max_bmc == -1: + time = max(1,.01*G_T) + abc('bmc3 -C %d -T %f -F 165'%(.01*G_C, time)) + set_max_bmc(bmc_depth()) + f = min(250,1.5*max_bmc) + f = max(20, f) + f = 10*f + if not method == 0: + b = 10 + b = max(b,max_bmc+2) + b = b*2**(x_factor-1) + b = 2*b + print 'Neen abstraction params: Bob = %d, Method #%d, %d conflicts, %d stable, %d sec., %d frames'%(b,method,c/3,s,t,f) + abc('&get; &abs_newstart -v -B %f -A %d -C %d -S %d -V %f -F %d'%(b,method,c/3,s,t,f)) + else: + abc('&get;&abs_start -v -C 500000 -R 1') + #abc('w abstemp.aig') + if is_sat(): + print 'Found true counterexample in frame %d'%cex_frame() + return Sat_true + NBF = bmc_depth() + print 'Abstraction good to %d frames'%n_bmc_frames() + set_max_bmc(NBF) + abc('&w %s_greg.aig; &abs_derive; &put; w %s_gabs.aig'%(f_name,f_name)) + print 'First abstraction: ', + print_circuit_stats() + latches_after = n_latches() + #if latches_before_abs == latches_after: + if latches_after >= .98*latches_before_abs: + abc('r %s_savetempabs.aig'%f_name) + print "No reduction!" + return Undecided_no_reduction + # refinement loop + if (n_ands() + n_latches() + n_pis()) < 15000: + print 'Running simulation iteratively' + for i in range(5): + result = iterate_simulation(latches_before_abs) + if result == Restart: + return result + if result == Sat_true: + return result + result = iterate_abstraction_refinement(latches_before_abs, NBF) + #if the result is 'Restart' we return and the calling routine increase + #x_factor to try one more time. + return result + +def absv(n,v): + """This is a version of 'abstract' which can control the methods used in Een's abstraction code (method = n) + as well as whether we want to view the output of this (v = 1)""" + global G_C, G_T, latches_before_abs, x_factor + #input_x_factor() + #x_factor = 3 + set_globals() + latches_before_abs = n_latches() + print 'Start: ', + print_circuit_stats() + c = 1.5*G_C + t = max(1,1.25*G_T) + s = min(max(3,c/30000),10) # stability between 3 and 10 + if max_bmc == -1: + time = max(1,.01*G_T) + abc('bmc3 -C %d -T %f -F 165'%(.01*G_C, time)) + set_max_bmc(bmc_depth()) + f = min(250,1.5*max_bmc) + f = max(20, f) + f = 10*f + b = x_factor*20 + if not n == 0: + b = 10 + b = max(b,max_bmc+2) + b = b*2**(x_factor-1) + b = 2*b + print 'Neen abstraction params: Method #%d, %d conflicts, %d stable, %f sec.'%(n,c/3,s,t) + if v == 1: + run_command('&get; &abs_newstart -v -B %f -A %d -C %d -S %d -V %f'%(b,n,c/3,s,t)) + else: + abc('&get; &abs_newstart -v -B %f -A %d -C %d -S %d -T %f'%(b,n,c/3,s,t)) + set_max_bmc(n_bmc_frames()) + print 'Abstraction good to %d'%n_bmc_frames() + abc('&w %s_greg.aig; &abs_derive; &put; w %s_gabs.aig'%(f_name,f_name)) + print 'Final abstraction: ', + print_circuit_stats() + latches_after = n_latches() + if latches_after >= .98*latches_before_abs: + print "No reduction!" + return Undecided_no_reduction + return Undecided_reduction + +def spec(): + """Main speculative reduction routine. Finds candidate sequential equivalences and refines them by simulation, BMC, or reachability + using any cex found. """ + input_x_factor() + global G_C,G_T,n_pos_before, x_factor, n_latches_before + set_globals() + n_pos_before = n_pos() + n_latches_before = n_latches() + set_globals() + t = max(1,.5*G_T) + r = max(1,int(t)) + print 'Running &equiv2 with C = %d, T = %f sec., F = %d -S 1 -R %d'%(G_C,t,200,r) + abc("&get; &equiv2 -C %d -F 200 -T %f -S 1 -R %d; &semi -F 50; &speci -F 20 -C 1000;&srm; r gsrm.aig; w %s_gsrm.aig; &w %s_gore.aig"%((G_C),t,r,f_name,f_name)) + print 'Initial speculation: ', + print_circuit_stats() + print 'Speculation good to %d frames'%n_bmc_frames() + return + +def speculate(): + """Main speculative reduction routine. Finds candidate sequential equivalences and refines them by simulation, BMC, or reachability + using any cex found. """ + + global G_C,G_T,n_pos_before, x_factor, n_latches_before + set_globals() + n_pos_before = n_pos() + + def refine_with_cex(): + """Refines the gore file to reflect equivalences that go away because of cex""" + global f_name + print 'CEX in frame %d for output %d'%(cex_frame(),cex_po()) + abc('&r %s_gore.aig; &resim -m; &w %s_gore.aig'%(f_name,f_name)) + #abc('&r %s_gore.aig; &equiv2 -vx ; &w %s_gore.aig'%(f_name,f_name)) + return + + def generate_srm(n): + """generates a speculated reduced model (srm) from the gore file""" + global f_name + pos = n_pos() + ab = n_ands() + abc('&r %s_gore.aig; &srm ; r gsrm.aig; w %s_gsrm.aig'%(f_name,f_name)) #do we still need to write the gsrm file + if n == 0: + if ((pos == n_pos()) and (ab == n_ands())): + print 'Failed to refine' + return 'failed' + if n == 1: + print 'Spec. Red. Miter: ', + print_circuit_stats() + return 'OK' + + def run_simulation(n): + f = 5 + w = (256/n)-1 + for k in range(9): + f = min(f * 2, 3500) + w = max(((w+1)/2)-1,1) + print '.', + #generate_srm(0) + abc('sim -m -F %d -W %d'%(f,w)) + if not is_sat(): + continue + if cex_po() < n_pos_before: + print 'Sim found true cex: Output = %d, Frame = %d'%(cex_po(),cex_frame()) + return Sat_true + refine_with_cex() + if n_pos_before == n_pos(): + return Undecided_no_reduction + while True: + result = generate_srm(0) + if result == 'failed': + return Sat_true + abc('sim -m -F %d -W %d'%(f,w)) + if not is_sat(): + break + if cex_po() < n_pos_before: + print 'Sim found true cex: Output = %d, Frame = %d'%(cex_po(),cex_frame()) + return Sat_true + refine_with_cex() + if n_pos_before == n_pos(): + return Undecided_no_reduction + return Undecided_no_reduction + + n_pos_before = n_pos() + n_latches_before = n_latches() + set_globals() + t = max(1,.5*G_T) + r = max(1,int(t)) + print 'Running &equiv2 with C = %d, T = %f sec., F = %d -S 1 -R %d'%(G_C,t,200,r) + abc("&get; &equiv2 -C %d -F 200 -T %f -S 1 -R %d; &semi -F 50; &speci -F 20 -C 1000;&srm; r gsrm.aig; w %s_gsrm.aig; &w %s_gore.aig"%((G_C),t,r,f_name,f_name)) + print 'Initial speculation: ', + print_circuit_stats() + print 'Speculation good to %d frames'%n_bmc_frames() + #simplify() + if n_pos_before == n_pos(): + print 'No new outputs. Quitting speculate' + return Undecided_no_reduction # return result is unknown + if is_sat(): + #print '\nWARNING: if an abstraction was done, need to refine it further\n' + return Sat_true + k = n_ands() + n_latches() + n_pis() + n = 0 + if k < 15000: + n = 1 + elif k < 30000: + n = 2 + elif k < 60000: + n = 4 + elif k < 120000: + n = 8 + if n > 0: # simulation can run out of memory for too large designs, so be careful + print 'RUNNING simulation iteratively' + for i in range(5): + result = run_simulation(n) + if result == Sat_true: + return result + simp_sw = 1 + int_sw = 1 + reach_sw = 0 + cexf = 0 + reach_failed = 0 + init = 1 + print '\nIterating BMC or BDD reachability' + while True: # now try real hard to get the last cex. + set_globals() + if not init: + set_size() + result = generate_srm(1) + if check_size() == True: + print 'Failed to refine' + return Error + if result == 'failed': + return Sat_true + if simp_sw == 1: + na = n_ands() + simplify() + if n_ands() > .7*na: #if not significant reduction, stop simplification + simp_sw = 0 + if n_latches() == 0: + return check_sat() + init = 0 # make it so that next time it is not the first time through + time = max(1,G_T/(5*n_pos())) + if int_sw ==1: + npo = n_pos() + if n_pos() > .5*npo: # if not sufficient reduction, turn this off + int_sw = 0 + if is_sat(): #if fast interpolation found a cex + cexf = cex_frame() + set_max_bmc(cexf - 1) + if cex_po() < n_pos_before: + print 'Int found true cex: Output = %d, Frame = %d'%(cex_po(),cex_frame()) + return Sat_true + refine_with_cex() + if n_pos_before == n_pos(): + return Undecided_no_reduction + if is_sat(): + print '1. cex failed to refine abstraction' + return Sat_true + continue + else: + if n_latches() == 0: + return check_sat() + ri = n_real_inputs() #seeing how many inputs would trm get rid of + nlri = n_latches() + ri + reach_allowed = ((nlri<75) or (((cexf>250)) and (nlri<300))) + if (((reach_allowed or (reach_sw == 1)) and not reach_failed)): + t = max(1,1.2*G_T) + f = max(3500, 2*max_bmc) + cmd = 'reachx -t %d'%max(10,int(t)) + reach_sw = 1 + else: + t = max(1,1.5*G_T) + if max_bmc == -1: + f = 200 + else: + f = max_bmc + f = int(1.5*f) + cmd = 'bmc3 -C %d -T %f -F %f'%(1.5*G_C,1.2*t,f) + reach_sw = 0 + print 'Running %s'%cmd + abc(cmd) + if is_sat(): + cexf = cex_frame() + set_max_bmc(cexf - 1) + #This is a temporary fix since reachx always reports cex_ps = 0 + if ((cex_po() < n_pos_before) and (cmd[:3] == 'bmc')): + print 'BMC found true cex: Output = %d, Frame = %d'%(cex_po(),cex_frame()) + return Sat_true + #End of temporary fix + refine_with_cex()#change the number of equivalences + if n_pos_before == n_pos(): + return Undecided_no_reduction + continue + else: + set_max_bmc(bmc_depth()) + print 'No cex found in %d frames'%n_bmc_frames() + if reach_sw == 0: + break + else: + if prob_status() == 1: + print 'Reachability converged in %d frames'%n_bmc_frames() + return Unsat + reach_failed = 1 + init = 1 + continue + if n_pos_before == n_pos(): + return Undecided_no_reduction + else: + return Undecided_reduction + +def set_size(): + """Stores the problem size of the current design. Size is defined as (PIs, POs, ANDS, FF, max_bmc)""" + global npi, npo, nands, nff, nmd + npi = n_pis() + npo = n_pos() + nands = n_ands() + nff = n_latches() + nmd = max_bmc + +def check_size(): + """Assumes the problem size has been set by set_size before some operation. This checks if the size was changed + Size is defined as (PIs, POs, ANDS, FF, max_bmc) + Returns TRUE is size is the same""" + global npi, npo, nands, nff, nmd + result = ((npi == n_pis()) and (npo == n_pos()) and (nands == n_ands()) and (nff == n_latches()) and (nmd == max_bmc)) +## if result == 1: +## print 'Size unchanged' + return result + +def inferior_size(): + """Assumes the problem size has been set by set_size beore some operation. + This checks if the new size is inferior (larger) to the old one + Size is defined as (PIs, POs, ANDS, FF)""" + global npi, npo, nands, nff + result = ((npi < n_pis()) or (npo < n_pos()) or (nands < n_ands()) ) + return result + +def quick_verify(n): + """Low resource version of final_verify n = 1 means to do an initial simplification first""" + abc('trm') + if n == 1: + simplify() + if n_latches == 0: + return check_sat() + abc('trm') + print 'After trimming: ', + print_circuit_stats() + #try_rpm() + set_globals() + if is_sat(): + return Sat_true + c = max(G_C/10, 1000) + t = max(1,.4*G_T) + print 'RUNNING interpolation with %d conflicts, max %d sec and 100 frames'%(c,t) + abc('int -v -F 100 -C %d -T %f'%(c,t)) + status = get_status() + if status <= Unsat: + print 'Interpolation went to %d frames, '%n_bmc_frames(), + print RESULT[status] + return status + N = bmc_depth() + L = n_latches() + I = n_real_inputs() + if ( ((I+L<200)&(N>100)) or (I+L<125) or L < 51 ): #heuristic that if bmc went deep, then reachability might also + t = max(1,.4*G_T) + cmd = 'reachx -t %d'%max(10,int(t)) + print 'Running %s'%cmd + abc(cmd) + status = get_status() + if status <= Unsat: + print 'Reachability went to %d frames, '%n_bmc_frames() + print RESULT[status] + return status + print 'BDD reachability aborted' + simplify() #why is this here + if n_latches() == 0: + print 'Simplified to 0 FF' + return check_sat() + set_max_bmc(bmc_depth()) # doesn't do anything + print 'No success, max_depth = %d'%max_bmc + return Undecided_reduction + +def get_status(): + """this simply translates the problem status encoding done by ABC (-1,0,1)=(undecided,SAT,UNSAT) into the status code used by our python code.""" + status = prob_status() #interrogates ABC for the current status of the problem. + # 0 = SAT + if status == 1: + status = Unsat + if status == -1: #undecided + status = Undecided_no_reduction + return status + +def try_rpm(): + """rpm is a cheap way of doing reparameterization and is an abstraction method, so may introduce false cex's. + It finds a minimum cut between the PIs and the main sequential logic and replaces this cut by free inputs. + A quick BMC is then done, and if no cex is found, we assume the abstraction is valid. Otherwise we revert back + to the original problem before rpm was tried.""" + global x_factor + if n_ands() > 30000: + return + set_globals() + pis_before = n_pis() + abc('w %s_savetemp.aig'%f_name) + abc('rpm') + result = 0 + if n_pis() < .5*pis_before: + bmc_before = bmc_depth() + #print 'running quick bmc to see if rpm is OK' + t = max(1,.1*G_T) + abc('bmc3 -C %d, -T %f'%(.1*G_C, t)) + if is_sat(): #rpm made it sat by bmc test, so undo rpm + abc('r %s_savetemp.aig'%f_name) + else: + abc('trm') + print 'WARNING: rpm reduced PIs to %d. May make SAT.'%n_pis() + result = 1 + else: + abc('r %s_savetemp.aig'%f_name) + return result + +def final_verify(): + """This is the final method for verifying anything is nothing else has worked. It first tries BDD reachability + if the problem is small enough. If this aborts or if the problem is too large, then interpolation is called.""" + global x_factor + set_globals() +## simplify() +## if n_latches() == 0: +## return check_sat() +## abc('trm') + #rpm_result = try_rpm() + set_globals() + N = bmc_depth() + L = n_latches() + I = n_real_inputs() + #try_induction(G_C) + if ( ((I+L<250)&(N>100)) or (I+L<200) or (L<51) ): #heuristic that if bmc went deep, then reachability might also + t = max(1,1.5*G_T) + #cmd = 'reach -v -B 1000000 -F 10000 -T %f'%t + #cmd = 'reachx -e %d'%int(long(t)) + #cmd = 'reachx -e %d -t %d'%(int(long(t)),max(10,int(t))) + cmd = 'reachx -t %d'%max(10,int(t)) + print 'Running %s'%cmd + abc(cmd) + status = get_status() + if status <= Unsat: + print 'Reachability went to %d frames, '%n_bmc_frames(), + print RESULT[status] + return status + print 'BDD reachability aborted' + #f = max(100,bmc_depth()) + c = max(G_C/5, 1000) + t = max(1,G_T) + print '\nRUNNING interpolation with %d conflicts, %d sec, max 100 frames'%(c,t) + abc('int -v -F 100 -C %d -T %f'%(c,t)) + status = get_status() + if status <= Unsat: + print 'Interpolation went to %d frames, '%n_bmc_frames(), + print RESULT[status] + return status + simplify() + if n_latches() == 0: + return check_sat() + print 'Undecided' + return Undecided_reduction + +def check_sat(): + """This is called if all the FF have disappeared, but there is still some logic left. In this case, + the remaining logic may be UNSAT, which is usually the case, but this has to be proved. The ABC command 'dsat' is used fro combinational problems""" +## if n_ands() == 0: +## return Unsat + abc('dsat -C %d'%G_C) + if is_sat(): + return Sat_true + elif is_unsat(): + return Unsat + else: + return Undecided_no_reduction + +def try_era(s): + """era is explicit state enumeration that ABC has. It only works if the number of PIs is small, + but there are cases where it works and nothing else does""" + if n_pis() > 12: + return + cmd = '&get;&era -mv -S %d;&put'%s + print 'Running %s'%cmd + run_command(cmd) + +def try_induction(C): + """Sometimes proving the property directly using induction works but not very often. + For 'ind' to work, it must have only 1 output, so all outputs are or'ed together temporarily""" + return Undecided_reduction + print '\nTrying induction' + abc('w %s_temp.aig'%f_name) + abc('orpos; ind -uv -C %d -F 10'%C) + abc('r %s_savetemp.aig'%f_name) + status = prob_status() + if not status == 1: + return Undecided_reduction + print 'Induction succeeded' + return Unsat + +def final_verify_recur(K): + """During prove we make backups as we go. These backups have increasing abstractions done, which can cause + non-verification by allowing false counterexamples. If an abstraction fails with a cex, we can back up to + the previous design before the last abstraction and try to proceed from there. K is the backup number we + start with and this decreases as the backups fails. For each backup, we just try final_verify. + If ever we back up to 0, which is the backup just after simplify, we then try speculate on this. This often works + well if the problem is a SEC problem where there are a lot of equivalences across the two designs.""" + for j in range(K): + i = K-(j+1) + if i == 0: #don't try final verify on original + status = 3 + break + print '\nVerifying backup number %d:'%i, + abc('r %s_backup_%d.aig'%(initial_f_name,i)) + print_circuit_stats() + status = final_verify() + if status >= Unsat: + return status + if i > 0: + print 'SAT returned, trying less abstract backup' + continue + break + if ((i == 0) and (status > Unsat) and (n_ands() > 0)): + print '\nTrying speculate on initial backup number %d:'%i, + abc('r %s_backup_%d.aig'%(initial_f_name,i)) + ps() + if n_ands() < 20000: + status = speculate() + if ((status <= Unsat) or (status == Error)): + return status + status = final_verify() + if status == Unsat: + return status + else: + return Undecided_reduction + + +def pre_simp(): + """This uses a set of simplification algorithms which preprocesses a design. + Includes forward retiming, quick simp, signal correspondence with constraints, trimming away + PIs, and strong simplify""" + set_globals() + #print 'trying forward' + try_forward() + #print 'trying quick simp' + quick_simp() + #print 'trying_scorr_constr' + status = try_scorr_constr() + #status = 3 + #print 'trying trm' + if ((n_ands() > 0) or (n_latches()>0)): + abc('trm') + print 'Forward, quick_simp, scorr_constr,: ', + print_circuit_stats() + status = process_status(status) + if status <= Unsat: + return status + simplify() + print 'Simplify: ', + print_circuit_stats() + if n_latches() == 0: + return check_sat() + try_phase() + if n_latches() == 0: + return check_sat() + #abc('trm') + if ((n_ands() > 0) or (n_latches()>0)): + abc('trm') + status = process_status(status) + if status <= Unsat: + return status + status = try_scorr_constr() + abc('trm') + return process_status(status) + +def try_scorr_constr(): + set_size() + abc('w %s_savetemp.aig'%f_name) + status = scorr_constr() + if inferior_size(): + abc('r %s_savetemp.aig'%f_name) + return status + +def process(status): + """Checks if there are no FF and if so checks if the remaining combinational + problem is UNSAT""" + if n_latches() == 0: + return check_sat() + return status + +def try_phase(): + """Tries phase abstraction. ABC returns the maximum clock phase it found using n_phases. + Then unnrolling is tried up to that phase and the unrolled model is quickly + simplified (with retiming to see if there is a significant reduction. + If not, then revert back to original""" + n = n_phases() + if ((n == 1) or (n_ands() > 30000)): + return + print 'Number of possible phases = %d'%n + abc('w %s_savetemp.aig'%f_name) + na = n_ands() + nl = n_latches() + ni = n_pis() + no = n_pos() + cost_init = (1*n_pis())+(2*n_latches())+.05*n_ands() + cost_min = cost_init + cost = cost_init + abc('w %s_best.aig'%f_name) + for j in range(4): + abc('r %s_savetemp.aig'%f_name) + p = 2**(j+1) + if p > n: + break + abc('phase -F %d'%p) + if na == n_ands(): + break + abc('scl;rw') + if n_latches() > nl: #why would this ever happen + break + #print_circuit_stats() + abc('rw;lcorr;trm') + #print_circuit_stats() + cost = (1*n_pis())+(2*n_latches())+.05*n_ands() + if cost < cost_min: + cost_min = cost + abc('w %s_best.aig'%f_name) + else: + break + if cost < cost_init: + abc('r %s_best.aig'%f_name) + simplify() + abc('trm') + print 'Phase abstraction obtained :', + print_circuit_stats() + return + abc('r %s_savetemp.aig'%f_name) + return + +def try_forward(): + """Attempts most forward retiming, and latch correspondence there. If attempt fails to help simplify, then we revert back to the original design + This can be effective for equivalence checking problems where synthesis used retiming""" + abc('w %s_savetemp.aig'%f_name) + if n_ands() < 30000: + abc('dr') + abc('lcorr') + nl = n_latches() + na = n_ands() + abc('w %s_savetemp0.aig'%f_name) + abc('r %s_savetemp.aig'%f_name) + abc('dr -m') + abc('lcorr') + abc('dr') + if ((n_latches() <= nl) and (n_ands() < na)): + print 'Forward retiming reduced size to: ', + print_circuit_stats() + return + else: + abc('r %s_savetemp0.aig'%f_name) + return + return + +def quick_simp(): + """A few quick ways to simplify a problem before more expensive methods are applied. + Uses & commands if problem is large. These commands use the new circuit based SAT solver""" + na = n_ands() + if na < 30000: + abc('scl;rw') + elif na < 80000: + abc('&get;&scl;&put;rw') + +def scorr_constr(): + #return Undecided_no_reduction #temporarily disable the for the moment + """Extracts implicit constraints and uses them in signal correspondence + Constraints that are found are folded back when done""" + na = max(1,n_ands()) + if ((na > 40000) or n_pos()>1): + return Undecided_no_reduction + f = 40000/na + f = min(f,16) + n_pos_before = n_pos() + f = 1 #temporary until bug fixed. + abc('w %s_savetemp.aig'%f_name) + if n_ands() < 3000: + cmd = 'unfold -a -F 2' + else: + cmd = 'unfold' + abc(cmd) + if ((n_ands() > na) or (n_pos() == 1)): + abc('r %s_savetemp.aig'%f_name) + return Undecided_no_reduction + print_circuit_stats() + print 'Number of constraints = %d'%(n_pos() - n_pos_before) + abc('scorr -c -F %dd'%f) + if n_pos_before == 1: + #abc('cone -s -O 0') #don't fold constraints back in + abc('fold') + else: + abc('fold') +## abc('fold') + return Undecided_no_reduction + +def process_status(status): + """ if there are no FF, the problem is combinational and we still have to check if UNSAT""" + if n_latches() == 0: + return check_sat() + return status + +def input_x_factor(): + """Sets the global x_factor according to user input""" + global x_factor, xfi + print 'Type in x_factor:', + xfi = x_factor = input() + print 'x_factor set to %f'%x_factor + +def prove(a): + """Proves all the outputs together. If ever an abstraction was done then if SAT is returned, + we make RESULT return "undecided". + if a = 0 we skip the first quick_verify""" + global x_factor,xfi,f_name + x = time.clock() + max_bmc = -1 + K = 0 + print 'Initial: ', + print_circuit_stats() + x_factor = xfi + print 'x_factor = %f'%x_factor + print '\nRunning pre_simp' + set_globals() + status = pre_simp() + if status <= Unsat: + print 'Time for proof = %f sec.'%(time.clock() - x) + return RESULT[status] + if n_ands() == 0: + abc('bmc3 -T 2') + if is_sat(): + return 'SAT' + abc('trm') + write_file('smp') + abc('w %s_backup_%d.aig'%(initial_f_name,K)) + K = K +1 + set_globals() + if ((n_ands() < 30000) and (a == 1) and (n_latches() < 300)): + print '\nRunning quick_verify' + status = quick_verify(0) + if status <= Unsat: + if not status == Unsat: + print 'CEX in frame %d'%cex_frame() + print 'Time for proof = %f sec.'%(time.clock() - x) + return RESULT[status] + if n_ands() == 0: + abc('bmc3 -T 2') + if is_sat(): + return 'SAT' + print'\nRunning abstract' + nl_b = n_latches() + status = abstract() + abc('trm') + write_file('abs') + status = process_status(status) + if ((status <= Unsat) or status == Error): + if status < Unsat: + print 'CEX in frame %d'%cex_frame() +## status = final_verify_recur(K) +## write_file('final') + print 'Time for proof = %f sec.'%(time.clock() - x) + return RESULT[status] + print 'Time for proof = %f sec.'%(time.clock() - x) + return RESULT[status] + abc('w %s_backup_%d.aig'%(initial_f_name,K)) + K = K +1 + if status == Undecided_reduction: + print '\nRunning quick_verify' + status = quick_verify(1) + status = process_status(status) + if status <= Unsat: + if status < Unsat: + print 'CEX in frame %d'%cex_frame() + #print 'Time for proof = %f sec.'%(time.clock() - x) + status = final_verify_recur(K-1) + abc('trm') + write_file('final') + print 'Time for proof = %f sec.'%(time.clock() - x) + return RESULT[status] + if n_ands() > 20000: + print 'Speculation skipped because too large' + K = 2 + elif n_ands() == 0: + print 'Speculation skipped because no and nodes' + K = 2 + else: + print '\nRunning speculate' + status = speculate() + abc('trm') + write_file('spec') + status = process_status(status) + if status == Unsat: + print 'Time for proof = %f sec.'%(time.clock() - x) + return RESULT[status] + if ((status < Unsat) or (status == Error)): + print 'CEX in frame %d'%cex_frame() + K = K-1 #if spec found a true cex, then result of abstract was wrong + else: + abc('w %s_backup_%d.aig'%(initial_f_name,K)) + K = K +1 + status = final_verify_recur(K) + abc('trm') + write_file('final') + print 'Time for proof = %f sec.'%(time.clock() - x) + return RESULT[status] + +def prove_g_pos(a): + """Proves the outputs clustered by a parameter a. + a is the disallowed increase in latch support Clusters must be contiguous + If a = 0 then outputs are proved individually. Clustering is done from last to first + Output 0 is attempted to be proved inductively using other outputs as constraints. + Proved outputs are removed if all the outputs have not been proved. + If ever one of the proofs returns SAT, we stop and do not try any other outputs.""" + global f_name, max_bmc,x_factor + x = time.clock() + #input_x_factor() + init_f_name = f_name + #fast_int(1) + print 'Beginning prove_g_pos' + result = prove_all_ind() + print 'Number of outputs reduced to %d by induction and fast interpolation'%n_pos() + print '\n************Trying second level prove****************\n' + try_rpm() + result = prove(0) + #result = prove_0_ind() + if result == 'UNSAT': + print 'Second prove returned UNSAT' + return result + if result == 'SAT': + print 'CEX found' + return result + print '\n********** Proving each output separately ************' + result = prove_all_ind() + print 'Number of outputs reduced to %d by induction and fast interpolation'%n_pos() + f_name = init_f_name + abc('w %s_osavetemp.aig'%f_name) + n = n_pos() + print 'Number of outputs = %d'%n + #count = 0 + pos_proved = [] + J = 0 + jnext = n-1 + while jnext >= 0: + max_bmc = -1 + f_name = init_f_name + abc('r %s_osavetemp.aig'%f_name) + #Do in reverse order + jnext_old = jnext + if a == 0: # do not group + extract(jnext,jnext) + jnext = jnext -1 + else: + jnext = group(a,jnext) + if jnext_old > jnext+1: + print '\nProving outputs [%d-%d]'%(jnext + 1,jnext_old) + else: + print '\nProving output %d'%(jnext_old) + #ps() + #fast_int(1) + f_name = f_name + '_%d'%jnext_old + result = prove_1() + if result == 'UNSAT': + if jnext_old > jnext+1: + print '\n******** PROVED OUTPUTS [%d-%d] ******** \n\n'%(jnext+1,jnext_old) + else: + print '\n******** PROVED OUTPUT %d ******** \n\n'%(jnext_old) + pos_proved = pos_proved + range(jnext +1,jnext_old+1) + continue + if result == 'SAT': + print 'One of output in (%d to %d) is SAT'%(jnext + 1,jnext_old) + return result + else: + print '\n******** UNDECIDED on OUTPUTS %d thru %d ******** \n\n'%(jnext+1,jnext_old) + f_name = init_f_name + abc('r %s_osavetemp.aig'%f_name) + if not len(pos_proved) == n: + print 'Eliminating %d proved outputs'%(len(pos_proved)) + remove(pos_proved) + abc('trm') + write_file('group') + result = 'UNDECIDED' + else: + print 'Proved all outputs. The problem is proved UNSAT' + result = 'UNSAT' + print 'Total time for prove_g_pos = %f sec.'%(time.clock() - x) + return result + +def prove_pos(): + """Proves the outputs clustered by a parameter a. + a is the disallowed increase in latch support Clusters must be contiguous + If a = 0 then outputs are proved individually. Clustering is done from last to first + Output 0 is attempted to be proved inductively using other outputs as constraints. + Proved outputs are removed if all the outputs have not been proved. + If ever one of the proofs returns SAT, we stop and do not try any other outputs.""" + global f_name, max_bmc,x_factor + a=0 + x = time.clock() + #input_x_factor() + init_f_name = f_name + #fast_int(1) + print 'Beginning prove_g_pos' + result = prove_all_ind() + print 'Number of outputs reduced to %d by induction and fast interpolation'%n_pos() + print '\n********** Proving each output separately ************' + f_name = init_f_name + abc('w %s_osavetemp.aig'%f_name) + n = n_pos() + print 'Number of outputs = %d'%n + #count = 0 + pos_proved = [] + J = 0 + jnext = n-1 + while jnext >= 0: + max_bmc = -1 + f_name = init_f_name + abc('r %s_osavetemp.aig'%f_name) + #Do in reverse order + jnext_old = jnext + if a == 0: # do not group + extract(jnext,jnext) + jnext = jnext -1 + else: + jnext = group(a,jnext) + if jnext_old > jnext+1: + print '\nProving outputs [%d-%d]'%(jnext + 1,jnext_old) + else: + print '\nProving output %d'%(jnext_old) + #ps() + #fast_int(1) + f_name = f_name + '_%d'%jnext_old + result = prove_1() + if result == 'UNSAT': + if jnext_old > jnext+1: + print '\n******** PROVED OUTPUTS [%d-%d] ******** \n\n'%(jnext+1,jnext_old) + else: + print '\n******** PROVED OUTPUT %d ******** \n\n'%(jnext_old) + pos_proved = pos_proved + range(jnext +1,jnext_old+1) + continue + if result == 'SAT': + print 'One of output in (%d to %d) is SAT'%(jnext + 1,jnext_old) + return result + else: + print '\n******** UNDECIDED on OUTPUTS %d thru %d ******** \n\n'%(jnext+1,jnext_old) + f_name = init_f_name + abc('r %s_osavetemp.aig'%f_name) + if not len(pos_proved) == n: + print 'Eliminating %d proved outputs'%(len(pos_proved)) + remove(pos_proved) + abc('trm') + write_file('group') + result = 'UNDECIDED' + else: + print 'Proved all outputs. The problem is proved UNSAT' + result = 'UNSAT' + print 'Total time for prove_g_pos = %f sec.'%(time.clock() - x) + return result + + +def prove_g_pos_split(): + """like prove_g_pos but quits when any output is undecided""" + global f_name, max_bmc,x_factor + x = time.clock() + #input_x_factor() + init_f_name = f_name + #fast_int(1) + print 'Beginning prove_g_pos_split' + result = prove_all_ind() + print 'Number of outputs reduced to %d by induction and fast interpolation'%n_pos() + try_rpm() + print '\n********** Proving each output separately ************' + f_name = init_f_name + abc('w %s_osavetemp.aig'%f_name) + n = n_pos() + print 'Number of outputs = %d'%n + pos_proved = [] + J = 0 + jnext = n-1 + while jnext >= 0: + max_bmc = -1 + f_name = init_f_name + abc('r %s_osavetemp.aig'%f_name) + jnext_old = jnext + extract(jnext,jnext) + jnext = jnext -1 + print '\nProving output %d'%(jnext_old) + f_name = f_name + '_%d'%jnext_old + result = prove_1() + if result == 'UNSAT': + if jnext_old > jnext+1: + print '\n******** PROVED OUTPUTS [%d-%d] ******** \n\n'%(jnext+1,jnext_old) + else: + print '\n******** PROVED OUTPUT %d ******** \n\n'%(jnext_old) + pos_proved = pos_proved + range(jnext +1,jnext_old+1) + continue + if result == 'SAT': + print 'One of output in (%d to %d) is SAT'%(jnext + 1,jnext_old) + return result + else: + print '\n******** UNDECIDED on OUTPUTS %d thru %d ******** \n\n'%(jnext+1,jnext_old) + print 'Eliminating %d proved outputs'%(len(pos_proved)) + # remove outputs proved and return + f_name = init_f_name + abc('r %s_osavetemp.aig'%f_name) + remove(pos_proved) + abc('trm') + write_file('group') + return 'UNDECIDED' + f_name = init_f_name + abc('r %s_osavetemp.aig'%f_name) + if not len(pos_proved) == n: + print 'Eliminating %d proved outputs'%(len(pos_proved)) + remove(pos_proved) + abc('trm') + write_file('group') + result = 'UNDECIDED' + else: + print 'Proved all outputs. The problem is proved UNSAT' + result = 'UNSAT' + print 'Total time = %f sec.'%(time.clock() - x) + return result + + + +def group(a,n): + """Groups together outputs beginning at output n and any contiguous preceeding output + that does not increase the latch support by a or more""" + global f_name, max_bmc + nlt = n_latches() + extract(n,n) + nli = n_latches() + if n == 0: + return n-1 + for J in range(1,n+1): + abc('r %s_osavetemp.aig'%f_name) + j = n-J + #print 'trying %d to %d'%(j,n) + extract(j,n) + #print 'n_latches = %d'%n_latches() + #if n_latches() >= nli + (nlt - nli)/2: + if n_latches() == nli: + continue + if n_latches() > nli+a: + break + abc('r %s_osavetemp.aig'%f_name) +## if j == 1: +## j = j-1 + print 'extracting [%d-%d]'%(j,n) + extract(j,n) + ps() + return j-1 + +def extract(n1,n2): + """Extracts outputs n1 through n2""" + no = n_pos() + if n2 > no: + return 'range exceeds number of POs' + abc('cone -s -O %d -R %d'%(n1, 1+n2-n1)) + abc('scl') + +def prove_0_ind(): + """Uses all other outputs as constraints to try to prove output 0 by induction""" + abc('w %s_osavetemp.aig'%f_name) + #ps() + abc('constr -N %d'%(n_pos()-1)) + #ps() + abc('fold') + #ps() + abc('ind -u -C 1000000 -F 20') + status = get_status() + abc('r %s_osavetemp.aig'%f_name) + return status + +def remove(list): + """Removes outputs in list as well as easy output proved by fast interpolation""" + zero(list) + abc('scl') + fast_int(1) + +def zero(list): + """Zeros out POs in list""" + for j in list: + run_command('zeropo -N %d'%j) + +def sp(): + """Alias for super_prove""" + print 'Executing super_prove' + result = super_prove() + return result + +def super_prove(): + """Main proof technique now. Does original prove and if after speculation there are multiple output left + if will try to prove each output separately, in reverse order. It will quit at the first output that fails + to be proved, or any output that is proved SAT""" + global max_bmc, init_initial_f_name, initial_f_name + init_initial_f_name = initial_f_name + if x_factor > 1: + print 'x_factor = %d'%x_factor + input_x_factor() + max_bmc = -1 + x = time.clock() + result = prove(0) + k = 1 + print result + if not result[:3] == 'UND': + print 'Total time taken by super_prove = %f sec.'%(time.clock() - x) + return result + if n_pos() > 1: + result = prove_g_pos(0) + print result + if result == 'UNSAT': + print 'Total time taken by super_prove = %f sec.'%(time.clock() - x) + return result + if result == 'SAT': + k = 0 #Don't try to prove UNSAT on an abstraction that had SAT + # should go back to backup 1 since probably spec was bad. + y = time.clock() + result = BMC_VER_result(k) + print 'Total time taken by last gasp verification = %f sec.'%(time.clock() - y) + print 'Total time for %s = %f sec.'%(init_initial_f_name,(time.clock() - x)) + return result + +def reachm(t): + run_command('&get;&reach -vcs -T %d;&put'%t) + + +def BMC_VER_result(n): + global init_initial_f_name + #print init_initial_f_name + if n == 0: + print '\nTrying proof on initial simplified and abstracted circuit\n' + abc('r %s_smp.abs.aig'%init_initial_f_name) + ps() + x = time.clock() + result = 5 + N = 0 + T = 150 + if (n_pis()+n_latches() < 250): + print ' Trying deep Reachability' + run_command('reachx -t 150') + #run_command('&get;&reach -vcs -T %d'%T) + result = get_status() + if result == Unsat: + return 'UNSAT' + if ((result < Unsat) and (n == 0)): + N = 1 + if ((result >= Unsat) and (N == 0)): + print 'Trying deep interpolation' + run_command('int -v -F 30000 -C 1000000 -T %d'%T) + result = get_status() + if result == Unsat: + return 'UNSAT' +## try_split() +## if n_pos() > 1: +## result = prove_g_pos_split() +## if result[:5] == 'UNSAT': +## return result + #ps() + abc('r %s_smp.aig'%init_initial_f_name) + ps() + if N == 1: + print '\nTrying deep interpolation on initial simplified circuit\n' + run_command('int -v -F 30000 -C 1000000 -T %d'%T) + result = get_status() + if result == Unsat: + return 'UNSAT' + if result < Unsat: + return 'SAT' + print '\nTrying deep BMC on initial simplified circuit\n' + run_command('bmc3 -v -T %d -F 200000 -C 1000000'%T) + result = get_status() + if result < Unsat: + result = 'SAT' + print ' CEX found in frame %d'%cex_frame() + else: + result = 'UNDECIDED' + print 'Additional time taken by BMC/ability = %f sec.'%(time.clock() - x) + return result + +def try_split(): + abc('w %s_savetemp.aig'%f_name) + na = n_ands() + split(3) + if n_ands()> 2*na: + abc('r %s_savetemp.aig'%f_name) + + +def time_diff(): + global last_time + new_time = time.clock() + diff = new_time - last_time + last_time = new_time + result = 'Lapsed time = %.2f sec.'%diff + return result + +def prove_all_ind(): + """Tries to prove output k by induction, using outputs > k as constraints. Removes proved outputs from POs.""" + abc('w %s_osavetemp.aig'%f_name) + plist = [] + for j in range(n_pos()): + abc('r %s_osavetemp.aig'%f_name) + extract(j,n_pos()) + abc('constr -N %d'%(n_pos()-1)) + abc('fold') + n = max(1,n_ands()) + f = max(1,min(40000/n,16)) + f = int(f) + abc('ind -u -C 10000 -F %d'%f) + status = get_status() + if status == Unsat: + plist = plist + [j] + print '%d'%j, + print '\nOutputs proved inductively = ', + print plist + abc('r %s_osavetemp.aig'%f_name) + remove(plist) #remove the outputs proved + return status + +def split(n): + abc('orpos;&get') + abc('&posplit -v -N %d;&put;dc2;trm'%n) + +def keep_splitting(): + for j in range(5): + split(5+j) + no = n_pos() + status = prove_g_pos_split(0) + if status <= Unsat: + return status + if no == n_pos(): + return Undecided + +def drill(n): + run_command('&get; &reach -vcs -H 5 -S %d -T 50 -C 40'%n) + +def prove_1(): + """Proves all the outputs together. If ever an abstraction was done then if SAT is returned, + we make RESULT return "undecided". + """ + a = 1 + global x_factor,xfi,f_name + x = time.clock() + max_bmc = -1 + K = 0 + print 'Initial: ', + print_circuit_stats() + x_factor = xfi + print 'x_factor = %f'%x_factor + print '\nRunning pre_simp' + set_globals() + status = pre_simp() + if status <= Unsat: + print 'Time for proof = %f sec.'%(time.clock() - x) + return RESULT[status] + abc('trm') + write_file('smp') + abc('w %s_backup_%d.aig'%(initial_f_name,K)) + K = K +1 + set_globals() + if ((n_ands() < 30000) and (a == 1) and (n_latches() < 300)): + print '\nRunning quick_verify' + status = quick_verify(0) + if status <= Unsat: + if not status == Unsat: + print 'CEX in frame %d'%cex_frame() + print 'Time for proof = %f sec.'%(time.clock() - x) + return RESULT[status] + print'\nRunning abstract' + nl_b = n_latches() + status = abstract() + abc('trm') + write_file('abs') + status = process_status(status) + if ((status <= Unsat) or status == Error): + if status < Unsat: + print 'CEX in frame %d'%cex_frame() + print 'Time for proof = %f sec.'%(time.clock() - x) + return RESULT[status] + print 'Time for proof = %f sec.'%(time.clock() - x) + return RESULT[status] + abc('w %s_backup_%d.aig'%(initial_f_name,K)) + status = final_verify_recur(2) + abc('trm') + write_file('final') + print 'Time for proof = %f sec.'%(time.clock() - x) + return RESULT[status] + +def qprove(): + global x_factor + x = time.clock() + x_factor = 3 + print '\n*********pre_simp**********\n' + pre_simp() + print '\n*********absv**********\n' + result = absv(3,1) + x_factor = 2 + print '\n*********absv**********\n' + result = absv(3,1) + print '\n*********speculate**********\n' + result = speculate() + if result <= Unsat: + return RESULT[result] + print '\n*********absv**********\n' + result = absv(3,1) + print '\n*********prove_pos**********\n' + result = prove_pos() + if result == 'UNDECIDED': + print '\n*********BMC_VER_result**********\n' + result = BMC_VER_result(1) + print 'Time for proof = %f sec.'%(time.clock() - x) + return result + + + diff --git a/scripts/bmc2.sh b/scripts/bmc2.sh new file mode 100644 index 00000000..3e9d9566 --- /dev/null +++ b/scripts/bmc2.sh @@ -0,0 +1,15 @@ +#!/bin/sh + +abc_root() +{ + cwd="$(pwd)" + cd $(dirname "$1") + echo $(dirname "$(pwd)") + cd "${cwd}" +} + +abc_dir=$(abc_root "$0") +bin_dir="${abc_dir}"/bin +aig_file="$1" + +exec ${bin_dir}/abc -c "/rf ${aig_file} ; /pushredirect ; /pushdtemp ; bmc2 ; /popdtemp ; /popredirect ; /print_aiger_result" diff --git a/scripts/bmc3.sh b/scripts/bmc3.sh new file mode 100644 index 00000000..bba01e20 --- /dev/null +++ b/scripts/bmc3.sh @@ -0,0 +1,15 @@ +#!/bin/sh + +abc_root() +{ + cwd="$(pwd)" + cd $(dirname "$1") + echo $(dirname "$(pwd)") + cd "${cwd}" +} + +abc_dir=$(abc_root "$0") +bin_dir="${abc_dir}"/bin +aig_file="$1" + +exec "${bin_dir}"/abc -c "/rf ${aig_file} ; /pushredirect ; /pushdtemp ; bmc3 ; /popdtemp ; /popredirect ; /print_aiger_result" diff --git a/scripts/dprove.sh b/scripts/dprove.sh new file mode 100644 index 00000000..4289aad3 --- /dev/null +++ b/scripts/dprove.sh @@ -0,0 +1,15 @@ +#!/bin/sh + +abc_root() +{ + cwd="$(pwd)" + cd $(dirname "$1") + echo $(dirname "$(pwd)") + cd "${cwd}" +} + +abc_dir=$(abc_root "$0") +bin_dir="${abc_dir}"/bin +aig_file="$1" + +exec ${bin_dir}/abc -c "/rf ${aig_file} ; /pushredirect ; /pushdtemp ; dprove ; /popdtemp ; /popredirect ; /print_aiger_result" diff --git a/scripts/getch.py b/scripts/getch.py new file mode 100644 index 00000000..89e13078 --- /dev/null +++ b/scripts/getch.py @@ -0,0 +1,37 @@ + +class _Getch: + """Gets a single character from standard input. Does not echo to the screen.""" + def __init__(self): + try: + self.impl = _GetchWindows() + except ImportError: + self.impl = _GetchUnix() + + def __call__(self): return self.impl() + + +class _GetchUnix: + def __init__(self): + import tty, sys + + def __call__(self): + import sys, tty, termios + fd = sys.stdin.fileno() + old_settings = termios.tcgetattr(fd) + try: + tty.setraw(sys.stdin.fileno()) + ch = sys.stdin.read(1) + finally: + termios.tcsetattr(fd, termios.TCSADRAIN, old_settings) + return ch + + +class _GetchWindows: + def __init__(self): + import msvcrt + + def __call__(self): + import msvcrt + return msvcrt.getch() + +getch = _Getch() diff --git a/scripts/new_abc_commands.py b/scripts/new_abc_commands.py new file mode 100644 index 00000000..21d62d33 --- /dev/null +++ b/scripts/new_abc_commands.py @@ -0,0 +1,183 @@ + +# You can use 'from pyabc import *' and then not need the pyabc. prefix everywhere + +import os +import pyabc +import abc_common +import tempfile +import shutil +import redirect + +# A new command is just a function that accepts a list of string arguments +# The first argument is always the name of the command +# It MUST return an integer. -1: user quits, -2: error. Return 0 for success. + +# a command that calls prove(1) and returns success +def prove_cmd(args): + result = abc_common.prove(1) + print result + return 0 + +# registers the command: +# The first argument is the function +# The second argument is the category (mainly for the ABC help command) +# The third argument is the new command name +# Keep the fourth argument 0, or consult with Alan + +pyabc.add_abc_command(prove_cmd, "ZPython", "/prove", 0) + +def read_cmd(args): + if len(args)==2: + abc_common.read_file_quiet(args[1]) + else: + abc_common.read_file() + return 0 + +pyabc.add_abc_command(read_cmd, "ZPython", "/rf", 0) + +def chdir_cmd(args): + os.chdir( args[1] ) + return 0 + +pyabc.add_abc_command(chdir_cmd, "ZPython", "/cd", 0) + +def pwd_cmd(args): + print os.getcwd() + return 0 + +pyabc.add_abc_command(pwd_cmd, "ZPython", "/pwd", 0) + +def ls_cmd(args): + os.system("ls " + " ".join(args[1:])) + return 0 + +pyabc.add_abc_command(ls_cmd, "ZPython", "/ls", 0) + +pushd_temp_stack = [] + +def pushdtemp_cmd(args): + tmpdir = tempfile.mkdtemp() + pushd_temp_stack.append( (os.getcwd(), tmpdir) ) + os.chdir(tmpdir) + return 0 + +pyabc.add_abc_command(pushdtemp_cmd, "ZPython", "/pushdtemp", 0) + +def popdtemp_cmd(args): + prev, temp = pushd_temp_stack.pop() + os.chdir(prev) + shutil.rmtree(temp, ignore_errors=True) + return 0 + +pyabc.add_abc_command(popdtemp_cmd, "ZPython", "/popdtemp", 0) + +pushredirect_stack = [] + +def push_redirect_cmd(args): + fdout = redirect.start_redirect( redirect.null_file, sys.stdout) + pushredirect_stack.append( (sys.stdout, fdout) ) + + fderr = redirect.start_redirect( redirect.null_file, sys.stderr) + pushredirect_stack.append( (sys.stderr, fderr) ) + + return 0 + +pyabc.add_abc_command(push_redirect_cmd, "ZPython", "/pushredirect", 0) + +def pop_redirect_cmd(args): + err, fderr = pushredirect_stack.pop() + redirect.end_redirect(err, fderr) + + out, fdout = pushredirect_stack.pop() + redirect.end_redirect(out, fdout) + + return 0 + +pyabc.add_abc_command(pop_redirect_cmd, "ZPython", "/popredirect", 0) + +def print_aiger_result(args): + status = pyabc.prob_status() + + if status==1: + print 0 + elif status==0: + print 1 + else: + print 2 + + return 0 + +pyabc.add_abc_command(print_aiger_result, "ZPython", "/print_aiger_result", 0) + +def super_prove_aiger_cmd(args): + + noisy = len(args)==2 and args[1]=='-n' + + if not noisy: + pyabc.run_command('/pushredirect') + pyabc.run_command('/pushdtemp') + + try: + result = abc_common.super_prove() + except: + result = None + + if not noisy: + pyabc.run_command('/popdtemp') + pyabc.run_command('/popredirect') + + if result=="SAT": + print 1 + elif result=="UNSAT": + print 0 + else: + print 2 + + return 0 + +pyabc.add_abc_command(super_prove_aiger_cmd, "ZPython", "/super_prove_aiger", 0) + + +def prove_one_by_one_cmd(args): + + noisy = len(args)==2 and args[1]=='-n' + + # switch to a temporary directory + pyabc.run_command('/pushdtemp') + + # write a copy of the original file in the temporary directory + pyabc.run_command('w original_aig_file.aig') + + # iterate through the ouptus + for po in range(0, pyabc.n_pos()): + + if not noisy: + pyabc.run_command('/pushredirect') + + # replace the nework with the cone of the current PO + pyabc.run_command( 'cone -O %d -s'%po ) + + # run super_prove + try: + result = abc_common.super_prove() + except: + result = 'UNKNOWN' + + if not noisy: + pyabc.run_command('/popredirect') + + print 'PO %d is %s'%(po, result) + + # stop if the result is not UNSAT + if result != "UNSAT": + break + + # read the original file for the next iteration + pyabc.run_command('r original_aig_file.aig') + + # go back to the original directory + pyabc.run_command('/popdtemp') + + return 0 + +pyabc.add_abc_command(prove_one_by_one_cmd, "ZPython", "/prove_one_by_one", 0) diff --git a/scripts/reachx_cmd.py b/scripts/reachx_cmd.py new file mode 100644 index 00000000..dd59eb0a --- /dev/null +++ b/scripts/reachx_cmd.py @@ -0,0 +1,111 @@ +# You can use 'from pyabc import *' and then not need the pyabc. prefix everywhere + +import sys +import optparse +import subprocess +import tempfile +import threading +import os +import os.path +from contextlib import contextmanager, nested + +import pyabc + + +def wait_with_timeout(p, timeout): + """ Wait for a subprocess.Popen object to terminate, or until timeout (in seconds) expires. """ + + if timeout <= 0: + timeout = None + + t = threading.Thread(target=lambda: p.wait()) + t.start() + + t.join(timeout) + + if t.is_alive(): + p.kill() + + t.join() + + return p.returncode + +@contextmanager +def replace_sys_argv(argv): + if 'argv' in sys.__dict__: + old_argv = sys.argv + sys.argv = argv + yield + sys.argv = old_argv + else: + sys.argv = argv + yield + del sys.argv + +@contextmanager +def temp_file_name(suffix=""): + file = tempfile.NamedTemporaryFile(delete=False, suffix=suffix) + name = file.name + file.close() + + try: + yield name + finally: + os.unlink(name) + +def cygpath(path): + if sys.platform == "win32": + if os.path.isabs(path): + drive, tail = os.path.splitdrive(path) + drive = drive.lower() + tail = tail.split(os.path.sep) + return '/cygdrive/%s'%drive[0] + '/'.join(tail) + else: + path = path.split(os.path.sep) + return "/".join(path) + return path + +def run_reachx_cmd(effort, timeout): + with nested(temp_file_name(suffix=".aig"), temp_file_name()) as (tmpaig_name, tmplog_name): + pyabc.run_command("write %s"%tmpaig_name) + + cmdline = [ + 'read %s'%cygpath(tmpaig_name), + 'qua_ffix -effort %d -L %s'%(effort, cygpath(tmplog_name)), + 'quit' + ] + + cmd = ["jabc", "-c", " ; ".join(cmdline)] + + p = subprocess.Popen(cmd, shell=False, stdout=sys.stdout, stderr=sys.stderr) + + rc = wait_with_timeout(p,timeout) + + if rc != 0: + # jabc failed or stopped. Write a status file to update the status to unknown + with open(tmplog_name, "w") as f: + f.write('snl_UNK -1 unknown\n') + f.write('NULL\n') + f.write('NULL\n') + + pyabc.run_command("read_status %s"%tmplog_name) + + return rc + +def reachx_cmd(argv): + usage = "usage: %prog [options]" + + parser = optparse.OptionParser(usage) + + parser.add_option("-e", "--effort", dest="effort", type=int, default=0, help="effort level. [default=0, means unlimited]") + parser.add_option("-t", "--timeout", dest="timeout", type=int, default=0, help="timeout in seconds [default=0, unlimited]") + + with replace_sys_argv(argv): + options, args = parser.parse_args() + + rc = run_reachx_cmd(options.effort, options.timeout) + print "%s command: jabc returned: %d"%(argv[0], rc) + + return 0 + +pyabc.add_abc_command(reachx_cmd, "Verification", "reachx", 0) diff --git a/scripts/redirect.py b/scripts/redirect.py new file mode 100644 index 00000000..498fe150 --- /dev/null +++ b/scripts/redirect.py @@ -0,0 +1,94 @@ +""" + +A simple context manager for redirecting streams in Python. +The streams are redirected at the the C runtime level so that the output of C extensions +that use stdio will also be redirected. + +null_file : a stream representing the null device (e.g. /dev/null on Unix) +redirect: a context manager for redirecting streams + +Author: Baruch Sterin (sterin@berkeley.edu) + +""" + +import os +import sys + +from contextlib import contextmanager + +null_file = open( os.devnull, "w" ) + +@contextmanager +def _dup( f ): + fd = os.dup( f.fileno() ) + yield fd + os.close(fd) + +@contextmanager +def redirect(dst = null_file, src = sys.stdout): + + """ + Redirect the src stream into dst. + + Example: + with redirect( open("somefile.txt", sys.stdout ) ): + do some stuff ... + """ + + if src.fileno() == dst.fileno(): + yield + return + + with _dup( src ) as fd_dup_src: + + dst.flush() + + src.flush() + os.close( src.fileno() ) + os.dup2( dst.fileno(), src.fileno() ) + + yield + + src.flush() + os.close( src.fileno() ) + os.dup2( fd_dup_src, src.fileno() ) + +def start_redirect(dst = null_file, src = sys.stdout): + + """ + Start redirection of src stream into dst. Return the duplicated file handle of the source. + + Example: + fd = start_redirect( open("somefile.txt"), sys.stdout ) + ... do some stuff ... + end_redirect(sys.stdout, fd) + """ + + if src.fileno() == dst.fileno(): + return None + + fd_dup_src = os.dup( src.fileno() ) + + dst.flush() + src.flush() + + os.close( src.fileno() ) + os.dup2( dst.fileno(), src.fileno() ) + + return fd_dup_src + +def end_redirect(src, fd_dup_src): + + """ + End redirection of stream src.Redirect the src stream into dst. src is the source stream and fd_dup_src is the value returned by + start_redirect() + """ + + if fd_dup_src is None: + return + + src.flush() + os.close( src.fileno() ) + os.dup2( fd_dup_src, src.fileno() ) + + os.close(fd_dup_src) diff --git a/scripts/super_prove.sh b/scripts/super_prove.sh new file mode 100644 index 00000000..c3823b3a --- /dev/null +++ b/scripts/super_prove.sh @@ -0,0 +1,15 @@ +#!/bin/sh + +abc_root() +{ + cwd="$(pwd)" + cd $(dirname "$1") + echo $(dirname "$(pwd)") + cd "${cwd}" +} + +abc_dir=$(abc_root "$0") +bin_dir="${abc_dir}"/bin +aig_file="$1" + +exec ${bin_dir}/abc -c "/rf ${aig_file} ; /super_prove_aiger" -- cgit v1.2.3