mirror of
https://github.com/YosysHQ/yosys
synced 2025-04-07 18:05:24 +00:00
Merge branch 'btor-ng'
This commit is contained in:
commit
8e22e8118a
|
@ -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
30
backends/btor/test_cells.sh
Normal file
30
backends/btor/test_cells.sh
Normal file
|
@ -0,0 +1,30 @@
|
|||
#!/bin/bash
|
||||
|
||||
set -ex
|
||||
|
||||
rm -rf test_cells.tmp
|
||||
mkdir -p test_cells.tmp
|
||||
cd test_cells.tmp
|
||||
|
||||
../../../yosys -p 'test_cell -n 5 -w test all /$alu /$fa /$lcu /$lut /$sop /$macc /$mul /$div /$mod'
|
||||
|
||||
for fn in test_*.il; do
|
||||
../../../yosys -p "
|
||||
read_ilang $fn
|
||||
rename gold gate
|
||||
synth
|
||||
|
||||
read_ilang $fn
|
||||
miter -equiv -make_assert -flatten gold gate main
|
||||
hierarchy -top main
|
||||
write_btor ${fn%.il}.btor
|
||||
"
|
||||
boolectormc -kmax 1 --trace-gen --stop-first -v ${fn%.il}.btor > ${fn%.il}.out
|
||||
if grep " SATISFIABLE" ${fn%.il}.out; then
|
||||
echo "Check failed for ${fn%.il}."
|
||||
exit 1
|
||||
fi
|
||||
done
|
||||
|
||||
echo "OK."
|
||||
|
|
@ -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 a new issue