Checkers in Formal Verification - SVA: The Power of Assertions in SystemVerilog - page 520

checker check_latency(en, data_ready, max_latency,

1

event clk = $inferred_clock,

2

untyped rst = $inferred_disable);

3

default clocking @clk; endclocking

4

default disable iff rst;

5

6
7

let ub(x) = $clog2(x + 1) - 1;

let nstages = $bits(en) + 1;

8

let stage_ub = ub(nstages);

9

let big_latency = max_latency + 1;

10

let latency_ub = ub(big_latency);

11

12
13

rand bit start;

bit [stage_ub:0] stage = '0;

14

bit [latency_ub:0] latency = '0;

15

16
17

bit go;

assign go = data_ready && start;

18

19
20

function type (stage) next_stage;

if (rst) return 0;

21

if (stage == 0 && go) return 1;

22

if (stage != 0 && stage != nstages && en[stage])

23

return stage + 1;

24

return stage;

25

endfunction : next_stage

26

27
28

function type (latency) next_latency;

if (rst || latency == 0 && !go) return 0;

29

if (latency == big_latency) return big_latency;

30

return latency + 1;

31

endfunction : next_latency

32

33
34

always @clk begin

stage <= next_stage();

35

latency <= next_latency();

36

end

37

38
39

a1: assert property (

$rose(stage == nstages) -> latency != big_latency);

40

endchecker : check_latency

41

Fig. 23.1 Checking pipeline latency

1. start is low at both clock ticks 10 and 20.
2. start is low at clock tick 10 and high at clock tick 20.
3. start is high at clock tick 10 and low at clock tick 20.
4. start is high at both clock ticks 10 and 20.
In the first, we never start counting and do not check anything; in the second,
we check only the transaction starting at clock tick 20; in the third, we check only