From d61845a837b54e18b80d4782aa76228bae71ab89 Mon Sep 17 00:00:00 2001
From: Fabian Schuiki <fabian@schuiki.ch>
Date: Wed, 15 Jan 2025 17:26:36 -0800
Subject: [PATCH] Add sanity checks for z3, yosys, and sby installations

After installation, execute the tools on a simple example to check that
they have been properly installed. This is especially useful for Yosys
and SymbiYosys which depend on each other and z3, and other Python
dependencies.
---
 integration-test/sby.sh   | 21 +++++++++++++++++++++
 integration-test/yosys.sh | 17 +++++++++++++++++
 integration-test/z3.sh    | 13 +++++++++++++
 3 files changed, 51 insertions(+)

diff --git a/integration-test/sby.sh b/integration-test/sby.sh
index a63fab2..79b7fd0 100755
--- a/integration-test/sby.sh
+++ b/integration-test/sby.sh
@@ -1,5 +1,6 @@
 #!/bin/bash
 # Downloads, compiles, and installs SymbiYosys
+set -xe
 
 YOSYS_VER=0.47
 
@@ -11,3 +12,23 @@ cd sby-yosys-$YOSYS_VER
 make PREFIX=/usr install
 cd ..
 rm -r sby-yosys-$YOSYS_VER
+
+# Perform a sanity check.
+cat > /tmp/sanity.v <<EOF
+module Foo(a);
+  input [7:0] a;
+  assert property (a * 2 == a + a);
+endmodule
+EOF
+
+sby <<EOF
+[options]
+mode prove
+
+[engines]
+smtbmc z3
+
+[script]
+read -formal /tmp/sanity.v
+prep -top Foo
+EOF
diff --git a/integration-test/yosys.sh b/integration-test/yosys.sh
index 353abcc..e63ff5d 100755
--- a/integration-test/yosys.sh
+++ b/integration-test/yosys.sh
@@ -1,5 +1,6 @@
 #!/bin/bash
 # Downloads, compiles, and installs Yosys
+set -xe
 
 YOSYS_VER=0.47
 
@@ -13,3 +14,19 @@ make -j$(nproc)
 make install
 cd /tmp
 rm -r /tmp/yosys
+
+# Perform a sanity check.
+cat > /tmp/sanity.v <<EOF
+module Adder(a, b, z);
+  input  [7:0] a;
+  input  [7:0] b;
+  output [7:0] z;
+  assign z = a + b;
+endmodule
+EOF
+
+yosys <<EOF
+read_verilog /tmp/sanity.v
+hierarchy -check
+opt
+EOF
diff --git a/integration-test/z3.sh b/integration-test/z3.sh
index 86fd566..137d611 100755
--- a/integration-test/z3.sh
+++ b/integration-test/z3.sh
@@ -1,6 +1,7 @@
 #!/bin/bash
 # Installs Z3 into "/usr/local"; this directory has precedence among the default
 # $PATH locations and will shadow the "/usr" installation.
+set -xe
 
 Z3_VER=4.11.2
 
@@ -47,3 +48,15 @@ else
   # There is no appropriate package release, resorting to compilation.
   compile_Z3
 fi
+
+# Perform a sanity check.
+z3 -in -smt2 >/tmp/z3.log <<EOF
+(declare-const a Bool)
+(declare-const b Bool)
+(define-fun demorgan () Bool
+    (= (and a b) (not (or (not a) (not b)))))
+(assert (not demorgan))
+(check-sat)
+EOF
+cat /tmp/z3.log
+grep "unsat" /tmp/z3.log >/dev/null