RE: [sv-ac] Issue #1296

Actually, I think that both 

always @(posedge clk1 or posedge clk2)

and

@(posedge clk or negedge clk)

are generally not synthesizable.

Shalom


> -----Original Message-----
> From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On
> Behalf Of Korchemny, Dmitry
> Sent: Tuesday, February 28, 2006 6:14 PM
> To: Eduard Cerny; john.havlicek@freescale.com
> Cc: sv-ac@eda.org
> Subject: RE: [sv-ac] Issue #1296
> 
> Hi Ed,
> 
> I would like to better understand the synthesizability issue.
> It is not
> clear to me how to synthesize a property with an edge-sensitive
> clock
> without a system clock?
> 
> E.g.,
> 
> assert property (@clk a |-> b);
> 
> Nevertheless, this property is legal.
> 
> Let's now consider the (illegal) property
> 
> assert property (@(posedge clk1) a |-> @(posedge clk2) b);
> 
> It is clear how to synthesize it when we have a reference
> clock. For FV
> purposes and for the emulation there is always a reference
> clock,
> therefore there are no synthesizability problems.
> 
> The question is why we need the synthesizability for the
> simulation? If
> the purpose is to "synthesize" a pure Verilog code, it may be
> solved by
> using
> 
> always @(posedge clk1 or posedge clk2)
> 
> Indeed, this is a reference clock for our case.
> 
> In the former example, @clk may be represented as @(posedge clk
> or
> negedge clk), therefore I don't see much difference between
> these two
> cases. Thus, if the first is synthesizable, why is not the
> second?
> 
> Thanks,
> Dmitry
> 
> -----Original Message-----
> From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On
> Behalf Of
> Eduard Cerny
> Sent: Wednesday, February 22, 2006 6:12 PM
> To: john.havlicek@freescale.com; Korchemny, Dmitry
> Cc: sv-ac@eda.org
> Subject: RE: [sv-ac] Issue #1296
> 
> Yes, the reason for not allowing simultaneous clock ticks of
> clk1 and
> clk2, rather than the nearest strructly future tick of clk2
> wass
> synthesizability w/o an additional system clock. I do not think
> that we
> should go back and start changing that.
> 
> ed
> 
> 
> > -----Original Message-----
> > From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On
> > Behalf Of John Havlicek
> > Sent: Wednesday, February 22, 2006 8:24 AM
> > To: dmitry.korchemny@intel.com
> > 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
> > 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
> > >
> > >
> >