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

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<mailto: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<mailto:danielm@aldec.com.pl>]
Sent: Tuesday, January 31, 2012 2:16 AM
To: Dana Fisman Ofek
Cc: ben@systemverilog.us<mailto:ben@systemverilog.us>; sv-ac@eda-stds.org<mailto: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+3 if 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+4 if 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> [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<mailto: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.