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.