Hi Dmitry, I have read through the 1682 proposal. The big problem with it is that it doesn't specify how the future-value functions are to be implemented, according to the Verilog scheduling semantics. Do the future-value functions simply compare the sampled value of the signal with the Observed value when the assertion executes? Tom Korchemny, Dmitry wrote On 09/17/07 12:39 AM,: > Hi Johan, > > I fixed Example 2 and added a row to the table. I also fixed the numeration (as pointed by Shalom). > > Thanks, > Dmitry > > -----Original Message----- > From: johan.martensson@jasper-da.com [mailto:johan.martensson@jasper-da.com] > Sent: Tuesday, September 11, 2007 4:00 PM > To: Korchemny, Dmitry > Cc: sv-ac@eda-stds.org > Subject: Re: [sv-ac] 1682 > > Hi Dmitry, > > there was a mistake in what I wrote below. The property in Example 2: > > | a: assume property(@$global_clocking $rising_gclk(clk) ##1 > | (!$falling_gclk(clk)[*1:$]) |-> $steady_gclk(sig) ); > > states that sig must be stable between any rising edge > of clk and the first subsequent falling edge of clk. > > This leads me to think that there maybe is a typo in the property. > > The following property seems to fit the description better. > > a: assume property(@$global_clocking $falling_gclk(clk) ##1 > (!$falling_gclk(clk)[*1:$]) |-> $steady_gclk(sig) ); > > Best Regards, > > Johan M > > > > > On Tue, Sep 11, 2007 at 12:22:11PM +0200, Johan Mårtensson wrote: > >>Hi Dimitry, >> >>A couple of additional comments on 1682.2007.09.09.pdf. >> >>1) Table 16-25 >>------------- >> >>I think the example table 16-25 would gain somewhat by adding a row for >>a timepoint where the there is an edge on sig in the next timepoint. >>I think that would help avoid a possible misunderstanding. >>For example at time 40 $sampled(sig)==0, $future_gclk(sig)==0, >>$rising_gclk(sig)==false, $falling_gclk(sig)==false, >>$changing_gclk(sig)==false, $steady_gclk(sig)==true, (i.e. same as for >>time point 30) >> >>2) Example 2 >>------------- >> >>| Example 2: The following assumptions states that a signal sig must >>| remain stable between two falling edges of a clock clk as sampled by >>| global clocking. This differs from the property in Example 1 in the case >>| where the first falling edge of clk has not yet occurred. In Example 1, >>| sig is not allowed to change in that case, but in this example sig can >>| toggle freely while we wait for clk to begin. >>| >>| a: assume property(@$global_clocking $rising_gclk(clk) ##1 >>| (!$falling_gclk(clk)[*1:$]) |-> $steady_gclk(sig) ); >>| >> >>There seems to be some kind of mismatch between the explanation and the >>assumption a. >> >>The property seems to state not that "signal sig must remain stable >>between two falling edges of a clock clk" but that sig must be stable >>between (and including) any rising edge of clk and (but not >>including) the first subsequent falling edge of clk." >> >>Furthermore in case clk has a rising edge before it has its first >>falling edge then sig may be constrained before the first falling edge >>of clk contrary to what seems to be stated in the explanation. >> >>Best Regards, >> >>Johan M >> >> >>On Wed, Sep 05, 2007 at 04:33:56PM +0300, Bustan, Doron wrote: >> >>>Hi, >>> >>> >>> >>> >>> >>> >>> >>>Here are my remarks >>> >>> >>> >>>1. Font is not correct. >>>2. Most of the text should be in blue. >>>3. first paragraph: >>> >>> >>> >>> I would replace: >>> >>> >>> >>> "These functions include the capability to access the >>>previous (resp. the next) value as sampled by >>> >>> the global clock tick that precedes (resp. follows) >>>immediately the time at which the function was called. >>> >>> Sampling of an expression is explained in 16.4." >>> >>> >>> >>> with >>> >>> >>> >>> "These functions include the capability to access the sample >>>value at previous (resp. the next) global clock >>> >>> tick that precedes (resp. follows) immediately the timestep >>>at which the function is called. >>> >>> Sample value is explained in 16.4." >>> >>> >>> >>>4. page 1 >>> >>> - $falling_gclk(expression) returns true if the sampled >>>value of the LSB of the expression >>> >>> is changing to 1 at the next global clocking tick. >>>Otherwise, it returns false. >>> >>> >>> >>> Should be >>> >>> >>> >>> - $falling_gclk(expression) returns true if the sampled value of >>>the LSB of the expression >>> >>> is changing to 0 at the next global clocking tick. Otherwise, it >>>returns false. >>> >>> >>> >>>5. example1, I would say that the error message error("sig is not >>>stable"); is executed at time 90. >>>6. page 3, I would change" >>> >>> >>> >>>"The following functions allow to access the immediate past and future >>>values as sampled by the >>> >>> global clock or detect changes in values of an expression as >>>sampled by the global clock." >>> >>> >>> >>> to >>> >>> >>> >>>"The following functions allow to access the sample value of an >>>expression at immediate past and future ticks of the >>> >>> global clock and to detect changes in sample value from past >>>(current) tick of the global clock to its current (next) tick." >>> >>> >>> >>>Doron >>> >>> >>> >>> >>> >>> >>>-- >>>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. >> > > -- ------------------ Thomas J. Thatcher Sun Microsystems 408-616-5589 ------------------ -- This message has been scanned for viruses and dangerous content by MailScanner, and is believed to be clean.Received on Wed Sep 19 17:07:40 2007
This archive was generated by hypermail 2.1.8 : Wed Sep 19 2007 - 17:08:17 PDT