Re: [sv-ac] Issue #1296

Hi Dmitry:

The main challenge is to detect simultaneity of "independent" clocking
events via a synthesizable RTL construction.

Ed Cerny posed the problem slightly differently, but the essence is
the following.  Suppose that you may not assume that @(clk1) and
@(clk2) can be resolved in terms of a clocking event of finer 
granularity.  Then how do you build a synthesizable RTL representation
of a checker for 

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

that detects simultaneity of clk1 and clk2 if it happens to occur?

I am sorry not to be able to phrase this more directly, but, frankly,
I do not understand the precise notion of synthesizability well
enough to do so.

It is clear to me that verification IP have been and can be designed 
to detect such simultaneity, but the requirement that the verification 
IP be represented by synthesizable RTL is stricter.

Best regards,

John H.


> X-MimeOLE: Produced By Microsoft Exchange V6.5.7226.0
> Content-class: urn:content-classes:message
> Date: Wed, 22 Feb 2006 15:30:30 +0200
> X-MS-Has-Attach: 
> X-MS-TNEF-Correlator: 
> Thread-Topic: [sv-ac] Issue #1296
> Thread-Index: AcY3s6Oxsq45ysH5S4SpLjMN//m64AAAEVDw
> From: "Korchemny, Dmitry" <dmitry.korchemny@intel.com>
> Cc: <sv-ac@eda.org>
> X-OriginalArrivalTime: 22 Feb 2006 13:30:31.0060 (UTC) FILETIME=[26C31D40:01C637B4]
> X-Scanned-By: MIMEDefang 2.31 (www . roaringpenguin . com / mimedefang)
> 
> Hi John,
> 
> Can you remember any specific problems related to the RTL
> synthesizability?
> I cannot see any issues with it.
> 
> Thanks,
> Dmitry
> 
> -----Original Message-----
> From: John Havlicek [mailto:john.havlicek@freescale.com]=20
> Sent: Wednesday, February 22, 2006 3:24 PM
> To: Korchemny, Dmitry
> Cc: sv-ac@eda.org
> Subject: 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=20
> are other ways in which Annex E as it stands now is more general than=20
> Section 17 (e.g., the treatment of "disable iff" as a general property=20
> operator).
> 
> The relaxed approach to clock changes across |-> and ##0 is in alignment
> 
> with PSL, in which the form
> 
> A@(clk1) |-> B@(clk2)=20
> 
> is legal with the semantics that you describe.
> 
> I also support this approach, and we should strongly consider=20
> 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:=20
> > X-MS-TNEF-Correlator:=20
> > Thread-Topic: [sv-ac] Issue #1296
> > Thread-Index: AcY3q27ufJLqkUB+SG22UhtMQ1X/mw=3D=3D
> > From: "Korchemny, Dmitry" <dmitry.korchemny@intel.com>
> > X-OriginalArrivalTime: 22 Feb 2006 12:28:08.0199 (UTC)
> FILETIME=3D[6FD7D970:01C637AB]
> > X-Scanned-By: MIMEDefang 2.31 (www . roaringpenguin . com /
> mimedefang)
> > X-Virus-Status: Clean
> > Sender: owner-sv-ac@eda.org
> >=20
> > This is a multi-part message in MIME format.
> >=20
> > ------_=3D_NextPart_001_01C637AB.6FC6E9CA
> > Content-Type: text/plain;
> > 	charset=3D"us-ascii"
> > Content-Transfer-Encoding: quoted-printable
> >=20
> > Hi all,
> >=20
> > =3D20
> >=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.,
> >=20
> > @(clk1) A |->@(clk2) B
> >=20
> > 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
> > =3D20
> >=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
> > =3D20
> >=20
> > ---
> >=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
> >=20
> > @(posedge clk0) s0 |-> @(posedge clk1) s1 ##1 @(posedge clk2) s2
> >=20
> > is illegal, but
> >=20
> > @(posedge clk0) s0 |-> @(posedge clk0) s1 ##1 @(posedge clk2) s2
> >=20
> > is legal.
> >=20
> > ---
> >=20
> > =3D20
> >=20
> > Thanks,
> >=20
> > Dmitry
> >=20
> >=20