SV assertion query

Hi,

I am trying to write assertion for the following requirement,
When req is asserted, ack should follow within 10 cycles and ack should go low next clock cycle and stay low for the rest of the time


property p1;
@(posedge clk) disable iff (!rst_n)
$rose(req)|->##[1:10]ack ##1 (~ack)##0 (~ack)[*1:$];

Will this work?

In reply to svq:
2 options


module m;
  bit req, ack, clk, rst_n=1; 
  a_p1: assert property(
    @(posedge clk) disable iff (!rst_n)
    $rose(req)|->##[1:10]ack ##1 !ack[*1:$]); 

  // using the followed-by sequence follwed-by property 
  a_p2: assert property(
    @(posedge clk) disable iff (!rst_n)
    $rose(req)|->##[1:10]ack #=# always @(posedge clk) !ack);
    
endmodule 

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
  2. Free books: Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
    Real Chip Design and Verification Using Verilog and VHDL($3) Amazon.com
  3. Papers:

Udemy courses by Srinivasan Venkataramanan (http://cvcblr.com/home.html)
https://www.udemy.com/course/sva-basic/
https://www.udemy.com/course/sv-pre-uvm/

In reply to ben@SystemVerilog.us:

Thank you Ben for the quick response. Will there be any scenario expression[*0:] will be useful? It should always be expression[*1:] right?

In reply to svq:
I am giving you 2 pages from my SVA book that explains the [*0
It explains lots of things.


Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
  2. Free books: Component Design by Example https://rb.gy/9tcbhl
    Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
  3. Papers:

Udemy courses by Srinivasan Venkataramanan (http://cvcblr.com/home.html)
https://www.udemy.com/course/sva-basic/
https://www.udemy.com/course/sv-pre-uvm/

In reply to ben@SystemVerilog.us:

Thanks Ben. This is very helpful.
According to this, “Assertion of this property terminates, when antecedent matches and one of the consequent threads match”. In that case, technically below assertion will terminate if ack stays low for 1 or 2 or 3 or 4… cycles right. How does it make sure that ack stays low for rest of the simulation. Example: A scenario where ack stayed low for 2 cycles, and then went high in 3rd cycle. But assertion would have terminated. Is it because there is no expression after !ack[*1:] in this case?


    $rose(req)|->##[1:10]ack ##1 !ack[*1:$]); 

In reply to svq:
You are correct, my apologies. What you need is the always property
From my book:


// after the ack, you always after every cycle need the !ack 
  a_p2: assert property(
    @(posedge clk) disable iff (!rst_n)
    $rose(req)|->##[1:10]ack #=# always @(posedge clk) !ack);


http://systemverilog.us/vf/ackalways.sv

Thanks for the explanation . This makes sense. Last question, is it all right to use |=> in place of #=# ?

In reply to ben@SystemVerilog.us:

Hi,Ben.
I was wondering if it is possible to replace

always @(posedge clk) !ack

with

always !ack

In reply to svq:

Thanks for the explanation . This makes sense. Last question, is it all right to use |=> in place of #=# ?


// You are suggesting changing this: 
$rose(req)|->##[1:10]ack #=# always @(posedge clk) !ack);

// To
$rose(req)|->##[1:10]ack |=>  always @(posedge clk) !ack);
// The issues here are VACUITY and meeting requirements
// If ack==0 for all 10 cycles, then the assertion is vacuously true.

The followed-by operator in the consequent concatenates a sequence and a property.
In this example, if ack==0 for all 10 cycles then the assertion fails.

In reply to Yuankun:
The reason I initially used the always @(posedge clk) !ack is because I was not sure without doing some 1800 research of the clock flows through from the sequence to the property, so I took the safe mode.
Many many years ago, when I was learning VHDL, I had lots of syntax/legality questions. Finally, my mentor got fed up with me and said the following:

If you are in doubt about what is legal or illegal, write a test code and simulate it.
I can assure you, the simulator tool knows the LRM much better than you.
:)

Here, I followed that advice instead of digging into 1800, and the answer is YES.
The clock does flow through from the sequence to the followed-by property


$rose(req)|->##[1:10]ack #=# always !ack); // WORKS OK, IS LRGAL

In reply to ben@SystemVerilog.us:

Thanks Ben for your kind reply.

In reply to ben@SystemVerilog.us:

Hi Ben,

Will the above solutions work if requests come in back to back. In the case of back to back requests, the $rose will not fire for the 2nd request, correct ?

In reply to DVJoe:

In reply to ben@SystemVerilog.us:
Hi Ben,
Will the above solutions work if requests come in back to back. In the case of back to back requests, the $rose will not fire for the 2nd request, correct ?

At every clocking event there is an attempt at the assertion.
See my paper Understanding the SVA Engine,
https://verificationacademy.com/verification-horizons/july-2020-volume-16-issue-2

If signal “a” is the sequence 0 0 1 1 1 0 1 1
All attempts where a==0 are vacuous.
In the above sequence you have 2 $rose(a) and with each of them a successful attempt.

In reply to ben@SystemVerilog.us:

Hi Ben,

I went through the paper that you mentioned above. Thanks for the detailed explanation on what happens underneath the hood for multiple threads.

I do want to specifically bring up the last 2 examples that you specified in this paper :

(1) first_match operator :
first_match(rose(a) ##[1:] b) |-> ##3 c;

(2) Goto operator
$rose(a) ##1 b[->1]) |-> ##3 c; // Use the goto operator

I want to explore the use of the above for this simple case : “Write an assertion for a transaction where a request is followed by an ack in 1-3 cycles”. Now if I use the same style solution as above :

$rose(req)|->##[1:3]ack

If my requests on each posedge are in the order you specified :

Posedge# Req Ack Comment
Posedge0 0 0
Posedge1 1 0 Request#1
Posedge2 1 0 Request#2
Posedge3 1 1 Request#3 and Ack for Req #1. But this ack will satisfy #Request2 too !!!.. How do you filter this out ? Using the first_match operator ?
Posedge4 0 1 Ack for Req #2
Posedge5 1 1 Ack for Req #3
Posedge6 1 1 Ack for Req #4
Posedge7 0 1 Ack for Req #5

My concern again is that the above assertion will fire for the 1st posedge and 5th posedge only and won’t fire for the other requests.

Now, if I were to rewrite this assertion as follows : Level sensitive ( not really ideal because of performance issues)

req |-> ##[1:3]ack

Here, I would fire a thread each time request was high, but then if you look at posedge #3, how do I avoid NOT counting the ack for request#1 towards request #2 ? Do I use the first_match operator here ? Should I rewrite it like this :

first_match(req |-> ##[1:3]ack)

Can you please clarify ? Sorry if this has already been addressed in other threads in this forum. I did search to see if I could find a similar discussion, but I could not find it.

In reply to DVJoe:

See my solution at
https://verificationacademy.com/forums/systemverilog/assertion-req-and-gnt-signals

In reply to ben@SystemVerilog.us:

Thanks Ben. That one nails it. I am so frustrated that this solution ( using the power of a local variable) eluded me this past week. But this solution you mentioned -

@(posedge clk) ($rose(req), v_serving_ticket=ticket, inc_ticket()) |->
##[1:10] now_serving==v_serving_ticket ##0 ack;

It does open up a new concept for me - that I can bundle up function calls in an antecedent too… I never thought we could do this. But now that I see it, it of course makes sense.