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 cholds on cycle n+1if such exists, and dholds on
cycle n+4if such a cycle exits (in contrast to the strong version which
will also require that cycle n+4exist).

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 cholds on cycle nif such exists, and dholds on cycle n+3if
such a cycle exits (in contrast to the strong version which will also
require that cycle n+3exist).

DANiel

On 1/30/2012 6:20 PM, Dana Fisman Ofek wrote:
>
> Hi Ben,
>
> The number of cycles required after the lastain 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_nexttimeoperator, dictates that s_nexttime[k] prop
> holds on cycle niff there are at least n+kcycles and the property
> propholds at cycle n+k.
>
> In contrast, the semantics of its weak version, the nexttimeoperator,
> dictates that nexttime[k] propholds on cycle nalso if there are less
> than n+k cycles.
>
> In our case the property propis 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 cholds on cycle n+1if such exists, and dholds on cycle
> n+4if such a cycle exits (in contrast to the strong version which will
> also require that cycle n+4exist).
>
> Best,
>
> Dana
>
> *From:*owner-sv-ac@eda.org [mailto: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.