summaryrefslogtreecommitdiff
path: root/tests/sva/sva_not.sv
blob: d81a48653aabeca34103f38693523364a0cac786 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
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