Hi I need some help to solve this assertion question.
Whenever The signal A goes high , from the next cycle the signal B should repeat n no. of times, where n is equal to value of bit[3:0]C when signal A is asserted.
In reply to boopalakrishnan:
property chkr;
int prev_c,cnt;
@(posedge clk)
($rose(A), prev_c = C, cnt =0 ) |=> $rose(B) ##1(B,cnt++)[*1:$] ##1(!B && (cnt == prev_c-1));
endproperty: chkr
setup a testbench here with passing and a failing case:
Edit: it is a safe practice to add [*1:`MAX] instead of $
In reply to ssureshg_:
Hi ssureshg_,
When would this condition change/get satisfied 1(B,cnt++)[*1:$] ? Looks like B should be high for atleast 1 to infinite times, so when would be move to last condition check?
Thanks
you can try this
assert property @(posedge clk) $rose(a) |= > b[*c];
In reply to saikishorereddy:
for above expression to compile, c has to be a constant.
requirement is c is being supplied from another signal
I think, have look at below paper where 1st issue is just like you have.
In reply to ssureshgverifier@gmail.com:
Hi ssureshg,
I’m new to SV assertions. Could you please break down your sequence and explain this part?
@(posedge clk)
($rose(A), prev_c = C, cnt =0 ) |=> rose(B) ##1(B,cnt++)[*1:] ##1(!B && (cnt == prev_c-1));
##1(B,cnt++)[*1:$] ##1(!B && (cnt == prev_c-1)) -----> This part to be specific.
Thanks!