Issue with until and throughout operators in a liveness check

Hi,

Suppose if I have a requirement like this:-
If the signal A rises and it remains high until an event B happens then from the next cycle, I should see an event C at some point in the future.
I tried this, but not working.

$rose(A) ##1 A until B[->1] |=> s_eventually C

I am confused if I should use throughout or until in the antecedent of this assertion.

Also, if on the occasion that A drops before event B then its not a fire it just means that C wont happen.And if that is the case can this serve my purpose?

A ##0 B |-> s_eventually C

is the above mentioned assertion (ie in part 2)same as this:
$rose(A) ##1 A throughout B[->1] |=> s_eventually C

if they are same then how are they effectively becoming the same and if not then how do they differ?

Any help/advice are appreciated. Thanks

In reply to nipradee:

$rose(A) ##1 A until B[->1] |=> s_eventually C

The until operator is for properties; specifically,
property_expr ::= property_expr s_until property_expr
Thus, a_sequence ##1 propert is illegal.

2)Also, if on the occasion that A drops before event B then its not a fire it just means that C wont happen.And if that is the case can this serve my purpose?
A ##0 B |-> s_eventually C

Yes.

  1. is the above mentioned assertion (ie in part 2)same as this:
    $rose(A) ##1 A throughout B[->1] |=> s_eventually C

Not quite. A ##0 B does does not require that A can be true before an occurrence of B.
Also, A is not a rose, thus, anytime A && B are true, the antecedent is a match.
The $rose(A) ##0 A throughout B[->1] covers the case of A ##0 B, but it also cover other cases before the B when A must hold until a B.
(You had $rose(A) ##1 A throughout B[->1] The minimum length of the sequence is
$rose(A) ##1 A ##0 B
BTE, the throughout is a sequence operator, and it is used correctly here.

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr


  1. SVA Alternative for Complex Assertions
    https://verificationacademy.com/news/verification-horizons-march-2018-issue
  2. SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
  3. SVA in a UVM Class-based Environment
    https://verificationacademy.com/verification-horizons/february-2013-volume-9-issue-1/SVA-in-a-UVM-Class-based-Environment

In reply to ben@SystemVerilog.us:
Did an edit to my reply
Ben