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.