From 523b7a252e654c2121a0734cd03c84d30accc21b Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 2 Aug 2022 20:22:27 +0200 Subject: [PATCH] Regression test for YosysHQ/yosys#3433 --- tests/regression/smt_dynamic_index_assign.sby | 22 +++++++++++++++++++ 1 file changed, 22 insertions(+) create mode 100644 tests/regression/smt_dynamic_index_assign.sby diff --git a/tests/regression/smt_dynamic_index_assign.sby b/tests/regression/smt_dynamic_index_assign.sby new file mode 100644 index 0000000..993d75a --- /dev/null +++ b/tests/regression/smt_dynamic_index_assign.sby @@ -0,0 +1,22 @@ +[options] +mode cover +depth 36 + +[engines] +smtbmc boolector + +[script] +read -formal top.sv +prep -top top + +[file top.sv] +module top(input clk); + reg [33:0] bits = 0; + reg [5:0] counter = 0; + + always @(posedge clk) begin + counter <= counter + 1; + bits[counter] <= 1; + cover (&bits); + end +endmodule