projects
/
yosys.git
/ blob
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
history
|
raw
|
HEAD
Add tests for these new models
[yosys.git]
/
tests
/
sva
/
sva_not.sv
1
module top (
2
input clk,
3
input reset,
4
input ping,
5
input [1:0] cfg,
6
output reg pong
7
);
8
reg [2:0] cnt;
9
localparam integer maxdelay = 8;
10
11
always @(posedge clk) begin
12
if (reset) begin
13
cnt <= 0;
14
pong <= 0;
15
end else begin
16
cnt <= cnt - |cnt;
17
pong <= cnt == 1;
18
if (ping) cnt <= 4 + cfg;
19
end
20
end
21
22
assert property (
23
@(posedge clk)
24
disable iff (reset)
25
not (ping ##1 !pong [*maxdelay])
26
);
27
28
`ifndef FAIL
29
assume property (
30
@(posedge clk)
31
not (cnt && ping)
32
);
33
`endif
34
endmodule