A simple assertion; req implies ack; does not fail

SystemVerilog
, , ,
1

Hello,

I have a simple assertion as follows:

$rose(req) |=> !req[*1:10] until ack ##1 !ack;

On detection of $rose(req), I check to see that !req consecutively remains low -until- ack is true. Once ack is true, it should de-assert ack the very next clock.

I test with $rose(req); then keep !req asserted until ack arrives. But then I keep ack=1 for 4 clocks. It does not go low the very next clock. Still, the assertion does not fail. The thread “!req[*1:10] until ack” seems to keep firing, even after ack has arrived and the ‘until’ condition is satisfied.

Any ideas why the assertion does not fail? Thanks.

Here’s the EDA playground link that simulates this scenario. UDEMY : STUDENT QUESTION : Req=>Ack - EDA Playground

Example

2

In reply to a72:
I never liked to use the until construct when the left hand side is is not a simple expression. I find it confusing to use the until when property_expr1 is a sequence rather than a simple expression.
property_expr1 until property_expr2
An until property of the non-overlapping form (i.e., until, s_until) evaluates to true if property_expr1 evaluates to true at every clock tick beginning with the starting clock tick of the evaluation attempt and continuing until at least one tick before a clock tick where property_expr2 (called the terminating property) evaluates to true.

Try this for your assertion.


// $rose(req) |=> !req[*1:10] until ack ##1 !ack;
$rose(req) |=> !req[*1:10] intersect 
                 ack[->1] ##1 !ack;

More discussion on this coming soon.
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
  1. 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/

3

In reply to a72:

Probably, you expect the assertion fails because ack keeps 1 for 2 or more cycles.
But the property sees only negedge of ack, not how long ack keeps 1 or 0.

In short, B of “A until B” is like a event of end of A.

4

In reply to ben@SystemVerilog.us:

Ben, Thanks for the solution.

So, I also tried removing ‘until’ and still the test did not fail.

I tried

$rose(req) |=> !req[*1:10] ##1 ack ##1 !ack;

Here, the testbench is the same. ack stays high for more than one clock (when it should de-assert after 1 clock) and the test does not fail.

I understand ‘until’ is probably not the best choice but could you please explain why it does not work? It completely negates my understanding of ‘until’

Appreciate any further insight you can share.

Thanks.

5

In reply to a72:

  1. *$rose(req) |=> !req[1:10] ##1 ack ##1 !ack;

