0
votes

This was my first naive attempt. Basically vld can go high anytime in the 20 cycles. But the first time it goes high, data needs to be a specific value, say 'h20.

sequence correct_vld_and_data;
    ##[1:20] vld
    ##0 (data == 'h20);
endsequence

property prop_correct_vld_and_data;
    @(posedge clk)
        (precondition_met) 
        -> 
        (correct_vld_and_data);
endproperty

assert prop_correct_vld_and_data;

The problem is, above sequence matches for the following case; but I don't want it to match, meaning I do want the assertion error to fire:

t=0    : precondition_met==1
t=1-4  : vld==0
t=5    : vld==1 data=='h5
t=6-9  : vld==0
t=10   : vld==1 data=='h20
t=11-20: vld==0

The first time that vld goes high, I need data=='h20 and not 'h5 like it is this case.

1

1 Answers

0
votes

I think you should use then the first match_operator like this : (precondition_met) ##0 first_match(##[1:20] vld) |-> data == 'h20

Because in your example it has two matches : the first one when data=='h5 the second one when data=='h20