blob: 2ecc9780c5de124d9f9f542f7d02c4f63bbaf474 (
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
71
72
73
|
#!/bin/bash
set -ex
prefix=${1%.ok}
prefix=${prefix%.sv}
prefix=${prefix%.vhd}
test -f $prefix.sv -o -f $prefix.vhd
generate_sby() {
cat <<- EOT
[options]
mode bmc
depth 10
expect $1
[engines]
smtbmc yices
[script]
EOT
if [ -f $prefix.sv ]; then
if [ "$1" = "fail" ]; then
echo "read -sv ${prefix}_fail.sv"
else
echo "read -sv $prefix.sv"
fi
fi
if [ -f $prefix.vhd ]; then
echo "read -vhdl $prefix.vhd"
fi
cat <<- EOT
prep -top top
chformal -early -assume
[files]
EOT
if [ -f $prefix.sv ]; then
echo "$prefix.sv"
fi
if [ -f $prefix.vhd ]; then
echo "$prefix.vhd"
fi
if [ "$1" = "fail" ]; then
cat <<- EOT
[file ${prefix}_fail.sv]
\`define FAIL
\`include "$prefix.sv"
EOT
fi
}
if [ -f $prefix.ys ]; then
$PWD/../../yosys -q -e "Assert .* failed." -s $prefix.ys
elif [ -f $prefix.sv ]; then
generate_sby pass > ${prefix}_pass.sby
generate_sby fail > ${prefix}_fail.sby
sby --yosys $PWD/../../yosys -f ${prefix}_pass.sby
sby --yosys $PWD/../../yosys -f ${prefix}_fail.sby
else
generate_sby pass > ${prefix}.sby
sby --yosys $PWD/../../yosys -f ${prefix}.sby
fi
touch $prefix.ok
|
