diff options
Diffstat (limited to 'scripts/abc.rc')
| -rw-r--r-- | scripts/abc.rc | 288 |
1 files changed, 47 insertions, 241 deletions
diff --git a/scripts/abc.rc b/scripts/abc.rc index a39ed76a..365a49ca 100644 --- a/scripts/abc.rc +++ b/scripts/abc.rc @@ -1,10 +1,12 @@ +# reachx python new_abc_commands.py python -c "import reachx_cmd" + # 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 +#unset checkread # does not check 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 @@ -23,29 +25,39 @@ set capounix MetaPl-Capo10.1 set gnuplotwin wgnuplot.exe set gnuplotunix gnuplot -# standard aliases -alias srw "b; rw; b" -alias fix "ps; st; ps; srw; ps; plat; cycle -x -F 1; plat; logic; undc; st; zero; ps; scorr; ps" -alias fixp "st; srw; cycle -x -F 1; logic; undc; st; zero " +# Niklas Een's commands +#load_plugin C:\_projects\abc\lib\bip_win.exe "BIP" +#load_plugin /hd/common/pyabc/bip "BIP" +# standard aliases +alias hi history alias b balance +alias cg clockgate alias cl cleanup alias clp collapse +alias cs care_set alias esd ext_seq_dcs alias f fraig alias fs fraig_sweep alias fsto fraig_store alias fres fraig_restore +alias fr fretime alias ft fraig_trust +alias ic indcut alias lp lutpack +alias pcon print_cone alias pd print_dsd alias pex print_exdc -d alias pf print_factor alias pfan print_fanio +alias pg print_gates alias pl print_level +alias plat print_latch alias pio print_io alias pk print_kmap +alias pm print_miter alias ps print_stats +alias psb print_stats -b alias psu print_supp alias psy print_symm alias pun print_unate @@ -53,16 +65,15 @@ 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 r3f retime -M 3 -f +alias r3b retime -M 3 -b alias ren renode alias rh read_hie +alias ri read_init alias rl read_blif alias rb read_bench alias ret retime +alias dret dretime alias rp read_pla alias rt read_truth alias rv read_verilog @@ -70,8 +81,10 @@ alias rvl read_verlib alias rsup read_super mcnc5_old.super alias rlib read_library alias rlibc read_library cadence.genlib -alias rw drw -alias rwz drw -z +alias rty read_liberty +alias rlut read_lut +alias rw rewrite +alias rwz rewrite -z alias rf refactor alias rfz refactor -z alias re restructure @@ -79,7 +92,6 @@ 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 @@ -100,242 +112,36 @@ alias wp write_pla alias wv write_verilog # standard scripts -alias share "b; multi; fx; b" -alias resyn "b; drw; rwz; b; rwz; b" -alias resyn2 "b; drw; rf; b; drw; rwz; b; rfz; rwz; b" -alias resyn2a "b; drw; b; drw; rwz; b; rwz; 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; drw -l; rwz -l; b -l; rwz -l; b -l" - -alias compress2 "b -l; drw -l; rf -l; b -l; drw -l; rwz -l; b -l; rfz -l; rwz -l; b -l" +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; drw -l; b -l; drw -l; rf -l" -alias rwsat2 "st; drw -l; b -l; drw -l; rf -l; fraig; drw -l; b -l; drw -l; rf -l" -alias shake "st; ps; sat -C 5000; drw -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 " +alias rwsat "st; rw -l; b -l; rw -l; rf -l" +alias drwsat2 "st; drw; b -l; drw; drf; ifraig -C 20; drw; b -l; drw; drf" +alias share "st; multi -m; fx; resyn2" +alias addinit "read_init; undc; strash; zero" +alias blif2aig "undc; strash; zero" +alias v2p "&vta_gla; &ps; &gla_derive; &put; w 1.aig; pdr -v" +alias g2p "&ps; &gla_derive; &put; w 2.aig; pdr -v" # resubstitution scripts for the IWLS paper -alias src_rw "st; drw -l; rwz -l; rwz -l" +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; drw -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; drw; rs -K 6 -N 2; rf; rs -K 8; b; rs -K 8 -N 2; drw; 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; drw -l; rs -K 6 -N 2 -l; rf -l; rs -K 8 -l; b -l; rs -K 8 -N 2 -l; drw -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; drw -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; drw; rs -K 6 -N 2 -F 2; rf; rs -K 8 -F 2; b; rs -K 8 -N 2 -F 2; drw; 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; drw -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; drw -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;drw;dr;lcorr;drw;dr;ps;scorr;ps;fraig;ps;dc2;dr;scorr -F 2;ps;dc2rs;w temp.aig" -alias smp1 "scl;drw;dr;lcorr;drw;dr;scorr;fraig;dc2rs" -alias smp2 "ua;ps;scl;ps;drw;dr;lcorr;drw;dr;ps;scorr;ps;fraig;ps;dc2;dr;ps;dc2rs;w temp.aig" -alias smpf "ua;ps;scl;lcr;ps;drw;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;drw;&get;&ps;&scl;&ps;&put;dr;&get;&ps;&lcorr;&ps;&dc2;&ps;&scorr;&ps;&put;drw;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;drw;ps;scorr -c;ps;fraig;ps;compress2rs;ps" - -alias abseen "&get;,abs -vt=60 -timeout=60 -bob=10 -aig=temp.aig;r temp.aig" -alias pdreen "&get;,pdr -vt=60" -alias inteen "&get;,imc -vt=60" -alias bmceen "&get;,bmc -vt=60" - +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" +# use this script to convert 1-valued and DC-valued flops for an AIG +alias fix_aig "logic; undc; strash; zero" +# use this script to convert 1-valued and DC-valued flops for a logic network coming from BLIF +alias fix_blif "undc; strash; zero" +# lazy man's synthesis +alias recadd3 "st; rec_add3; b; rec_add3; dc2; rec_add3; if -K 8; bidec; st; rec_add3; dc2; rec_add3; if -g -K 6; st; rec_add3" |