mirror of https://github.com/YosysHQ/abc.git
344 lines
13 KiB
Plaintext
344 lines
13 KiB
Plaintext
python new_abc_commands.py
|
|
python reachx_cmd.py
|
|
|
|
load_plugin bip "Bip"
|
|
|
|
# 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 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 "
|
|
|
|
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 drw
|
|
alias rwz drw -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; 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 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 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 "
|
|
|
|
# resubstitution scripts for the IWLS paper
|
|
alias src_rw "st; drw -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"
|
|
|
|
|
|
|
|
|
|
|
|
|