Hi Johan: assert property(@(1'b1) P); is legal syntax. As an event, 1'b1 never occurs, so there will never be an underlying evaluation of P. Note that this is not what our formal semantics says for this form. The discrepency is because the formal semantics does not account for the semantics of event controls. The formal semantics assumes that an event control has been translated into a boolean expression c in assert property(@(c) P); that evaluates to true exactly on the letters at which the original event control @(1'b1) has events. For this specific example, we can take c = 1'b0. Something else that is not accounted for in the formal semantics is the preponed sampling. We assume that the letters in Annex F are given in a way that the expression evaluation on a letter yields the appropriate sampled values of the underlying variables. Thus, assert property(@(posedge clk) clk); will fail at every posedge of clk, because if clk has a posedge in a timestep, then the preponed value of clk must (when coerced to bit) be 1'b0. On the other hand, assert property(@(negedge clk) clk); may pass or fail at a negedge of clk, depending on whether the preponed value of clk is 1'b1 or one of 1'bx,1'bz. J.H. > Date: Wed, 14 Nov 2007 10:24:30 +0100 > From: Johan =?iso-8859-1?Q?M=E5rtensson?= <johan.martensson@jasper-da.com> > Cc: martin@jasper-da.com, sv-ac@eda.org > Content-Disposition: inline > X-OriginalArrivalTime: 14 Nov 2007 09:24:33.0538 (UTC) FILETIME=[2AD67620:01C826A0] > > 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.Received on Thu Nov 15 10:44:00 2007
This archive was generated by hypermail 2.1.8 : Thu Nov 15 2007 - 10:44:14 PST