From bc8ab3ab44f58fc126b103f4a28dd9f6ec3fd90b Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Thu, 15 Feb 2018 15:26:37 +0100 Subject: Fix verific PRIM_SVA_AT handling in properties with PRIM_SVA_DISABLE_IFF --- tests/sva/sva_not.sv | 34 ++++++++++++++++++++++++++++++++++ 1 file changed, 34 insertions(+) create mode 100644 tests/sva/sva_not.sv (limited to 'tests/sva') 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 -- cgit v1.2.3