From b42b6445b8641700e9538aa6df8c5c5297328698 Mon Sep 17 00:00:00 2001
From: Matt Venn <matt@mattvenn.net>
Date: Mon, 13 Jun 2022 13:51:04 +0200
Subject: [PATCH] tristate example

---
 docs/examples/tristate/README.md    | 13 +++++++++++++
 docs/examples/tristate/tristate.sby | 19 +++++++++++++++++++
 docs/examples/tristate/tristates.v  | 18 ++++++++++++++++++
 3 files changed, 50 insertions(+)
 create mode 100644 docs/examples/tristate/README.md
 create mode 100644 docs/examples/tristate/tristate.sby
 create mode 100644 docs/examples/tristate/tristates.v

diff --git a/docs/examples/tristate/README.md b/docs/examples/tristate/README.md
new file mode 100644
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
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
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
-- 
2.30.2