From b405a27654f326eb1117c0eda8e7389a64fc5c94 Mon Sep 17 00:00:00 2001
From: "T. Meissner" <programming@goodcleanfun.de>
Date: Mon, 7 Oct 2019 19:13:46 +0200
Subject: 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
---
 travis.sh | 27 ++++++++++++++++++++++-----
 1 file changed, 22 insertions(+), 5 deletions(-)

(limited to 'travis.sh')

diff --git a/travis.sh b/travis.sh
index 086f497..2ce0d20 100755
--- a/travis.sh
+++ b/travis.sh
@@ -5,7 +5,7 @@ set -e
 cd "$(dirname $0)"
 . ./utils.sh
 
-prefix='//opt/ghdl'
+prefix='/opt/ghdl'
 
 #--
 travis_start "ghdl" "[Build] ghdl/synth:latest" "$ANSI_MAGENTA"
@@ -67,11 +67,28 @@ EOF
 
 travis_finish "ghdlsynth"
 #---
-travis_start "testsuite" "[Test] testsuite" "$ANSI_MAGENTA"
+travis_start "formal" "[Build] ghdl/synth:formal" "$ANSI_MAGENTA"
 
-docker run --rm -t -e TRAVIS=$TRAVIS -v /$(pwd)://src -w //src -e YOSYS='yosys -m ghdl' ghdl/synth:beta bash -c "$(cat <<EOF
+docker build -t ghdl/synth:formal . -f- <<-EOF
+FROM ghdl/synth:beta
+
+COPY --from=ghdl/cache:formal ./z3 /opt/z3
+COPY --from=ghdl/cache:formal ./symbiyosys /usr/local
+
+RUN apt-get update -qq \
+ && DEBIAN_FRONTEND=noninteractive apt-get -y install --no-install-recommends \
+    python3 \
+ && apt-get autoclean && apt-get clean && apt-get -y autoremove \
+ && rm -rf /var/lib/apt/lists/*
+
+ENV PATH=/opt/z3/bin:\$PATH
+EOF
+
+travis_finish "formal"
+#---
+printf "${ANSI_MAGENTA}[Test] testsuite ${ANSI_NOCOLOR}\n"
+
+docker run --rm -t -e TRAVIS=$TRAVIS -v /$(pwd)://src -w //src -e YOSYS='yosys -m ghdl' ghdl/synth:formal bash -c "$(cat <<EOF
 ./testsuite/testsuite.sh
 EOF
 )"
-
-travis_finish "testsuite"
-- 
cgit v1.2.3