From bc8ab3ab44f58fc126b103f4a28dd9f6ec3fd90b Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Thu, 15 Feb 2018 15:26:37 +0100
Subject: [PATCH] Fix verific PRIM_SVA_AT handling in properties with
 PRIM_SVA_DISABLE_IFF

---
 frontends/verific/verific.cc |  2 +-
 tests/sva/sva_not.sv         | 34 ++++++++++++++++++++++++++++++++++
 2 files changed, 35 insertions(+), 1 deletion(-)
 create mode 100644 tests/sva/sva_not.sv

diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 09c379f19..fa0db1f56 100644
--- 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
index 000000000..d81a48653
--- /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
-- 
2.30.2