Fail problem

SystemVerilog
1

Hi All,
$rose(a) |=> (~a[*1:10]) intersect (b[->1] ##1 !b) is used in waveform


|  |  |  |  |  |  |  |  |  |           (clk rising_edge) 

_  -  _  -  _  _  _  _  _  _           (signal a)

_  _  _  _  _  _  _  -  -  _           (signal b)

The tool shows the property starts at 2nd tick, and fails at fourth tick.
~a[*1:10] = ~a[*1] or ~a[*2] or … or ~a[*10]. In the waveform, ~a[1] is true and ~[a2] is false. But,1 or 0 or 0 = 1, so the left operand of intersect are always true.
why it fails at fourth tick?
Thank you!

2

In reply to peter:
(~a[*1:10]) intersect (b[->1] ##1 !b) says that
a==0 at ALL cycles between the attempt and the sequence (b[->1] ##1 !b).
$rose(a) |=> (~a[*1:10]) intersect (b[->1] ##1 !b)
In your example, $rose(a) is at T2, and (~a[*1:10] fails at t4 because a==1
I don’t understand your argument.
See my paper Reflections on Users’ Experiences with SVA, Part II | Verification Horizons - July 2022 | Verification Academy


   1  2  3  4  5  6  7  8  9
|  |  |  |  |  |  |  |  |  |           (clk rising_edge) 
 
_  -  _  -  _  _  _  _  _  _           (signal a) ==1 at t1, t3
 
_  _  _  _  _  _  _  -  -  _           (signal b)
   +--------------------+
___+                    +----           (b[->1] ##1 !b)

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/
3

In reply to ben@SystemVerilog.us:
Hi Ben,thanks for reply.


   1  2  3  4  5  6  7  8  9
|  |  |  |  |  |  |  |  |  |           (clk rising_edge) 
 
_  -  _  -  _  _  _  _  _  _           (signal a) ==1 at t1, t3

I have some questions related to intersect.
(~a[*1:10]) intersect (b[->1] ##1 !b) , (~a[*1:10]) and (b[->1] ##1 !b) start and end in the same cycle.

Q1: How to know the start point for (b[->1] ##1 !b) and (~a[*1:10])?
Q2: if b is 1 at t2, does it mean that (b[->1] ##1 !b) not match at t2? Therefore,(~a[*1:10]) intersect (b[->1] ##1 !b) not match, and my property is false. Am I correct?
Thank you

4

In reply to peter:


   1  2  3  4  5  6  7  8  9
|  |  |  |  |  |  |  |  |  |           (clk rising_edge) 
  +--+  +--+
__+  +__+  +_____  _  _  _           (signal a) ==1 at t1, t3
 
_  _  _  _  _  _  _  -  -  _           (signal b)
                      +--+
______________________+  +____          (b[->1] ##1 !b)

I have some questions related to intersect.
(~a[*1:10]) intersect (b[->1] ##1 !b) , (~a[*1:10]) and (b[->1] ##1 !b) start and end in the same cycle.

Not quite correct.
(~a[*1:10]) and (b[->1] ##1 !b) Must start in the same cycle
and in one sequence ends, then the other sequence must match at the completion
of that other ended sequence.
For the above diagram, If I wrote as follows:
(##1 a ##1 !a ##1 a ##1 !a[*1:]) intersect (b[->1] ##1 !b) then when the RHS sequence ends, the LHS sequence must match until that point. The LHS is endless because of the [*1:].
If the LHS does not have a match during the RHS sequence, then the antecedent fails.

5

In reply to ben@SystemVerilog.us:

Hi Ben,
What is the difference between these two sequence?

A:(~a[*1:10]) intersect (!b[*0] ##1 b ##1 !b)
B:(~a[*1:10]) intersect (##1 b ##1 !b)

I used sequence A can pass,but I supposed it should fail.
Would you explain detaily to me why sequence A and B is not same ?
Thank a lot

6

In reply to peter:
a_sequence[*0] is called an empty match
(b[*0] ##1 c ) is equivalent to c
Thus,
A:(~a[*1:10]) intersect (!b[*0] ##1 b ##1 !b) // is same as
A:(~a[*1:10]) intersect (b ##1 !b)
// Obviously different that
B:(~a[*1:10]) intersect (##1 b ##1 !b)


/* 1800'2017 16.9.2.1 Repetition, concatenation, and empty matches Using 0 as a sequence repetition number, an empty sequence (see 16.7 ) results, as in this example: */
a [*0] 
/* Because empty matches occur over an interval of zero clock ticks and are thus of length 0, they follow the set of concatenation rules specified below. In the following rules, an empty sequence is denoted as empty, and another sequence (which may be empty or nonempty) is denoted as seq.*/
 — (empty ##0 seq) does not result in a match. 
 — (seq ##0 empty) does not result in a match. 
 — (empty ##n seq), where n is greater than 0, is equivalent to (##(n-1) seq). 
 — (seq ##n empty), where n is greater than 0, is equivalent to (seq ##(n-1) `true).

Ben Systemverilog.us

7

In reply to ben@SystemVerilog.us:

Hi Ben,
what is the meaning of empty match? someone says s[*0] not match any posititve number of clocks.
I am a bit confused.
what scenario we need using the empty match? (would you give an example)

Thank you

8

In reply to peter:

a_seq[*0] is an empty match because repeating something 0 times means it does not exist.
It comes up when you write something like
a ##1 b[*0:1] ##1 c
// same as
a ##1 b[*0] ##1 c or a ##1 b[*1] ##1 c
// same as
a ##1 c or a ##1 b[*1] ##1 c