A SVA question

SystemVerilog
,
1

Hi All,
I’m new to SVA, and I met a simple question.
There’re 2 sigs: req and gnt. when req is true, gnt should respond within [1:3] clock.
I’ve wrote an assertion looks like this:
req |-> ##[1:3] gnt;

but,this assertion cann’t guarantee req and gnt will be a pair. For example,

cyc:|-1-|-2-|-3-|-4-|-5-|-6-|-7-|
req:|-1-|-0-|-1-|-0-|-0-|-0-|-0-|
gnt:|-0-|-0-|-0-|-1-|-0-|-0-|-1-|

in this case,the assertion will be triggerd in cycle 1,and success in cycle 4,but req in cycle 3 will also success in cycle 4,so the assertion success. But my intent is to check req in cycle 1 while gnt in cycle 4, and req in cycle 3 while gnt in cycle 7. In other words, the gnt should only be paired with req only once,req in cycle 3 should consider gnt in cycle 7,not gnt in cycle 4,so the assertion result should be failure. How should I write the assertion?
My English is not very good, i don’t know if I explain it clearly.
Thank you

2

What you’re asking is that each req should have its own corresponding ack.
We all have experienced the following scenario in a bakery or at the paint department in a hardware store. At the store you have one servicing employee and customers come in at different times, often forming a queue. Some customers take a very short time (e.g., they want one bagel, or the item they want is not available – a fail) or they take forever (e.g., wanting many items). So how doe the store handles this? Simple, they have a roll of tickets with incrementing numbers. They also have a board that displays the ticket currently being serviced. A new customer takes a ticket and waits for the store employee who after a service (pass or fail) increments the number on the board and takes on the next customer.
OK, our SVA model will do just that. I have 2 variables: ticket and servicing. In the SVA property, when req==1, the property saves the ticket number, and then increments the ticket for the next attempt of req. The assertion checks for a ack with a servicing number being the same as the ticket that was handed for that attempt. When the assertion terminates (success or failure), the servicing number is incremented.

module reqacq_seq;
    bit req, ack, clk; 
    bit[3:0] ticket, servicing;
    function void inc_ticket(); 
        ticket=ticket + 1'b1; 
    endfunction : inc_ticket
    
    function void inc_servicing(); 
        servicing=servicing + 1'b1; 
    endfunction : inc_servicing
        
    
    property p_reqack; 
        bit[3:0] v_ticket;
        (req, v_ticket=ticket, inc_ticket()) |-> 
             ##[1:3] (ack && servicing==v_ticket);
    endproperty : p_reqack 
    ap_reqack: assert property( @ (posedge clk) p_reqack) inc_servicing();
                                else inc_servicing(); 


endmodule

I did not simulate this code (compiles OK), but it should work.
Please see my latest white paper “Assertions Instead of FSMs/logic for Scoreboarding and Verification”
https://verificationacademy.com/verification-horizons/october-2013-volume-9-issue-3
That paper addresses the application of sequence match items.
Ben Cohen http://www.systemverilog.us/

  • SystemVerilog Assertions Handbook, 3rd Edition, 2013
  • A Pragmatic Approach to VMM Adoption
  • Using PSL/SUGAR … 2nd Edition
  • Real Chip Design and Verification
  • Cmpt Design by Example
  • VHDL books