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

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+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.