Add sanity checks for z3, yosys, and sby installations

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

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

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