aboutsummaryrefslogtreecommitdiffstats
path: root/testsuite/testenv.sh
diff options
context:
space:
mode:
authorT. Meissner <programming@goodcleanfun.de>2019-10-07 19:13:46 +0200
committertgingold <tgingold@users.noreply.github.com>2019-10-07 19:13:46 +0200
commitb405a27654f326eb1117c0eda8e7389a64fc5c94 (patch)
tree87867ece999abba761b40ea5d2debdd6018247f4 /testsuite/testenv.sh
parentbf8b41da7f0650d93b79447a2a62313b15afc9af (diff)
downloadghdl-yosys-plugin-b405a27654f326eb1117c0eda8e7389a64fc5c94.tar.gz
ghdl-yosys-plugin-b405a27654f326eb1117c0eda8e7389a64fc5c94.tar.bz2
ghdl-yosys-plugin-b405a27654f326eb1117c0eda8e7389a64fc5c94.zip
testsuite: Add formal tests (#57)
* Add formal tests for shift operations * ci: build ghdl/synth:formal and run test suites in it * add testsuite/formal/testsuite.sh * create testsuite/issues * ci: remove a level of grouping * testenv: fix SYMBIYOSYS * refactor * testsuite/formal/shifts: Add check for shifts > vector length
Diffstat (limited to 'testsuite/testenv.sh')
-rw-r--r--testsuite/testenv.sh18
1 files changed, 16 insertions, 2 deletions
diff --git a/testsuite/testenv.sh b/testsuite/testenv.sh
index 23c67e0..b736b91 100644
--- a/testsuite/testenv.sh
+++ b/testsuite/testenv.sh
@@ -12,6 +12,10 @@ if [ x"$YOSYS" = x ]; then
YOSYS="yosys -m ../../ghdl.so"
fi
+if [ x"$SYMBIYOSYS" = x ]; then
+ SYMBIYOSYS="sby"
+fi
+
cmd ()
{
echo "ยท $@"
@@ -23,6 +27,11 @@ run_yosys ()
cmd $YOSYS "$@"
}
+run_symbiyosys ()
+{
+ cmd $SYMBIYOSYS --yosys "$YOSYS" "$@"
+}
+
analyze ()
{
printf "${ANSI_BLUE}Analyze $@ $ANSI_NOCOLOR\n"
@@ -36,10 +45,15 @@ synth ()
travis_finish "synth"
}
+formal ()
+{
+ travis_start "formal" "Verify $@"
+ run_symbiyosys -f -d work $@.sby
+ travis_finish "formal"
+}
+
clean ()
{
- travis_start "rm" "Remove work library"
"$GHDL" --remove $GHDL_STD_FLAGS
rm -f out.blif
- travis_finish "rm"
}