From 96f64f4788ca64adde55421a6abadefd182d9a1a Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 3 May 2022 13:22:18 +0200 Subject: verific: Fix conditions of SVAs with explicit clocks within procedures For SVAs that have an explicit clock and are contained in a procedure which conditionally executes the assertion, verific expresses this using a mux with one input connected to constant 1 and the other output connected to an SVA_AT. The existing code only handled the case where the first input is connected to 1. This patch also handles the other case. --- tests/sva/nested_clk_else.sv | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100644 tests/sva/nested_clk_else.sv (limited to 'tests') diff --git a/tests/sva/nested_clk_else.sv b/tests/sva/nested_clk_else.sv new file mode 100644 index 000000000..4421cb36a --- /dev/null +++ b/tests/sva/nested_clk_else.sv @@ -0,0 +1,11 @@ +module top (input clk, a, b); + always @(posedge clk) begin + if (a); + else assume property (@(posedge clk) b); + end + +`ifndef FAIL + assume property (@(posedge clk) !a); +`endif + assert property (@(posedge clk) b); +endmodule -- cgit v1.2.3