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"