aboutsummaryrefslogtreecommitdiffstats
path: root/tests/sva/runtest.sh
diff options
context:
space:
mode:
Diffstat (limited to 'tests/sva/runtest.sh')
-rw-r--r--tests/sva/runtest.sh11
1 files changed, 6 insertions, 5 deletions
diff --git a/tests/sva/runtest.sh b/tests/sva/runtest.sh
index 1b65ca9c9..2ecc9780c 100644
--- a/tests/sva/runtest.sh
+++ b/tests/sva/runtest.sh
@@ -22,18 +22,17 @@ generate_sby() {
if [ -f $prefix.sv ]; then
if [ "$1" = "fail" ]; then
- echo "verific -sv ${prefix}_fail.sv"
+ echo "read -sv ${prefix}_fail.sv"
else
- echo "verific -sv $prefix.sv"
+ echo "read -sv $prefix.sv"
fi
fi
if [ -f $prefix.vhd ]; then
- echo "verific -vhdl $prefix.vhd"
+ echo "read -vhdl $prefix.vhd"
fi
cat <<- EOT
- verific -import -extnets -all top
prep -top top
chformal -early -assume
@@ -58,7 +57,9 @@ generate_sby() {
fi
}
-if [ -f $prefix.sv ]; then
+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