initial commit of public abc

1 files changed, 332 insertions, 0 deletions

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"
+
+
+
+
+
+