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 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 332 insertions(+) create mode 100644 scripts/abc.rc (limited to 'scripts/abc.rc') 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" + + + + + + -- cgit v1.2.3