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

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.

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

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