Re: [sv-ac] 16.12.10 Nexttime property // clarification question

Dana,
My comparison to the followed-by was because of my misunderstanding of the
nexttime. Specifically,
 ap_acd: *assert property*(*a* |-> *s_nexttime **[2] (c ##3 d)* );
I originally viewed the nexttime as a requirement that the
property_expression of nexttime occurs at the termination of the index n,
i.e., the property expresseion of nextttime ends after *n *cycles, which is
a very wrong conclusion.
I still view nexxtime (property_expression) to be similar to the (
strong(#n 1'b1) #-# property_expression) in that it defines the starting
point of that property_expression. The differences are shown in the summary
below.
 .
What is most confusing is this statement "*true beginning at the last of
the next constant_expression clock ticks." *
Your explanationis clearer.

The semantics of s_nexttime operator, dictates that s_nexttime[k] prop holds
on cycle n iff there are at leastn+k cycles and the property prop holds at
cycle n+k.
In contrast, the semantics of its weak version, the nexttime operator,
dictates that nexttime[k] prop holds on cycle n also if there are less than
 n+k cycles

Apart from that, not sure how you can compare a unary operator such as *
nexttime*(prop) (or nexttime[k](prop)) to a binary operator such as (seq)*
followed-by*(prop)…
The comparison is because the LRM defines
property_expr ::= | sequence_expr #-# property_expr | sequence_expr #=#
property_expr
| nexttime property_expr| nexttime [ constant _expression ] property_expr |
s_nexttime property_expr
| s_nexttime [ constant_expression ] property_expr
Thus, they are all properties. See below for my summary on that.

In summary:

*Syntax: **nexttime [*constant_expression*] property_expr*

*[1] The indexed weak nexttime property nexttime [constant_expression]
property_expr evaluates to*

*true if, and only if, either there are not constant_expression clock ticks
or property_expr evaluates to*

*true beginning at the last of the next constant_expression clock ticks*.

*nonvacuous true* : there are n clocks, and P is true nonvacuously

*true vacuously*: no n clocks, or P is vacuous

*fail *: at least 1 more clock, but less than n clocks, or n clocks and P
fails

*Syntax: s_**nexttime [*constant_expression*] property_expr*

*[1] **The indexed strong nexttime property **s_nexttime **[**
constant_expression**] **property_expr***

*evaluates to true if, and only if, there exist constant_expression clock
ticks and property_expr evaluates to true beginning at the last of the next
constant_expression clock ticks**. *

*nonvacuous true* : there are n clocks, and P is true nonvacuously

*true vacuously*: n clocks and P is vacuous

*fail** *: less than n clocks, or n clocks and P fails

*Equivalency*

strong(##n 1'b1) #-# P // same as

not (strong(##n 1'b1) |-> not property_expr)

* *

*nonvacuous true* : there are n clocks, and P is true nonvacuously

*true vacuously*: n clocks, or P is vacuous

*fail** *: less than n clocks, or n clocks and P fails

Am I off somewhere on this?

Dana, Thanks.

Ben Cohen

On Tue, Jan 31, 2012 at 11:58 AM, Dana Fisman Ofek <Dana.Fisman@synopsys.com
> wrote:

> Hi Ben,****
>
> ** **
>
> [Ben] So in essence, the nexxttime[n] property_expression is almost
> equivalent to the ****
>
> [Ben] followed-by, but with requirements about the fate of the property
> if *n cycles *is never reached ****
>
> ** **
>
> That is no quite right. ****
>
> ** **
>
> First nexttime[n] does not impose there are any additional cycles. It is
> its strong version s_nexttime[n] that requires that.****
>
> ** **
>
> Also, while it’s true that follows by itself does not impose a certain
> requirement about future cycles, you can (if you want to) add such a
> requirement, by using strong(sequence) rather than weak(sequence). ****
>
> ** **
>
> That is, the requirement for future cycles can be attributed to almost all
> temporal operator, by choosing the strong rather than weak version.****
>
> ** **
>
> Apart from that, not sure how you can compare a unary operator such as *
> nexttime*(prop) (or nexttime[k](prop)) to a binary operator such as (seq)*
> followed-by*(prop)… ****
>
> ** **
>
> Best,****
>
> Dana****
>
> ** **
>
> *From:* ben cohen [mailto:hdlcohen@gmail.com]
> *Sent:* Tuesday, January 31, 2012 2:18 PM
> *To:* Dana Fisman Ofek
> *Cc:* Daniel Mlynek; sv-ac@eda-stds.org; Korchemny, Dmitry
>
> *Subject:* Re: [sv-ac] 16.12.10 Nexttime property // clarification
> question****
>
> ** **
>
> Dana, ****
>
> I think I understand my confusion. Be low is a summary of key points, and
> an explanation of my current (updated) understanding.****
>
> [LRM] *[1] The indexed strong nexttime property **s_nexttime **[constant_expression]
> property_expr*****
>
> *evaluates to true if, and only if, there exist constant_expression clock
> ticks and property_expr evaluates to true beginning at the last of the next
> constant_expression clock ticks. * ****
>
> *[Dana] So by saying that the property evaluates to true **at the last of
> the next constant_expression clock ticks **we require that starting at
> the correct cycle things behave as we expect them too. The evaluation may
> indeed last much after*****
>
> [Ben] ap_acd: *assert property*(*a* |-> *s_nexttime **[2] (c ##3 d)* );***
> *
>
> The following is equivalent to (in English) ****
>
> If(a) then after 2 cycles *c *must be true, and 3 cycles after that *d
> *must be true. ****
>
> Thus, if a==1 at cycle k, c must be a 1 at cycle k+2, and d must be a 1
> at cycle k+2+3. ****
>
> Because sequence (c ##3 d) is weak, the property (c ##3 d) would be
> true if c==1 at cycle k+2, and if there are no more clocks after that. If
> there are no more clocks, then the assertion ap_acd would be true
> nonvacuously since (per 16.14.8 c) an evaluation attempt of a property of
> the form weak(sequence_expr) is always nonvacuous.****
>
> ** **
>
> So in essence, the nexxttime[n] property_expression is almost equivalent
> to the followed-by, but with requirements about the fate of the property if
> *n cycles *is never reached : ****
>
> ## n 1'b1 #-# property_expression****
>
> For the followed-by if there are not *n cycles,* and simulation ends
> prior to the evaluation of the property, then the property is vacuous per
> 16.14.8 j) ****
>
> *An evaluation attempt of a property of the form sequence_expression #-#
> property_expr is*
>
> *nonvacuous if, and only if, there is a successful match of the
> antecedent sequence_expression and*
>
> *the evaluation attempt of property_expr that starts at the end point of
> the match is nonvacuous.*
>
> * *
>
> Thanks, ****
>
> Ben Cohen ****
>
> ** **
>
> On Tue, Jan 31, 2012 at 5:38 AM, Dana Fisman Ofek <
> Dana.Fisman@synopsys.com> wrote:****
>
> Thanks for the correction Daniel – you are perfectly right.****
>
> (I misread the property as if it was using |=> rather than |->).****
>
> ****
>
> Thanks,****
>
> Dana****
>
> ****
>
> *From:* Daniel Mlynek [mailto:danielm@aldec.com.pl]
> *Sent:* Tuesday, January 31, 2012 2:16 AM
> *To:* Dana Fisman Ofek
> *Cc:* ben@systemverilog.us; sv-ac@eda-stds.org; Korchemny, Dmitry
> *Subject:* Re: [sv-ac] 16.12.10 Nexttime property // clarification
> question****
>
> ****
>
> Dana>By the semantics of a weak sequence, the weak sequence (c ##3 d) hold
> on cycle n iff c holds on cycle n+1 if such exists, and d holds on cycle
> n+4 if such a cycle exits (in contrast to the strong version which will
> also require that cycle n+4 exist).
>
> Why n+1 and n+4 I would rather think that:
>
> By the semantics of a weak sequence, the weak sequence (c ##3 d) hold on
> cycle n iff c holds on cycle n if such exists, and d holds on cycle n+3if such a cycle exits (in contrast to the strong version which will also
> require that cycle n+3 exist).
>
>
> DANiel
>
> On 1/30/2012 6:20 PM, Dana Fisman Ofek wrote: ****
>
> Hi Ben,****
>
> ****
>
> The number of cycles required after the last a in the property below is
> determined not only by the semantics of the *s_nexttime operator*, but
> also by the semantics of the *weak sequence construct*.****
>
> ****
>
> The semantics of s_nexttime operator, dictates that s_nexttime[k] prop holds
> on cycle n iff there are at least n+k cycles and the property prop holds
> at cycle n+k.****
>
> In contrast, the semantics of its weak version, the nexttime operator,
> dictates that nexttime[k] prop holds on cycle n also if there are less
> than n+k cycles.****
>
> ****
>
> In our case the property prop is a weak sequence (this is because it is
> not qualified and the LRM dictates that unqualified sequences are regarded
> as weak if they appear in assert (Section F.3.4.3.1)).****
>
> ****
>
> By the semantics of a weak sequence, the weak sequence (c ##3 d) hold on
> cycle n iff c holds on cycle n+1 if such exists, and d holds on cycle n+4if such a cycle exits (in contrast to the strong version which will also
> require that cycle n+4 exist). ****
>
> ****
>
> Best,****
>
> Dana****
>
> ****
>
> *From:* owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org<owner-sv-ac@eda.org>]
> *On Behalf Of *ben cohen
> *Sent:* Monday, January 30, 2012 11:51 AM
> *To:* sv-ac@eda-stds.org; Korchemny, Dmitry
> *Subject:* [sv-ac] 16.12.10 Nexttime property // clarification question***
> *
>
> ****
>
> 16.12.10 states the following: ****
>
> *s_nexttime [ constant_expression ] property_expr*****
>
> The indexed strong nexttime property s_nexttime [constant_expression]
> property_expr****
>
> evaluates to true if, and only if, there exist constant_expression clock
> ticks and property_expr****
>
> evaluates to true* beginning at the last of the next constant_expression
> clock ticks.*****
>
> ****
>
> *nexttime [ constant_expression ] property_expr*****
>
> The indexed weak nexttime property nexttime [constant_expression]
> property_expr evaluates to****
>
> true if, and only if, either there are not constant_expression clock ticks
> or* property_expr evaluates to*****
>
> *true beginning at the last of the next constant_expression clock ticks***
> **
>
> ****
>
> Given this assertion with a default clocking: ****
>
> ap_acd: *assert property*(*a* |-> *s_nexttime [2] (c ##3 d)* );****
>
> Assume for simplicity, that a==c==d==1 at all cycles, an for the purpose
> of discussion, we'll address a single attempt of *ap_acd.* ****
>
> Also assume that there are many many cycles after that one attempt where
> "a==1". Again, for this analysis, I am only looking at that one attempt of
> the assertion *ap_acd*. ****
>
> In (a |-> nexttime [2] (c ##3 d)) ****
>
> *nexttime[2] would imply that I need at least 2 more clocks after a or
> the property (c ##3 d) is false. *****
>
> ****
>
> I come to this conclusion because the LRM says "true if .. property_expr evaluates
> to true* beginning at the last of the next constant_expression clock
> ticks.".* Let constant_expression be 2, then that reads for ( nexttime
> [2] (c ##3 d ) ) must evaluates to true *beginning at the last of the
> next 2 clock ticks.* ****
>
> But (*(c ##3 d*) *is not true after 2 ticks, it needs 3.* ****
>
> BTW, If I use the weak nexttime, in *ap_acd,* then under the same
> circumstances, the assertion would be vacuous. ****
>
> ****
>
> Is my understanding of the nexttime operation incorrect? If I use the
> nexxtime, I need to know the length of the property, other wise the
> property is false if i have enough clock cycles, correct? ****
>
> Thanks, ****
>
> Ben Cohen ****
>
>
> --
> This message has been scanned for viruses and
> dangerous content by *MailScanner* <http://www.mailscanner.info/>, and is
> believed to be clean. ****
>
>
> --
> This message has been scanned for viruses and
> dangerous content by *MailScanner* <http://www.mailscanner.info/>, and is
> believed to be clean. ****
>
> ** **
>

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.