From e01ac8b84855aa7581d40a69d15c42d1432a8432 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Wed, 29 Jun 2022 16:43:07 +0200 Subject: [PATCH] tests: Test for invalid x-value FF init optimizations --- tests/regression/ff_xinit_opt.sby | 39 +++++++++++++++++++++++++++++++ 1 file changed, 39 insertions(+) create mode 100644 tests/regression/ff_xinit_opt.sby diff --git a/tests/regression/ff_xinit_opt.sby b/tests/regression/ff_xinit_opt.sby new file mode 100644 index 0000000..2078ad1 --- /dev/null +++ b/tests/regression/ff_xinit_opt.sby @@ -0,0 +1,39 @@ +[options] +mode bmc + +[engines] +smtbmc boolector + +[script] +read_verilog -formal ff_xinit_opt.sv +prep -flatten -top top + +opt -fast -keepdc + +[file ff_xinit_opt.sv] +module top( + input clk, + input [7:0] d +); + + (* keep *) + wire [7:0] some_const = $anyconst; + + wire [7:0] q1; + wire [7:0] q2; + + ff ff1(.clk(clk), .d(q1), .q(q1)); + ff ff2(.clk(1'b0), .d(d), .q(q2)); + + initial assume (some_const == q1); + initial assume (some_const == q2); + initial assume (q1 != 0); + initial assume (q2 != 0); + + always @(posedge clk) assert(some_const == q1); + always @(posedge clk) assert(some_const == q2); +endmodule + +module ff(input clk, input [7:0] d, (* keep *) output reg [7:0] q); + always @(posedge clk) q <= d; +endmodule -- 2.30.2