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.

1 files changed, 11 insertions, 0 deletions

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