mirror of https://github.com/YosysHQ/yosys.git
91 lines
1.6 KiB
Bash
91 lines
1.6 KiB
Bash
#!/usr/bin/env bash
|
|
|
|
set -e
|
|
|
|
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
|
|
set -x
|
|
$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
|
|
|
|
# Check that SBY is up to date enough for this yosys version
|
|
if sby --help | grep -q -e '--status'; then
|
|
set -x
|
|
sby --yosys $PWD/../../yosys -f ${prefix}_pass.sby
|
|
sby --yosys $PWD/../../yosys -f ${prefix}_fail.sby
|
|
else
|
|
echo "sva test '${prefix}' requires an up to date SBY, skipping"
|
|
fi
|
|
else
|
|
generate_sby pass > ${prefix}.sby
|
|
|
|
# Check that SBY is up to date enough for this yosys version
|
|
if sby --help | grep -q -e '--status'; then
|
|
set -x
|
|
sby --yosys $PWD/../../yosys -f ${prefix}.sby
|
|
else
|
|
echo "sva test '${prefix}' requires an up to date SBY, skipping"
|
|
fi
|
|
fi
|
|
|
|
{ set +x; } &>/dev/null
|
|
|
|
touch $prefix.ok
|
|
|