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?
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.
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.