System verilog assertion question

SystemVerilog
1

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.

2

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 $

3

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

4

In reply to ak_verifsj:

it would move automatically to last condition when B goes low, hence “!B”

5

you can try this
assert property @(posedge clk) $rose(a) |= > b[*c];

6

In reply to saikishorereddy:

for above expression to compile, c has to be a constant.
requirement is c is being supplied from another signal

7

I think, have look at below paper where 1st issue is just like you have.

8

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!