aboutsummaryrefslogtreecommitdiff
path: root/scripts
diff options
context:
space:
mode:
authorJack Koenig2017-12-12 16:06:31 -0800
committerGitHub2017-12-12 16:06:31 -0800
commitdf579547f769843b76922dbb055ea26839b1d7d4 (patch)
treef557811fb961a3125bbfef95815eb81f72ca8346 /scripts
parent0fd0c66adcf1226ee5947cdaa5629bf59c4123f1 (diff)
parent0d794d57df7b388109d7a0834d3b5be8f79892be (diff)
Merge pull request #684 from freechipsproject/remove-wires
Remove wires, replacing them with nodes
Diffstat (limited to 'scripts')
-rwxr-xr-x[-rw-r--r--]scripts/formal_equiv.sh24
1 files changed, 17 insertions, 7 deletions
diff --git a/scripts/formal_equiv.sh b/scripts/formal_equiv.sh
index 9e744d46..2e9fa74d 100644..100755
--- a/scripts/formal_equiv.sh
+++ b/scripts/formal_equiv.sh
@@ -1,16 +1,19 @@
+#!/usr/bin/env bash
# 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!"
+if [ $# -ne 3 ]; then
+ echo "There must be exactly three arguments!"
exit -1
fi
HASH1=`git rev-parse $1`
HASH2=`git rev-parse $2`
-echo "Comparing git revisions $HASH1 and $HASH2"
+DUT=$3
+
+echo "Comparing git revisions $HASH1 and $HASH2 on $DUT"
if [ $HASH1 = $HASH2 ]; then
echo "Both git revisions are the same! Nothing to do!"
@@ -20,10 +23,10 @@ fi
RET=""
make_verilog () {
git checkout $1
- local filename="rob.$1.v"
+ local filename="$DUT.$1.v"
sbt clean
- sbt "run-main firrtl.Driver -i regress/Rob.fir -o $filename -X verilog"
+ sbt "run-main firrtl.Driver -i $DUT.fir -o $filename -X verilog"
RET=$filename
}
@@ -43,11 +46,18 @@ else
echo "Running equivalence check using Yosys"
yosys -q -p "
read_verilog $FILE1
- rename Rob top1
+ rename $DUT top1
+ proc
+ memory
+ flatten top1
+ hierarchy -top top1
+
read_verilog $FILE2
- rename Rob top2
+ rename $DUT top2
proc
memory
+ flatten top2
+
equiv_make top1 top2 equiv
hierarchy -top equiv
clean -purge