Fix verific PRIM_SVA_AT handling in properties with PRIM_SVA_DISABLE_IFF

diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 09c379f1906311871f97205b535cadbda43c67f3..fa0db1f56feaf7186cf422ed4565da4bf0c6a730 100644 (file)
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -1350,7 +1350,7 @@ struct VerificSvaPP
                        return default_net;
                }
 
-               if (inst->Type() == PRIM_SVA_AT) {
+               if (inst->Type() == PRIM_SVA_AT || inst->Type() == PRIM_SVA_DISABLE_IFF) {
                        Net *new_net = rewrite(get_ast_input2(inst));
                        if (new_net) {
                                inst->Disconnect(inst->View()->GetInput2());

diff --git a/tests/sva/sva_not.sv b/tests/sva/sva_not.sv
new file mode 100644 (file)
index 0000000..d81a486
--- /dev/null
+++ b/tests/sva/sva_not.sv
@@ -0,0 +1,34 @@
+module top (
+       input clk,
+       input reset,
+       input ping,
+       input [1:0] cfg,
+       output reg pong
+);
+       reg [2:0] cnt;
+       localparam integer maxdelay = 8;
+
+       always @(posedge clk) begin
+               if (reset) begin
+                       cnt <= 0;
+                       pong <= 0;
+               end else begin
+                       cnt <= cnt - |cnt;
+                       pong <= cnt == 1;
+                       if (ping) cnt <= 4 + cfg;
+               end
+       end
+
+       assert property (
+               @(posedge clk)
+               disable iff (reset)
+               not (ping ##1 !pong [*maxdelay])
+       );
+
+`ifndef FAIL
+       assume property (
+               @(posedge clk)
+               not (cnt && ping)
+       );
+`endif
+endmodule