diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2015-06-22 23:05:13 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2015-06-22 23:05:13 -0700 |
| commit | 51a646a355c78cf0f4cf104d6316706653b24008 (patch) | |
| tree | 4584ce9a96b88d32f110944f76b29ab90bb92a99 /abc.rc | |
| parent | 327078393947f3c2e0b5548e5fada9ee67ef6134 (diff) | |
| download | abc-51a646a355c78cf0f4cf104d6316706653b24008.tar.gz abc-51a646a355c78cf0f4cf104d6316706653b24008.tar.bz2 abc-51a646a355c78cf0f4cf104d6316706653b24008.zip | |
Version abc90901
committer: Baruch Sterin <baruchs@gmail.com>
Diffstat (limited to 'abc.rc')
| -rw-r--r-- | abc.rc | 50 |
1 files changed, 46 insertions, 4 deletions
@@ -2,8 +2,8 @@ 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 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 @@ -138,9 +138,51 @@ alias pjsolve "scl; dc2; fr; dc2; ic; ic -t; if -a; cs tacas/005_care.aig; mfs alias t0 "r test/mc1.blif; st; test" alias t1 "r s27mc2.blif; st; test" alias t2 "r i/intel_001.aig; ps; indcut -v" -alias t "r c\s\0\000.aig; int" +#alias t "r c\s\0\000.aig; int" #alias t "r test/interpol.blif; st; int" +alias t "&r s444.aig; &ps; &era -v" -#read_library at\syn\brdcm.genlib + +alias spec "&r 1.aig;&srm -s;r gsrm.aig; bmc2 -F 1000 -C 10000; &resim; &w 1.aig; &ps " +alias spech "&r 1.aig;&srm -s;r gsrm.aig;scl;ps; bmc2 -F 1000 -C 25000; &resim; &w 1.aig; &ps " +alias spechx "&r 1.aig;&srm ;r gsrm.aig;smp;bmc2 -F 5000 -C 75000; &resim; &w 1.aig; &ps " +alias specb "&r 1.aig;&srm ;r gsrm.aig;smp;ps; reach -o -B 1000000 -F 2000; &resim; &w 1.aig; &ps " +alias specp "&r 1.aig;&srm ;r gsrm.aig;scorr -F 2;ps; simpk ; &resim; &w 1.aig; &ps " +alias sprb "ua; &get; eclassh; specb" +alias sprh "ua; &get; eclassh; spech" + +alias eclass "&equiv -smf -W 255 -F 1000; &w 1.aig" +alias transfer "w 1.aig; &r 1.aig" +alias &ua "set autoexec " +alias scr "&get; &scorr; &put" +alias lcr "&get; &lcorr; &put" +alias trm "logic;trim;st;ps" +alias inth "int -rv -C 25000" + +alias spr "ua; &get; eclass; spech" +alias reachx "reach -o -B 1000000000 -F 5000" +alias dc2rs "ua; compress2rs; ps" +alias simp "dprove -vrcbju -C 5000 -V 1" +alias simpk "dprove -vrcbkmfiu -B 10 -D 1000" +alias indh "ind -v -F 50 -C 10000" + +alias eclassh "&equiv -smf -W 512 -F 2000; &w 1.aig" +alias ffx "ps;orpos;qua_ffix" +alias bfx "ps;orpos;qua_bfix" +alias smp "ua;ps;scl;rw;dr;lcorr;rw;dr;scorr;fraig;dc2;dr;scorr -F 2;dc2rs;w temp.aig" + +alias s "w temp.aig" + +alias absh "abs -se -D 25000" +alias absr "abs -ser -G 2000" +alias absp "abs -sep -G 2000" + +alias spechi "ua; &get; &equiv -smf -W 512 -F 2000; &ps; &speci; &srm; r gsrm.aig;&ps;&w 1.aig" +alias spechis "ua; &get; &equiv -s -W 512 -F 2000; &ps; &speci; &srm -s; r gsrm.aig; &ps; &w 1.aig" +alias absh1 "absh -R 1" +alias simpkh "simpk -D 25000" + +alias spechisf "ua; &get; &equiv -smf -W 512 -F 2000; &ps; &semi -R 5; &srm; r gsrm.aig;&ps;&w 1.aig" +alias spechissf "ua; &get; &equiv -s -W 512 -F 2000; &ps; ; &srm -s; r gsrm.aig; &ps; &w 1.aig" |