How to write the assertion that between two requests grant should be there

SystemVerilog
1

Hi ,

could you please help on how to write an assertion such that between two requests there should be one grant. I have written the following. could you please conform whether it is correct.


 assert property(@ (posedge clk) 
  $rose(req) |-> !req[*1:$] ##1 grant && req==0 );
2

In reply to srbeeram:


// One mistake: 
$rose(req) |-> !req[*1:$]
// at the $rose(req) req==1, thus with the |-> the req cannot be ==0 in the same cycle. 
// you meant 
$rose(req) |-> strong(##1 !req[*1:$]  ##1 grant && req==0) ); // OK 
// says, at rose of req, no req until grant && req==0 
//
// This can also be expressed as
$rose(req) |-> strong( ##1 req[->1] intersect ##1 grant && !req[->1])  0;

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home.html
** 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:
3

In reply to ben@SystemVerilog.us:

Thanks Ben for the providing the clarifications.

4

In reply to ben@SystemVerilog.us:

Can we write this assertion like below.


property req_gnt_chk
@(posedge clk)
$rose(req) |=> (!req until_with grant);
endproperty

req_gnt : assert property (req_gnt_chk);

Thanks,
Harsh

5

In reply to harsh pandya:
yes, this is another approach. It’s really how one sees it, and they are ALL OK.

  • The (!req until_with grant); is more English-like, but you have to mentally visualize the meaning of the waveform or review the meaning of this property.
  • The req[->1] intersect ##1 grant && !req[->1] is more waveform style where you
    visualize 2 signals and see when to evaluate a gated signal.
  • The **(##1 !req[*1:$] ##1 grant && req==0)**is more stream-like where you have a stream of possible scenarios.

One may argue at my visualization approach, but this is how I see it. Having worked a lot with waveforms and hardware, I tend to avoid the English-like approaches, but this is me.
Ben

6

In reply to ben@SystemVerilog.us:

I agree with your point.
It’s more easy compared to English-like, when we comparing with waves.

Thanks,
Harsh