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

Question

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

Answer 1

Solution

ben@SystemVerilog.us

Full Access

2442 posts

February 07, 2022 at 10:41 am

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/
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
...
1) SVA Package: Dynamic and range delays and repeats https://rb.gy/a89jlh
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:
- Understanding the SVA Engine,
https://verificationacademy.com/verification-horizons/july-2020-volume-16-issue-2
- SVA Alternative for Complex Assertions
https://verificationacademy.com/news/verification-horizons-march-2018-issue
- SVA in a UVM Class-based Environment
https://verificationacademy.com/verification-horizons/february-2013-volume-9-issue-1/SVA-in-a-UVM-Class-based-Environment

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/

Answer 2

a72

Full Access

28 posts

February 07, 2022 at 10:58 am

In reply to ben@SystemVerilog.us:

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

Answer 3

DVtrojan

Full Access

7 posts

May 27, 2022 at 12:40 pm

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

Answer 4

ben@SystemVerilog.us

Full Access

2442 posts

May 27, 2022 at 2:29 pm

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

Answer 5

DVtrojan

Full Access

7 posts

May 27, 2022 at 2:54 pm

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

Answer 6

ben@SystemVerilog.us

Full Access

2442 posts

May 27, 2022 at 3:32 pm

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

Answer 7

ben@SystemVerilog.us

Full Access

2442 posts

May 28, 2022 at 7:48 am

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

Answer 8

DVtrojan

Full Access

7 posts

May 28, 2022 at 1:41 pm

In reply to ben@SystemVerilog.us:

Thanks Ben!

Answer 9

ben@SystemVerilog.us

Full Access

2442 posts

May 28, 2022 at 10:56 pm

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

Languages & Standards

Methodologies

Techniques & Tools

Universal Verification Methodology (UVM)

Featured Courses

Additional Courses

Formal-Based Techniques

Analog/Mixed Signal

UVM Forum

SystemVerilog Forum

Coverage Forum

Additional Forums

Implementation Patterns

Specification Patterns

Pattern Resources

UVM Cookbook

Coding Guidelines & Deployment

Coverage Cookbook

Featured & On-Demand

On-Demand Library

Recording Archive

Conferences & WRG

Siemens EDA Learning Center

Blog & News

Verification Horizons Publication

About Us

Training

Solution

Portfolio

Explore

Siemens

Contact