Skip to content

A
abc
Switch branch/tag
Find file
Normal viewHistoryPermalink
abc.rc 12.7 KB
Newer Older
initial commit of public abc
6130e39b
 
Alan Mishchenko committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 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"