Concurrent Assertion :: To check the No. of Occurrence of ' ack ' within certain clocks

SystemVerilog
,
6

In reply to hisingh:
on #1:


ack[=1] intersect 1[*5]; would be the same as those five options 
!ack[*0] ##1 ack ##1 !ack[*4] or  // same as:  ack ##1 !ack[*4]
!ack[*1] ##1 ack ##1 !ack[*3] or
!ack[*2] ##1 ack ##1 !ack[*2] or
!ack[*3] ##1 ack ##1 !ack[*1] or
!ack[*4] ##1 ack ##1 !ack[*0] // Same as: !ack[*4] ##1 ack

(2) Is the above solution an alternative to your unique solution in :: Uniq_Ack
NO. What happens is the antecedent is a match in cycle 1, 2, 3 and ack is true in cycle 5?
The assertion for those 3 attempts would pass in t5.
The uniqueness thing that you are referring in the link checks that if you have an ack, there was only a single request for it, ulike have 3 requests satisfied by a single ack


// code from the link
always @(posedge clk) begin
        if(req && !ack)  req_count <= req_count + 1; // was if(req) ... * 1'b1
        if(ack && !req)  req_count <= req_count - 1; // was if(ack) ... - 1'b1
    end

    sequence s_req; @(posedge clk) $rose(req)  ##[0:5] 1'b1; endsequence // endpoints at 0, 1, ..5 cycles after req

    ap_ack2req: assert property(@(posedge clk) $rose(ack) |-> req_count > 0 && s_req.triggered);

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** 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:

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/