Re: [sv-ac] Issue #1296

Hi Dmitry:

You are correct that the clock-flow.pdf attached to mantis 1296
does not enforce the restrictions discussed in Section 17.  There 
are other ways in which Annex E as it stands now is more general than 
Section 17 (e.g., the treatment of "disable iff" as a general property 
operator).

The relaxed approach to clock changes across |-> and ##0 is in alignment 
with PSL, in which the form

A@(clk1) |-> B@(clk2) 

is legal with the semantics that you describe.

I also support this approach, and we should strongly consider 
removing the restrictions in Section 17, although I have said in
the past that Annex E can be written more generally than Section 17.

My recollection from the SV 3.1 effort was that the restrictions
in Section 17 were written in an attempt to ensure that synthesizable
RTL representations of the assertions could be constructed.

Best regards,

John H.


> X-Authentication-Warning: server.eda.org: majordom set sender to owner-sv-ac@eda.org using -f
> X-MimeOLE: Produced By Microsoft Exchange V6.5.7226.0
> Content-class: urn:content-classes:message
> Date: Wed, 22 Feb 2006 14:28:06 +0200
> X-MS-Has-Attach: 
> X-MS-TNEF-Correlator: 
> Thread-Topic: [sv-ac] Issue #1296
> Thread-Index: AcY3q27ufJLqkUB+SG22UhtMQ1X/mw==
> From: "Korchemny, Dmitry" <dmitry.korchemny@intel.com>
> X-OriginalArrivalTime: 22 Feb 2006 12:28:08.0199 (UTC) FILETIME=[6FD7D970:01C637AB]
> X-Scanned-By: MIMEDefang 2.31 (www . roaringpenguin . com / mimedefang)
> X-Virus-Status: Clean
> Sender: owner-sv-ac@eda.org
> 
> This is a multi-part message in MIME format.
> 
> ------_=_NextPart_001_01C637AB.6FC6E9CA
> Content-Type: text/plain;
> 	charset="us-ascii"
> Content-Transfer-Encoding: quoted-printable
> 
> Hi all,
> 
> =20
> 
> If I understand the attached document correctly, it says (among the
> other) that the antecedent and the consequent of a property may have
> different clocks. I.e.,
> 
> @(clk1) A |->@(clk2) B
> 
> is legal for any clk1 and clk2. And the meaning of this formula is: at
> the moment of the tight satisfaction of A wait for the nearest tick of
> clk2 (this includes the case when clk2 ticks at the same time as clk1)
> and then check B controlled by clk2.
> 
> =20
> 
> I definitely support this approach since it eliminates a redundant
> restriction on the consequent clock and makes property semantics
> cleaner. But there are several sentences in the LRM that should be fixed
> accordingly. E.g. Section 17.12.2:
> 
> =20
> 
> ---
> 
> Because |-> overlaps the end of its antecedent with the beginning of its
> consequent, the clock for the end of the antecedent must be the same as
> the clock for the beginning of the consequent. For example, if clk0 and
> clk1 are not identical and s0, s1, and s2 are sequences with no clocking
> events, then
> 
> @(posedge clk0) s0 |-> @(posedge clk1) s1 ##1 @(posedge clk2) s2
> 
> is illegal, but
> 
> @(posedge clk0) s0 |-> @(posedge clk0) s1 ##1 @(posedge clk2) s2
> 
> is legal.
> 
> ---
> 
> =20
> 
> Thanks,
> 
> Dmitry
> 
>