From b103bc89a6819115651b244df191f00969a539af Mon Sep 17 00:00:00 2001
From: Jack Koenig
Date: Sun, 1 Oct 2017 14:09:02 -0700
Subject: Add script for formally comparing emitted Verilog

Also add Travis test for running this script on PRs
---
 .run_formal_checks.sh | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100644 .run_formal_checks.sh

(limited to '.run_formal_checks.sh')

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
-- 
cgit v1.2.3