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

In reply to ben@SystemVerilog.us:

Ben ,

Thanks for the explanation .
Without the cover property the assertion works as intended .

Added another assertion as per Ack_should_be_preceded_with_request to throw errors for extra ’ ack ’ violations .

Have a few follow up questions ::

(1) The reason I added cover property is to ensure vacuous pass reports are not shown via assert property

[Q1] How is that if $rose( rdy ) is False there is No Vacuous pass report via ’ assert property ’ ?
Also will the assignment N subroutine call occur ONLY when $rose( rdy ) has Non - vacuous pass ?

(2) I was referring to SV LRM 2017 , Section 16.11 , Syntax 16-15


  sequence_expr ::= // from A.2.10
   ...
   | ( sequence_expr {,  sequence_match_item} )  [ sequence_abbrev ]
   ...
   sequence_match_item ::=
       operator_assignment
     | inc_or_dec_expression
     | subroutine_call
 

The antecedent has 3 parts in your solution .

(a)  Sequence  Expression  ::  $rose( rdy ) 

(b)  Assignment 

(c)  Subroutine  call . 

I also notice that instead of the subroutine call , if I were to write the increment as 3rd part I get compilation error .

[Q2] Is the order fixed i.e assignment should be written before subroutine call ? . Can we have more than 3 parts too ?

     I  have  seen  codes  with  multiple  assignments  ::

 sequence dataCheck ;
   int  ldata1 , ldata2 ;

   ( rdc , ldata1 = rData , ldata2 = retryData ) ##5 .... 
   
    //  ' rdc '  is  another  sequence .  
 endsequence
 

[Q3] This was an application of a subroutine call from an expression .
What other cases can we use the subroutine for ?

The book I am currently referring ( by Ashok Mehta ) has codes using it for debugging purposes ( To display reports )
and also hints that it could be used to collect coverage information too .