From b42b6445b8641700e9538aa6df8c5c5297328698 Mon Sep 17 00:00:00 2001 From: Matt Venn Date: Mon, 13 Jun 2022 13:51:04 +0200 Subject: [PATCH 1/4] 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 From 7efabe828abdd1cf447cbd39cde0c4b16200a93a Mon Sep 17 00:00:00 2001 From: Matt Venn Date: Mon, 13 Jun 2022 13:59:12 +0200 Subject: [PATCH 2/4] expect fail --- docs/examples/tristate/tristate.sby | 1 + 1 file changed, 1 insertion(+) diff --git a/docs/examples/tristate/tristate.sby b/docs/examples/tristate/tristate.sby index 7970774..f85e937 100644 --- a/docs/examples/tristate/tristate.sby +++ b/docs/examples/tristate/tristate.sby @@ -3,6 +3,7 @@ pass fail [options] +fail: expect fail mode prove depth 5 From 687ee0f011289b4f7eced050ca216720ec3ddc0c Mon Sep 17 00:00:00 2001 From: Matt Venn Date: Mon, 13 Jun 2022 14:00:08 +0200 Subject: [PATCH 3/4] remove unused module port --- docs/examples/tristate/tristates.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/examples/tristate/tristates.v b/docs/examples/tristate/tristates.v index a6be03e..a41ffc2 100644 --- a/docs/examples/tristate/tristates.v +++ b/docs/examples/tristate/tristates.v @@ -7,7 +7,7 @@ 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); +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 From b88d7a13fb6b62ba77cfb90c3e0c34a79e3d4245 Mon Sep 17 00:00:00 2001 From: Matt Venn Date: Tue, 14 Jun 2022 15:35:22 +0200 Subject: [PATCH 4/4] add makefile for test --- docs/examples/tristate/Makefile | 3 +++ 1 file changed, 3 insertions(+) create mode 100644 docs/examples/tristate/Makefile diff --git a/docs/examples/tristate/Makefile b/docs/examples/tristate/Makefile new file mode 100644 index 0000000..1173566 --- /dev/null +++ b/docs/examples/tristate/Makefile @@ -0,0 +1,3 @@ +SUBDIR=../docs/examples/tristate +TESTDIR=../../../tests +include $(TESTDIR)/make/subdir.mk