diff options
| -rw-r--r-- | .run_formal_checks.sh | 17 | ||||
| -rw-r--r-- | .travis.yml | 3 | ||||
| -rw-r--r-- | scripts/formal_equiv.sh | 57 |
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 |