blob: deb4884d3d2ebe55c68d8784c63bb6e59a054c42 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
|
#!/usr/bin/env bash
# SPDX-License-Identifier: Apache-2.0
# 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 3 ]; then
echo "There must be exactly three arguments!"
exit -1
fi
HASH1=`git rev-parse $1`
HASH2=`git rev-parse $2`
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!"
exit 0
fi
RET=""
make_verilog () {
git checkout $1
local filename="$DUT.$1.v"
sbt "clean; runMain firrtl.stage.FirrtlMain -i $DUT.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 $DUT top1
proc
memory
flatten top1
hierarchy -top top1
read_verilog $FILE2
rename $DUT top2
proc
memory
flatten top2
equiv_make top1 top2 equiv
hierarchy -top equiv
clean -purge
equiv_simple -short
equiv_induct
equiv_status -assert
"
fi
|
