RE: [sv-ac] Mantis 2168 - Formal semantics for edge-sensitive clocks

Hi Johan,

Let's consider P to be a boolean for the sake of simplicity.

My understanding that according the formal semantics @1 P should fail since the event @1 never happens. Since most implementations ignore the liveness part in this case, this assertion will pass. In any case this apparently is not what you intend. The correct way to express it is:

@$global_clock P.

Thanks,
Dmitry

-----Original Message-----
From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On Behalf Of johan.martensson@jasper-da.com
Sent: Wednesday, November 14, 2007 11:24 AM
To: John Havlicek
Cc: martin@jasper-da.com; sv-ac@server.eda.org
Subject: Re: [sv-ac] Mantis 2168 - Formal semantics for edge-sensitive clocks

Hi John,


On Wed, Nov 07, 2007 at 07:16:16AM -0600, John Havlicek wrote:
> Hi Johan:
> 
> I have not looked at the proposal for 2168.
> 
> In 16.4, the phrase "occurrence of a clock tick" is used, but I don't
> think this is explicitly defined.
> 
> My understanding has always been that the clocking event of a
> concurrent assertion is associated with an event expression, and to
> say that that clock "ticks" means that there is an occurrence of the
> event specified by the associated event expression.
> 
> >From there, we rely on the definitions of when various kinds of events
> occur.
> 
> For the example you cited, I think the relevant definitions are in
> 9.4.2.  If clk is a net or variable, then clk occurs as an event when
> its value changes.

What if clk is a constant? For example, what is the semantics of


assert property @(1'b1) P;

?

Is this kind of syntax even supported?

Best Regards,

Johan

> 
> In Annex F, the notion of event is abstracted.  We write @(c) and
> simply treat c as a boolean expression.  We assume that c holding
> on a letter is the same as saying the the associated event occurs
> in the timestep associated with the letter.
> 
> J.H.
> 
> > Date: Tue, 6 Nov 2007 18:10:32 +0100
> > From: Johan =?iso-8859-1?Q?M=E5rtensson?= <johan.martensson@jasper-da.com>
> > Cc: "Seligman, Erik" <erik.seligman@intel.com>,
> >         John Havlicek <john.havlicek@freescale.com>,
> >         Martin =?iso-8859-1?Q?Norb=E4ck?= <martin@jasper-da.com>,
> >         sv-ac@eda.org
> > Content-Disposition: inline
> > X-OriginalArrivalTime: 06 Nov 2007 17:10:35.0594 (UTC) FILETIME=[F2379AA0:01C82097]
> > 
> > Hi Dmitry, John, all,
> > 
> > 
> > Is the semantics of 
> > 
> > assert property @(clk) P;
> > 
> > clear from the LRM?
> > 
> > All examples of direct property clocking in the LRM seem to be of the
> > form @(posedge clk) or @(negedge clk), which seems compatible with a
> > level sensitive semantics for the clocking expression.
> > 
> > At the moment in our implementation also the clocking in
> > 
> > assert property @(clk) P;
> > 
> > is interpreted as level sensitive, i.e. the property (if it doesn't
> > contain other clocking) P is updated on every system clock tick when clk
> > is true.
> > 
> > Is this interpretation wrong in view of the LRM?
> > 
> > Best Regards,
> > 
> > Johan M
> > 
> > 
> > On Thu, Nov 01, 2007 at 11:49:21AM +0200, Korchemny, Dmitry wrote:
> > > Hi all,
> > > 
> > >  
> > > 
> > > I filed a new mantis item on edge and level sensitive clocks. The
> > > problem is that in SystemVerilog the clocks are edge sensitive, e.g.,
> > > @clk means that clk is going to change, while in the formal semantics
> > > description in Annex F the clocks are level-sensitive and @clk means
> > > that clk is high. The rules of converting edge sensitive clocks to level
> > > sensitive clocks are lacking in Annex F, and they are a subject of this
> > > proposal. Please, have a look.
> > > 
> > >  
> > > 
> > > Thanks,
> > > 
> > > Dmitry
> > > 
> > > ---------------------------------------------------------------------
> > > Intel Israel (74) Limited
> > > 
> > > This e-mail and any attachments may contain confidential material for
> > > the sole use of the intended recipient(s). Any review or distribution
> > > by others is strictly prohibited. If you are not the intended
> > > recipient, please contact the sender and delete all copies.
> > > 
> > > -- 
> > > This message has been scanned for viruses and
> > > dangerous content by MailScanner, and is
> > > believed to be clean.
> > > 
> > 
> > 
> > 
> > -- 
> > ------------------------------------------------------------
> > Johan Mårtensson                 Office: +46 31 7451913
> > Jasper Design Automation         Mobile: +46 703749681 
> > Arvid Hedvalls backe 4           Fax: +46 31 7451939
> > 411 33 Gothenburg, Sweden        Skype ID: johanmartensson
> > ------------------------------------------------------------

-- 
------------------------------------------------------------
Johan Mårtensson                 Office: +46 31 7451913
Jasper Design Automation         Mobile: +46 703749681 
Arvid Hedvalls backe 4           Fax: +46 31 7451939
411 33 Gothenburg, Sweden        Skype ID: johanmartensson
------------------------------------------------------------

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.
---------------------------------------------------------------------
Intel Israel (74) Limited

This e-mail and any attachments may contain confidential material for
the sole use of the intended recipient(s). Any review or distribution
by others is strictly prohibited. If you are not the intended
recipient, please contact the sender and delete all copies.

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.