From 0d794d57df7b388109d7a0834d3b5be8f79892be Mon Sep 17 00:00:00 2001
From: Jack Koenig
Date: Tue, 12 Dec 2017 15:33:00 -0800
Subject: Refactor formal equivalence CI test

Make the check script allow different designs
Add FPU, ICache, and RocketCore to regress and use instead of Rob for CI
equivalence check
---
 .run_formal_checks.sh | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)
 mode change 100644 => 100755 .run_formal_checks.sh

(limited to '.run_formal_checks.sh')

diff --git a/.run_formal_checks.sh b/.run_formal_checks.sh
old mode 100644
new mode 100755
index f3b72a67..ace9e4b0
--- a/.run_formal_checks.sh
+++ b/.run_formal_checks.sh
@@ -1,4 +1,13 @@
+#!/usr/bin/env bash
 set -e
+
+if [ $# -ne 1 ]; then
+    echo "There must be exactly one argument!"
+    exit -1
+fi
+
+DUT=$1
+
 # Run formal check only for PRs
 if [ $TRAVIS_PULL_REQUEST = "false" ]; then
     echo "Not a pull request, no formal check"
@@ -13,5 +22,6 @@ else
     git remote set-branches origin $TRAVIS_BRANCH && git fetch
     git checkout $TRAVIS_BRANCH
     git checkout -
-    bash ./scripts/formal_equiv.sh HEAD $TRAVIS_BRANCH
+    cp regress/$DUT.fir $DUT.fir
+    ./scripts/formal_equiv.sh HEAD $TRAVIS_BRANCH $DUT
 fi
-- 
cgit v1.2.3