Add script for formally comparing emitted Verilog

Also add Travis test for running this script on PRs

1 files changed, 57 insertions, 0 deletions

diff --git a/scripts/formal_equiv.sh b/scripts/formal_equiv.sh
new file mode 100644
index 00000000..f7b0fa40
--- /dev/null
+++ b/scripts/formal_equiv.sh
@@ -0,0 +1,57 @@
+# This script is for formally comparing the Verilog emitted by different git revisions
+# There must be two valid git revision arguments
+set -e
+
+if [ $# -ne 2 ]; then
+    echo "There must be exactly two arguments!"
+    exit -1
+fi
+
+HASH1=`git rev-parse $1`
+HASH2=`git rev-parse $2`
+
+echo "Comparing git revisions $HASH1 and $HASH2"
+
+if [ $HASH1 = $HASH2 ]; then
+    echo "Both git revisions are the same! Nothing to do!"
+    exit 0
+fi
+
+RET=""
+make_verilog () {
+    git checkout $1
+    local filename="rob.$1.v"
+
+    sbt clean
+    sbt "run-main firrtl.Driver -i regress/Rob.fir -o $filename -X verilog"
+    RET=$filename
+}
+
+# Generate Verilog to compare
+make_verilog $HASH1
+FILE1=$RET
+
+make_verilog $HASH2
+FILE2=$RET
+
+echo "Comparing $FILE1 and $FILE2"
+
+if cmp -s $FILE1 $FILE2; then
+    echo "File contents are identical!"
+    exit 0
+else
+    echo "Running equivalence check using Yosys"
+    yosys -q -p "
+      read_verilog $FILE1
+      rename Rob top1
+      read_verilog $FILE2
+      rename Rob top2
+      proc
+      memory
+      equiv_make top1 top2 equiv
+      hierarchy -top equiv
+      clean -purge
+      equiv_simple
+      equiv_status -assert
+    "
+fi