Assertion in system verilog

SystemVerilog
, ,
1

I wan to do a check like below:

signal ‘A’ and signal ‘B’ both are running in one clk domain .

I wan to check value of signal ‘B’ after 10 consucative assert of signal ‘A’ , 5clk past value of ‘B’ from curren clk cycle…

Ex:
clk : 1 2 3 4 5 6 7 8 9 10 11 12 13
A : 0 0 1 1 1 1 1 1 1 1 1 1 1
B : 0 0 0 0 0 1 1 1 1 0 0 0

mean I wan to check 5 clk cycle past value of ‘B’ on 10th consucatave true of A.

I am doing like below:

A[*10] → $past(B,5)

But it’s not wrking as expected ., can anyone pls suggest correct one?

2

Ex:
clk : 1 2 3 4 5 6 7 8 9 10 11 12 13
A : 0 0 1 1 1 1 1 1 1 1 1 1 1
B :our issue is tah 0 0 0 0 0 1 1 1 1 0 0 0
mean I wan to check 5 clk cycle past value of ‘B’ on 10th consucatave true of A.
I am doing like below:
A[*10] → $past(B,5)
But it’s not working as expected ., can anyone pls suggest correct one?

Your issue is that at every successful attempt of A you start a new assertion thread. You need to restrict the first successful attempt. Thus,

Ex:
clk : 1 2 3 4 5 6 7 8 9 10 11 12 13
A : 0 0 1 1 1 1 1 1 1 1 1 1 1
B : 0 0 0 0 0 1 1 1 1 0 0 0
  $rose(A) ##0 A[*10] |-> $past(B,5)

Ben Cohen http://www.systemverilog.us/

  • SystemVerilog Assertions Handbook, 3rd Edition, 2013
  • A Pragmatic Approach to VMM Adoption
  • Using PSL/SUGAR … 2nd Edition
  • Real Chip Design and Verification
  • Cmpt Design by Example
  • VHDL books
3

In reply to ben@SystemVerilog.us:

But I wan also to slide that window for next subsequent 10 repeatative match for A without any $rose of A .

Will it possible ?

like:
clk: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25
A: 0 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1
B: 0 0 1 1 1 1 1 1 1 1 0 0 0 0 0 0 0 1 1 1 1 1 1 1 0 0

I am expecting comparision starts from clk : 11 and end at 21 continuously , with past 5 clk cycle from current value of B .

4

In reply to skumarsamal:

You need to define your requirements for things like "what happens if A[*10] fails? At what point do you start counting the sequence and exclude the other sequences. An English definition would help you write the assertions. I made some assumptions about your intent, and wrote the following, but you need to refine this code to meet your requirements.

module tenclk;
// $rose(A) ##0 A[*10] |-> $past(B,5) 
// But I wan also to slide that window for next subsequent 10 
// repeatative match for A without any $rose of A.
    bit clk, go=1'b1, A, B; 
    function void set_go();  go=1'b1; endfunction 
    function void reset_go();  go=1'b0; endfunction
    sequence q_ten; @ (posedge clk) (A && go, reset_go()) ##0 (A)[*10]; endsequence 
    
    ap_set_go_if_not_10: assert property(@ (posedge clk) A && go |-> 
              A[*10]) else set_go(); 
    
    ap_AB: assert property(@ (posedge clk) q_10.triggered |-> ($past(B, 5), set_go())); 
    
endmodule
5

In reply to ben@SystemVerilog.us:

the requirement is like below:

Signal A can be high n clk cycles (n :0,1,2…1000000000000000)

after each 10clk cycle A remains high , I wan to check 5 clk cycle past value of B at end of that sequence.

For example :

A is high from 3rd clk to 19 clk

So I wan to check value of B at clk ---- 8th -----------------------after end of 12th clk cycle
Similarly : B at clk -----9th ------------------------------after 13th clk cycle
B at clk -----10th ------------------------------after 14th clk cycle
B at clk -----11th ------------------------------after 15th clk cycle
B at clk -----12th ------------------------------after 16th clk cycle
B at clk -----13th ------------------------------after 17th clk cycle
B at clk -----14th ------------------------------after 18th clk cycle
B at clk -----15th ------------------------------after 19th clk cycle
No check at 16th ------------------------------after 20th clk cycle

Is it clear ?
an it be done like beolw:

property se;
@(posedge clk)
A[*10] |- $past(B,5);
endproperty

6

In reply to skumarsamal:

Your code should work then because at every clocking block you start a new attempt and a separate assertion thread if A==1.

property se;
@(posedge clk)
  A[*10] |-> $past(B,5);
endproperty

Ben Cohen SystemVerilog.us