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
|