Merge pull request #177 from mattvenn/tristate-example

Tristate example

docs/examples/tristate/Makefile

@@ -0,0 +1,3 @@
+SUBDIR=../docs/examples/tristate
+TESTDIR=../../../tests
+include $(TESTDIR)/make/subdir.mk

docs/examples/tristate/README.md

@@ -0,0 +1,13 @@
+# Tristate demo
+
+Run 
+
+    sby -f tristate.sby pass
+
+to run the pass task. This uses the top module that exclusively enables each of the submodules.
+
+Run 
+
+    sby -f tristate.sby fail
+
+to run the fail task. This uses the top module that allows submodule to independently enable its tristate outputs.

docs/examples/tristate/tristate.sby

@@ -0,0 +1,20 @@
+[tasks]
+pass
+fail
+
+[options]
+fail: expect fail
+mode prove
+depth 5
+
+[engines]
+smtbmc
+
+[script]
+read -sv tristates.v
+pass: prep -top top_pass
+fail: prep -top top_fail
+flatten; tribuf -formal
+
+[files]
+tristates.v

docs/examples/tristate/tristates.v

@@ -0,0 +1,18 @@
+`default_nettype none
+module module1 (input wire active, output wire tri_out);
+    assign tri_out = active ? 1'b0 : 1'bz;
+endmodule
+
+module module2 (input wire active, output wire tri_out);
+    assign tri_out = active ? 1'b0 : 1'bz;
+endmodule
+
+module top_pass (input wire clk, input wire active1, output wire out);
+    module1 module1 (.active(active1), .tri_out(out));
+    module2 module2 (.active(!active1), .tri_out(out));
+endmodule
+
+module top_fail (input wire clk, input wire active1, input wire active2, output wire out);
+    module1 module1 (.active(active1), .tri_out(out));
+    module2 module2 (.active(active2), .tri_out(out));
+endmodule