Assertion to check valid |-> 8 clks rsp

SystemVerilog
,
1

Hi,

I trying to write assertion to check that if valid is high, rsp should be high only after 8 clks. Valid can be high on consecutive clks and hence rsp should be high on consecutive clks as well.

**My question is if we were to implement the logic to drive rsp, we would use fork-join and call automatic task since this is pipelined process. Does assertion take care of this if it does how does that work? Is there a new assertion triggered every-time valid==1 and separate memory is allocated to check that assertion?


clks 0 1 2 3 4 5 6 7 8 9 10
     v v             r r 



assert property p1;

property p1;
   @(posedge clk) (valid==1) |-> rsp==0[*7] ##1 rsp==1;
endproperty
2

In reply to UVM_SV_101:

Yes, an assertion takes care of this by creating a new thread for every attempt, each with its own set of local variables and state information.

Your property will not work because rsp is not necessarily 0 for the 8 cycle duration. You would have to do

property p1;
   bit v;
   @(posedge clk) (1,v=valid) ##8 rsp==v;
endproperty

After 8 cycles, there would be 8 threads, each with their own local copy of v.

3

In reply to UVM_SV_101:

Your assertion is almost correct. Should be

 @(posedge clk) (valid==1) |=> rsp==0[*7] ##1 rsp==1;

At E every clocking event (the @(posedge clk) the property of the assertion is triggered independently from any other triggered assertions and has a life of its own.

I posted on LinkedIn An anecdote: is SVA a soap pipe?

At every blow event of a soap pipe, a bubble property is emitted. That bubble has a life of its own. It begins to spin, examining its initial states and composition, and then has several outcomes:

· It could disappear as if this bubble property was totally meaningless and vacuous.

· It could split and issue a new property bubble, and this process can repeat itself multiple times. Each of these new bubbles then has a life of its own.

. One or more of these split bubbles could be seen shining with glow and happiness as if it succeeded, or it can come down in a flash crashing miserably into failure.

Note: I describe this analogy to SVA assertions as a response to questions I see at the https://verificationacademy.com/forums/systemverilog where many users fail to understand the SVA inner model on how properties are handles starting from the clocking event.

Actually, to better understand the SVA model, I encourage you to read my paper Understanding the SVA Engine,

Verification Horizons - July 2020 | Verification Academy

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr
** 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:
4

In reply to ben@SystemVerilog.us:

Ben, your assertion does not take care of the overlapping responses.

5

In reply to dave_59:

Oops! You’re correct, my error.
A simple sequence like the one you have shown is good.
Thanks,
Ben systemverilog.us

6

In reply to dave_59:

In reply to UVM_SV_101:
Yes, an assertion takes care of this by creating a new thread for every attempt, each with its own set of local variables and state information.
Your property will not work because rsp is not necessarily 0 for the 8 cycle duration. You would have to do

property p1;
bit v;
@(posedge clk) (1,v=valid) ##8 rsp==v;
endproperty

After 8 cycles, there would be 8 threads, each with their own local copy of v.

Hi Dave,

According to logic there would be new thread every posedge of clk? Wouldnt that affect the performance?

Is there a way to put condition on it?

EDIT::
Oh never mind, that assertion takes care of valid==0, rsp==0 as well.

7

In reply to UVM_SV_101:

See my last reply at
https://verificationacademy.com/forums/systemverilog/assertion-req-and-gnt-signals
Ben systemverilog.us

8

In reply to ben@SystemVerilog.us:

Hi Ben/Dave,

I have a question on the above assertion. I simulated it and i see the assertion passes at 170ns.I see the first detection of valid =1 happens at 30ns and then after 8 clock cycles inclusive, i dont see the rsp becoming one after 8 cycles and i still see the assertion passed. Can you help me tell why the assertion passed at 170ns?

here is the code

9

In reply to rag123:
The assertion looks ok and it is a good solution.
The confusion may be in the way you read the waveforms.


// stimulus 
@(posedge clk) #1;  
     if (!randomize(valid,rsp)
// valid is sampled in the Preponed region of @(posedge clk) 
// From the waveform you when you see valid gong to a 1'b1, it is after 1 ns 
// but regardless of that, the sampling of valid is zero not a one.

Ben SystemVerilog.us

10

In reply to ben@SystemVerilog.us:

If you want vacuity when valid==0, you can use this definition of a property


property_statement ::=
property_expr ;
  if ( expression_or_dist ) property_expr
  [ else property_expr ]

ap2: assert property( @(posedge clk) if(!valid) 0 |-> 1 // vacuity because of the 0 
                                         else  ##8  rsp);

Ben SystemVerilog.us

11

In reply to dave_59:

In reply to ben@SystemVerilog.us:
Ben, your assertion does not take care of the overlapping responses.

This solution has no overlapping issue. .
@(posedge clk) (valid==1) |-> ##8 rsp==1;
BTW this is identical to the the property with the “if” clause
Ben systemverilog.us