From: Matt Venn Date: Mon, 13 Jun 2022 11:51:04 +0000 (+0200) Subject: tristate example X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b42b6445b8641700e9538aa6df8c5c5297328698;p=SymbiYosys.git tristate example --- 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