Hi Tom, As an example, consider Clause 17. Constrained random value generation. The random constraint solving is far not too obvious to implement, and it may have very poor performance. Nevertheless, the LRM does not say a word about its implementation. Another example is a formal verification of assertions. Its algorithm is not described in the LRM, either. Thanks, Dmitry ________________________________ From: Eduard Cerny [mailto:Eduard.Cerny@synopsys.com] Sent: Friday, September 21, 2007 4:08 PM To: Thomas.Thatcher@Sun.COM; Eduard Cerny Cc: Korchemny, Dmitry; sv-ac@eda-stds.org Subject: RE: [sv-ac] 1682 Hi Tom, I am not sure if we have to provide more detail for implementation, I'd think actually that not. The functions are well defined, so the implementor can have different ways to do it, as long as the reporting is correct. No? Best regards ed ________________________________ From: Thomas.Thatcher@Sun.COM [mailto:Thomas.Thatcher@Sun.COM] Sent: Friday, September 21, 2007 1:01 AM To: Eduard Cerny Cc: Korchemny, Dmitry; sv-ac@eda-stds.org Subject: Re: [sv-ac] 1682 Hi Ed, The text says that the "action block" is performed at the next global clocking tick, but didn't say anything about the evaluation of the assertion. Let's see if I understand what you are saying: A sequence expression like $rising_gclk(sig) must be evaluated as (@$global_clk ##1 $rose_gclk(sig)) in a simulation environment because the simulator can never know the final end-of-timestep value when the assertion is evaluated in the observed region. Is that correct? I think some additional explanation is necessary to make this clear. Thanks, Tom Eduard Cerny wrote: Hi Tom, It does say "An action block of an assertion containing next value functions is performed at the time when all the next values are actually computed, that is, at the global clocking tick that follows the assertion clock tick at which the final boolean expression of the assertion is evaluated." Whi implicitly means that you shift it all back by on global clock cycle. Using $past(x,,,$global_clock) and similat constructs. ed -----Original Message----- From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of Thomas Thatcher Sent: Wednesday, September 19, 2007 8:07 PM To: Korchemny, Dmitry Cc: johan.martensson@jasper-da.com; sv-ac@eda-stds.org Subject: Re: [sv-ac] 1682 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. --------------------------------------------------------------------- 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.Received on Tue Sep 25 05:43:28 2007
This archive was generated by hypermail 2.1.8 : Tue Sep 25 2007 - 05:43:35 PDT