blob: 004a172bad8708ec699dda9a659a97ecb2a05fc1 (
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
|
#!/bin/bash
set -ex
prefix=${1%.sv}
test -f $prefix.sv
generate_sby() {
cat <<- EOT
[options]
mode bmc
depth 10
expect $1
[engines]
smtbmc yices
[script]
EOT
if [ "$1" = "fail" ]; then
echo "verific -sv ${prefix}_fail.sv"
else
echo "verific -sv $prefix.sv"
fi
if [ -f $prefix.vhd ]; then
echo "verific -vhdl2008 $prefix.vhd"
fi
cat <<- EOT
verific -import -extnets -all top
prep -top top
[files]
$prefix.sv
EOT
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
}
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
touch $prefix.ok
|
