Endless assertion, any other way to rewrite it?

SystemVerilog
, ,
1

Hi,

I have an assertion in a bus arbiter, I want to check that the input request will be present at the output in less than 18 cycles.

I am using something like this, when there is a request, I store the request in a register. The assertion checks that before 18 cycles I will see an output request with the same address.

This assertion never pass or fail. I wanted to know if another style of coding this assertion could be better, so it could pass.

always_ff @(posedge clk)
if(reg_dr0.wr)
reg_dr0_reg <= reg_dr0;

req_dr0.wr & |(req_dr0.en) |-> ##[0:18] ram_req.wr & ram_req.addr == req_dr0_reg.addr

Regards

2

In reply to jcastillo:
The issue with your approach is that you are not necessarily capturing the value of reg_dr0 at the attempt phase as the if(reg_dr0.wr) may occur again at a later cycle. You really need to understand the concept of independent threads. This is how you fix this:


property p_req18; 
    bit[31:0] v; //  assuming 32 bits
    (req_dr0.wr & |req_dr0.en, v=reg_dr0 )|-> 
        ##[0:18] ram_req.wr && ram_req.addr ==v;
endproperty 
ap_req18: assert property(@ (posedge clk) p_req18);

I strongly suggest that you carefully read my paper
Understanding the SVA Engine
Verification Horizons - July 2020 | Verification Academy
In it I used three different types of SVA properties are used to
emphasize different important concepts of SVA:

  1. Antecedent/consequent: This model demonstrates the concepts of spawned threads,
    leading clocking event, attempts.
  2. Range delays in the consequent: This model demonstrates the testing of each element of the
    range until success is reached and the lack of need to limit the ranges to a matched (i.e., valid) consequent.
  3. Range delays in the antecedent: This model demonstrates the testing of each element of the
    range and the need for a first_match operator or other technique to limit the ranges to a matched antecedent.

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) Amazon.com
  3. Papers: