mirror of https://github.com/YosysHQ/yosys.git
Remove old BTOR back-end
This commit is contained in:
parent
5b6e52118c
commit
eceacdb9a3
|
@ -1,3 +0,0 @@
|
|||
|
||||
OBJS += backends/btor/btor.o
|
||||
|
|
@ -1,23 +0,0 @@
|
|||
|
||||
This is the Yosys BTOR backend.
|
||||
It is developed by Ahmed Irfan <irfan@fbk.eu> - Fondazione Bruno Kessler, Trento, Italy
|
||||
|
||||
Master git repository for the BTOR backend:
|
||||
https://github.com/ahmedirfan1983/yosys
|
||||
|
||||
|
||||
[[CITE]] BTOR: Bit-Precise Modelling of Word-Level Problems for Model Checking
|
||||
Johannes Kepler University, Linz, Austria
|
||||
http://fmv.jku.at/papers/BrummayerBiereLonsing-BPR08.pdf
|
||||
|
||||
|
||||
Todos:
|
||||
------
|
||||
|
||||
- Add checks for unsupported stuff
|
||||
- unsupported cell types
|
||||
- async resets
|
||||
- etc..
|
||||
|
||||
- Add support for $lut cells
|
||||
|
File diff suppressed because it is too large
Load Diff
|
@ -1,37 +0,0 @@
|
|||
#!/bin/sh
|
||||
|
||||
#
|
||||
# Script to write BTOR from Verilog design
|
||||
#
|
||||
|
||||
if [ "$#" -ne 3 ]; then
|
||||
echo "Usage: $0 input.v output.btor top-module-name" >&2
|
||||
exit 1
|
||||
fi
|
||||
if ! [ -e "$1" ]; then
|
||||
echo "$1 not found" >&2
|
||||
exit 1
|
||||
fi
|
||||
|
||||
FULL_PATH=$(readlink -f $1)
|
||||
DIR=$(dirname $FULL_PATH)
|
||||
|
||||
./yosys -q -p "
|
||||
read_verilog -sv $1;
|
||||
hierarchy -top $3;
|
||||
hierarchy -libdir $DIR;
|
||||
hierarchy -check;
|
||||
proc;
|
||||
opt; opt_expr -mux_undef; opt;
|
||||
rename -hide;;;
|
||||
#techmap -map +/pmux2mux.v;;
|
||||
splice; opt;
|
||||
memory_dff -wr_only;
|
||||
memory_collect;;
|
||||
flatten;;
|
||||
memory_unpack;
|
||||
splitnets -driver;
|
||||
setundef -zero -undriven;
|
||||
opt;;;
|
||||
write_btor $2;"
|
||||
|
Loading…
Reference in New Issue