[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, and is
believed to be clean.