A grant must at some time have been preceded by a request

SystemVerilog
, , ,
1

I have a simple spec “A grant must at some time have been preceded by a request”

If grant arrives and request never arrives before grant, the assertion fails. Need to look in the past for request, but would not know when request would have arrived.

$past only looks in the ‘past’ a fixed number of clocks. How do you make it look in the past forever?

Thanks much.
Ashok

2

In reply to a72:

You need to latch the occurrence of req. Thus,


    bit clk, req, grnt, req_occurred, reset_n;  

    always @(posedge clk) begin
        if($sampled(req))  req_occurred <= 1'b1; // updated with the $sampled( 
        if($sampled(grnt)) req_occurred <= 1'b0;
    end
   
   ap_grant: assert property(@(posedge clk) $rose(grnt) |-> req_occurred);

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) 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/

3

In reply to ben@SystemVerilog.us:

Thanks, Ben. So, it seems one has to develop ‘satellite’ supporting code to augment the assertion. I understand.

4

In reply to ben@SystemVerilog.us:

Hi Ben,

I think below should work too? eliminating the need for helper code. let me know what you think.

sequence s_req;
rose(req) ##[1:] 1’b1; // endpoints at 0,1,2,… cycles after req
endsequence

grant : assert property (
@(posedge clk)
$rose(gnt) |-> s_req.triggered;
)

5

In reply to DVtrojan:

  • ##[*1:$] req; // is syntactically incorrect
  • You probably meant: ##[1:$] req;
  • You would need a first_match(##[1:$] req)
  • My reservation on this solution is that it is not efficient as it creates at every attempt multiple threads.

Ben

6

In reply to ben@SystemVerilog.us:
had a typo just fixed
sequence s_req;
rose(req) ##[1:] 1’b1; // endpoints at 1,2,… cycles after req
endsequence

7

In reply to DVtrojan:

  • rose(req) ##[1:] 1’b1; // after the 1st req you get an endpoint at every cycle thereafter, till infinity.
  • The 1st attempt with the rose gnt would be OK. However,
  • $rose(gnt) |-> s_req.triggered;
    with any 2nd, 3rd, …nth grant the assertion would would be immediately passed.
    This is because the sequence (rose(req) ##[1:] 1’b1) is causing and endpoint at every cycle after the 1st rose of req
8

In reply to ben@SystemVerilog.us:
$rose(gnt) |-> s_req.triggered;
For the triggered solution to work, use this sequence declaration


sequence s_req;
  @(posedge clk). // updated. 
  first_match($rose(req) ##[1:$] gnt; // ##1 1'b1); // endpoint 1 cycle after gnt
endsequence
// the endpoint of the sequence must end when 
// the $rose(gnt) occurs
// Note: This solution has many threads for each successful attempt

Read my paper Understanding the SVA Engine,
https://verificationacademy.com/verification-horizons/july-2020-volume-16-issue-2

9

In reply to ben@SystemVerilog.us:

Thanks Ben!

10

In reply to DVtrojan:
Glad you liked my reply.
BTW, I made a correction above.
Always verify your assertions, preferably with a simulator.
Ben