diff options
| author | Jack Koenig | 2017-12-12 15:33:00 -0800 |
|---|---|---|
| committer | Jack Koenig | 2017-12-12 15:34:43 -0800 |
| commit | 0d794d57df7b388109d7a0834d3b5be8f79892be (patch) | |
| tree | f557811fb961a3125bbfef95815eb81f72ca8346 /.run_formal_checks.sh | |
| parent | e39609a2bfbbd108fa1e5044e9c270685d75a816 (diff) | |
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
Diffstat (limited to '.run_formal_checks.sh')
| -rwxr-xr-x[-rw-r--r--] | .run_formal_checks.sh | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/.run_formal_checks.sh b/.run_formal_checks.sh index f3b72a67..ace9e4b0 100644..100755 --- 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 |