tristate example

diff --git a/docs/examples/tristate/README.md b/docs/examples/tristate/README.md
new file mode 100644 (file)
index 0000000..155fab2
--- /dev/null
+++ b/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.

diff --git a/docs/examples/tristate/tristate.sby b/docs/examples/tristate/tristate.sby
new file mode 100644 (file)
index 0000000..7970774
--- /dev/null
+++ b/docs/examples/tristate/tristate.sby
@@ -0,0 +1,19 @@
+[tasks]
+pass
+fail
+
+[options]
+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

diff --git a/docs/examples/tristate/tristates.v b/docs/examples/tristate/tristates.v
new file mode 100644 (file)
index 0000000..a6be03e
--- /dev/null
+++ b/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, input wire active2, 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