//  !req[*1:10] ##1 ack ##1 !ack; has many threads
!req[*1] ##1 ack ##1 !ack;
!req[*2] ##1 ack ##1 !ack;
..
!req[*10] ##1 ack ##1 !ack;
// If any of those thread you have the sequence (ack ##1 ack)
// the simulator tries the other threads.
// You may want to consider the use of the first_match().  Thus
$rose(req) |=> first_match(!req[*1:10] ##1 ack) ##1 !ack;
  1. *rose(req) |=> !req[1:10] until ack ##1 !ack;
    I got failures, See Edit code - EDA Playground
    I replaced the req with “a”, and the ack with “b”.
  2. until, s_until
    The Conditions for True Outcome for P1 until P2 are:
    See the table from my SVA book at http://systemverilog.us/vf/until_conditions.png

807×827 74.4 KB

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 - SystemVerilog - Verification Academy
  2. Free books: * Component Design by Example https://rb.gy/9tcbhl
  1. 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/

6

In reply to ben@SystemVerilog.us:

Great. That makes perfect sense. I tried the first_match solution and it gives me exactly what I was looking for. Should have thought of it.

Thanks very much for your time.

7

In reply to ben@SystemVerilog.us:

Hi Ben,
In your table,
p1 until p2,
case1:
p1: 11110
p2: 00001
or:
case2:
p1: 11111
p2: 00001
case3:
p1: 11110
p2: 00001

Q1:Do you mean case1 and case2 pass and case 3 fail?
Q2:If I want P2 only reponse p1, it means that p2 can not be 1 unless p1 is active.
How should I do? Thanks a lot!

8

In reply to timag:
A notation in my table:
1 (yellow bold)== nonvacuous true in a clocking event;
1 (plain text)==hold (vacuous or nonvacuous)

From 1800 page 472 "An evaluation attempt of a property of the form property_expr1 until property_expr2 is nonvacuous if, and only if,

  1. there is a clock event in which either the evaluation attempt of property_expr1 or the evaluation attempt of property_expr2 is nonvacuous,
  2. property_expr2 does not hold in prior clock events,
  3. and property_expr1 holds in all prior clock events."

Q1:Do you mean case1 and case2 pass and case 3 fail?

From my table:
Conditions for nonvacuity and true outcome
p1 until p2,
case1:
p1: 11110
p2: 00001

case2:
p1: 11111
p2: 00001

case3:
p1: 11110
p2: 00001

If I want P2 only response p1, it means that p2 can not be 1 unless p1 is active.
How should I do?

So you are asking for the case where the nonvacuous true for the until applies when any attempt of P1 is nonvacuous and P2 is also nonvacuous. Is that the question?
The way it is defined in 1800, for a nonvacuous true then P1 can be vacuous at all attempts so long as p2 is nonvacuous.
To get what you want restrict your properties to sequences since the
evaluation of sequences as properties cannot be vacuous.

9

In reply to ben@SystemVerilog.us:

Hi Ben,
Why all statements in column P1,P2 are same?

10

In reply to peter:
They are not the same. The bold yellow “1” are different than the plain text “1”
A notation in my table:
1 (yellow bold)== nonvacuous true in a clocking event;
1 (plain text)==hold (vacuous or nonvacuous)

11

In reply to ben@SystemVerilog.us:

Hi Ben, Thanks for reply
I am confused the meaning of " evaluation attempt". Would you explain to me?
And what is assertion property attempt?
Thanks a lot!

12

In reply to peter:

In reply to ben@SystemVerilog.us:
I am confused the meaning of " evaluation attempt". Would you explain to me?
And what is assertion property attempt?

Attempt : When the assertion is attempted at its leading clocking event, it is considered as a start event. In essence, an attempt is the start of an evaluation of an assertion. Assertion statements are started (attempted) at every leading clocking event, unless they are disabled or if they are turned off. If the attempt succeeds, one or more threads for that successful attempt are started, and those threads are independent from previous or future attempts. If the attempt fails, that assertion for that attempt is either vacuous if the property has an implication operator, or it fails if there is no implication in the property.

In summary: An assertion statement starts a new evaluation at every leading every clocking event of the property. Each evaluation is considered an attempt, which is sometimes referred to as “the start”. There is a single attempt of an assertion statement per leading clocking event; thus, each attempt has a life and fate of its own, and it is independent from other attempts.

1800 talks about “evaluation attempt of property expr1”
…there is a clock event in which either the evaluation attempt of property_expr1 or the evaluation attempt of property_expr2 is nonvacuous,
[Ben] This means an evaluation attempt of a property within an assertion. Yes, it is a bit confusing because we generally talk about attempts of assertions, not properties.
[1800]An until property of the non-overlapping form (i.e., until, s_until) evaluates to true if property_expr1 evaluates to true at every clock tick beginning with the starting clock tick of the evaluation attempt and continuing until at least one tick before a clock tick where property_expr2 (called the terminating property) evaluates to true.

Consider the property (##1 b ##1 a until c );
When 1800 says … property_expr1 evaluates to true at every clock tick beginning with the starting clock tick of the evaluation attempt and continuing until at least one tick before a clock tick where property_expr2 (called the terminating property) evaluates to true.
That means
The “at every clock tick”, you have an evaluation attempt of (##1 b ##1 a)
@t0 evaluate ##1 b ##1 a
@t1 evaluate ##1 b ##1 a
…
@tn evaluate ##1 b ##1 a
and all of these p1 must evaluate to true (vacuously or nonvacuously) until p2 is true (vacuously or nonvacuously). The outcome is based on the values of these evaluations, as addressed in my table.

My take on the until: I would avoid it and replace it with other constructs that are more easy to understand.

13

In reply to ben@SystemVerilog.us:

Thanks for reply.
I created a waveform to test p until q in the simulation.
p,q is bit signal. clock period is 10

time:0,10,20,30,40,50,60,70,80
   p:0, 0, 0, 0, 0, 1, 1, 1, 
   q:0, 0, 0, 1, 1, 1, 1, 1,

The simulation result:
assertion start at 10 ,fail at 10
assertion start at 20 ,fail at 20
assertion start at 30 ,fail at 30
assertion start at 40 ,success at 40
assertion start at 50 ,success at 50
assertion start at 70 ,success at 70

Question1:
In the spec (434):
An until property of the non-overlapping form evaluates to true if property_expr1 evaluates to true at every clock tick beginning with the starting clock tick of the evaluation attempt and continuing until at least one tick before a clock tick where property_expr2 evaluates to true
It means that p1 must be true at starting clock tick. But,the tool show assertion success at 40,50. At starting clock ticks(40,50), p1 is zero. I don’t know why tool say the assertion success. What is your opinion?
Question2:
In the spec(Page.472) :
An evaluation attempt of a property of the form property_expr1 until property_expr2 is
nonvacuous if, and only if, there is a clock event in which either the evaluation attempt of
property_expr1 or the evaluation attempt of property_expr2 is nonvacuous, property_expr2 does not hold in prior clock events, and property_expr1 holds in all prior clock events.

It seems that there is conflict with page 434. In page 472 mentions that p1 fail and p2 is nonvacuous true. Then, the whole property is nonvacuous true. But, In page 434 it mentions that the whole property is true only when p1 is true and p2 is true. Please correct me if i am wrong.

Thanks a lot!!!

14

In reply to peter:

Show the code.