Add script for formally comparing emitted Verilog

Also add Travis test for running this script on PRs

3 files changed, 77 insertions, 0 deletions

diff --git a/.run_formal_checks.sh b/.run_formal_checks.sh
new file mode 100644
index 00000000..f3b72a67
--- /dev/null
+++ b/.run_formal_checks.sh
@@ -0,0 +1,17 @@
+set -e
+# Run formal check only for PRs
+if [ $TRAVIS_PULL_REQUEST = "false" ]; then
+    echo "Not a pull request, no formal check"
+    exit 0
+elif [[ $TRAVIS_COMMIT_MESSAGE == *"[skip formal checks]"* ]]; then
+    echo "Commit message says to skip formal checks"
+    exit 0
+else
+    # $TRAVIS_BRANCH is branch targeted by PR
+    # Travis does a shallow clone, checkout PR target so that we have it
+    # THen return to previous branch so HEAD points to the commit we're testing
+    git remote set-branches origin $TRAVIS_BRANCH && git fetch
+    git checkout $TRAVIS_BRANCH
+    git checkout -
+    bash ./scripts/formal_equiv.sh HEAD $TRAVIS_BRANCH
+fi
diff --git a/.travis.yml b/.travis.yml
index b41ba9b3..00a1fca2 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -32,3 +32,6 @@ jobs:
       script:
         - sbt clean assembly publish-local
         - bash .run_chisel_tests.sh
+    - stage: test
+      script:
+        - bash .run_formal_checks.sh
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