Interview Questions on Assertions

SystemVerilog
,
15

In reply to Shubhabrata:
You need a first_match. From my SVA book:
2.5.1 first_match operator
Section 2.3.2 addressed the multiple matching of sequences, and explained the consequences of
such matches. For example, the sequence ($rose(a) ##[2:3] b) has two possible matches, and
(rose(a) ##[2:] b) can have an infinite number of matches as that can be decomposed as a
series of threads ORed together. To avoid the possibility of multiple matches that could cause
unexpected errors, or cause an assertion to never succeed because all threads of an antecedent
must be tested for a property to succeed, one could use the first_match(a_sequence) operator.
 Rule: [1] The first_match operator matches only the first of possibly multiple matches for
an evaluation attempt of its operand sequence. This allows all subsequent matches to be
discarded from consideration. This is significant when a sequence is used in the antecedent of an assertion because when a range is used in the antecedent, it can create multiple threads, each triggering the evaluation of the consequent when matched, and all threads must hold for the assertion to hold. This can cause significant performance impacts and possible unexpected errors.
However, applying the first_match operator has significant (positive) effect on the evaluation of
the enclosing sequence. Consider the following example:

ap_never_succeed: assert property(
 ($rose(a) ##[2:$] b) |=> c);
//The assertion ap_never_succeed is equivalent to 
 ap_equivalent_to_ap_never_succeed: assert property(
 ($rose(a) ##2 b)or
 ($rose(a) ##3 b)or
 … 
 ($rose(a) ##n b)|=> c); // where n is infinity

For the ap_equivalent_to_ap_never_succeed assertion to succeed, all threads must succeed, and
there are an infinite number of threads; specifically, these threads include:

($rose(a) ##2 b) |=> c // thread 1
($rose(a) ##3 b) |=> c // thread 2 
 … 
 ($rose(a) ##n b)|=> c // thread n

If any of these threads fails, then the assertion fails; however success cannot be achieved. With the first_match method, only the first match of the sequence is considered, and all other threads are ignored. Thus, in the assertion ap_FM_can_succeed a first match of the antecedent is considered for the evaluation of the consequent.


ap_FM_can_succeed: assert property(
 first_match($rose(a) ##[2:$] b) |=> c);

// Question - If there are two occurrences of sig a rising with state=ACTIVE1, 
// and no sig b occurs between them, then within 3 cycles of the second rise of sig a, START must occur.
    property p1;
       first_match($rose(a) && state == ACTIVE1 ##1 !b[*1:$] ##1 
                   $rose(a) && state == ACTIVE1) |-> [1:3]state == start;
    endproperty
    assert property (p1);

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:
  1. Papers:
    Understanding the SVA Engine,
    Verification Horizons - July 2020 | Verification Academy
    Reflections on Users’ Experiences with SVA, part 1
    Reflections on Users’ Experiences with SVA | Verification Horizons - March 2022 | Verification Academy
    Reflections on Users’ Experiences with SVA, part 2
    Reflections on Users’ Experiences with SVA, Part II | Verification Horizons - July 2022 | Verification Academy
    SUPPORT LOGIC AND THE ALWAYS PROPERTY
    http://systemverilog.us/vf/support_logic_always.pdf
    SVA Alternative for Complex Assertions
    Verification Horizons - March 2018 Issue | Verification Academy
    SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy
    SVA for statistical analysis of a weighted work-conserving prioritized round-robin arbiter.
    https://verificationacademy.com/forums/coverage/sva-statistical-analysis-weighted-work-conserving-prioritized-round-robin-arbiter.
    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/