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