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
---
 scripts/formal_equiv.sh | 24 +++++++++++++++++-------
 1 file changed, 17 insertions(+), 7 deletions(-)
 mode change 100644 => 100755 scripts/formal_equiv.sh

(limited to 'scripts')

diff --git a/scripts/formal_equiv.sh b/scripts/formal_equiv.sh
old mode 100644
new mode 100755
index 9e744d46..2e9fa74d
--- 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
-- 
cgit v1.2.3