summaryrefslogtreecommitdiff
path: root/backends/btor
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2014-01-24 15:48:07 +0100
committerClifford Wolf <clifford@clifford.at>2014-01-24 15:48:07 +0100
commit6804edd5d4cc6cca1fbdf7cf6db236d0fcd46538 (patch)
tree050e881fbf222d07c5dad54767cdbaf9ad9dc810 /backends/btor
parentda26bb43782dc9be3bac66405ce6aad7068500da (diff)
Moved btor scripts to backends/btor/
Diffstat (limited to 'backends/btor')
-rw-r--r--backends/btor/btor.ys15
-rwxr-xr-xbackends/btor/verilog2btor.sh35
2 files changed, 50 insertions, 0 deletions
diff --git a/backends/btor/btor.ys b/backends/btor/btor.ys
new file mode 100644
index 00000000..7f3882b5
--- /dev/null
+++ b/backends/btor/btor.ys
@@ -0,0 +1,15 @@
+proc;
+opt; opt_const -mux_undef; opt;
+rename -hide;;;
+#converting pmux to mux
+techmap -map techlibs/common/pmux2mux.v;;
+memory -nomap;;
+#flatten design
+flatten;;
+#converting asyn memory write to syn memory
+memory_unpack;
+#cell output to be a single wire
+splitnets -driver;
+setundef -zero -undriven;
+opt;;;
+
diff --git a/backends/btor/verilog2btor.sh b/backends/btor/verilog2btor.sh
new file mode 100755
index 00000000..ef0134e0
--- /dev/null
+++ b/backends/btor/verilog2btor.sh
@@ -0,0 +1,35 @@
+#!/bin/sh
+
+#
+# Script to writing 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 $1;
+hierarchy -top $3;
+hierarchy -libdir $DIR;
+hierarchy -check;
+proc;
+opt; opt_const -mux_undef; opt;
+rename -hide;;;
+techmap -map $YOSYS_HOME/techlibs/common/pmux2mux.v;;
+memory -nomap;;
+flatten;;
+memory_unpack;
+splitnets -driver;
+setundef -zero -undriven;
+opt;;;
+write_btor $2;"
+