Concurrent assertion for state coverage

SystemVerilog
, , ,
2

In reply to ak180:
There are several concepts that seem to have missed, and you should have been taught those when you studied SVA. I strongly recommend that you thoughroughly read my paper

  1. Delay range: A delay range, such as ##[n:m], indicates that the delay between the first sequence and the next ranges from nth cycle up to either a maximum mth cycles. For example, the sequence (a ##[3:4] b ##1 c) is equivalent to the sequence ((a ##3 b ##1 c) or (a ##4 b ##1 c)). This example represents two sequence threads, and thus multiple possible matches are possible (2 in this case because the range is 2) .
  2. Range delays in the antecedent
    Consider the following property: $rose(a) ##[1:5] b |-> ##3 c;
    It states that at each end point of the sequence ($rose(a) ##[1:5] b) the variable “c” will be true three cycles later.
    The issue that arises with many users is that the antecedent is multithreaded, and that can causes unanticipated errors. SVA requires that each of the threads of that antecedent with a range or a repeat statement, must be tested with its appropriate consequent
    Specifically, the property rose(a) ##[1:] b |-> ##3 c; is equivalent to ($rose(a) ##[1] b) or ($rose(a) ##[2] b) or …(rose(a) ##[] b) |-> ##3 c; // where $ is infinity
    This ORing in the antecedent creates multiple threads, something like:
    ($rose(a) ##[1] b |-> ##3 c) and // separate thread
    ($rose(a) ##[2] b |-> ##3 c) and // separate thread
    …
    (rose(a) ##[] b |-> ##3 c);//
    This property can never succeed because for success ALL THREADS OF THE ANTECEDENT MUST BE TEST. Property CAN FAIL TOUGH!
    Note: Any non-matched thread of the antecedent (when b==0) creates a vacuously true property result for that thread, meaning that though TRUE, it is of no significance. However, any failure of one of those property threads (Antecedent through consequent) causes the assertion to fail. That would occur if one of the treads of the antecedent is a match and its corresponding consequent is not a match (when c==0). For the property to success, there can be no property failure (vacuity is considered a vacuous true), and at least one thread of the antecedent matches along with a match of its corresponding consequent.
  3. Ranges in repeats have the “or”: Same principles apply to the repeats on ranges.
    a[1:$] is equivalent to*a{*1] or a[2] or … a[n].
  4. Attempt: At every clocking event there is an attempt. With
    *@(posedge clk) (state == FSM_SAMPLE) [1:$] |=>
    you are creating at every clocking event an unnecessary infinite number of “or” threads.
  5. Use of multiple properties each with an antecedent: Do you realize that each non matched antecedent causes that property to be vacuous?
 seq1 |-> seq2 |-> seq3  |-> seq4
<---property->
<----- property ------>
<------------property -------->
  1. property coverage: What you are looking for is really a sequence coverage for the states of the FSM. Thus, use
property prop_fsm_normal_operation;
disable iff (!reset_n)
@(posedge clk) $rose(state == FSM_SAMPLE) ##1 (state == FSM_STREAM) [*1:$]
##1 (state == FSM_WAIT) [*1:$] ##1 (state == FSM_IDLE);
endproperty
cp_fsm: cover property (prop_fsm_normal_operation);

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 - SystemVerilog - Verification Academy
  2. Free books: Component Design by Example https://rb.gy/9tcbhl
    Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
  3. Papers: