RE: [sv-ac] 1682

Hi Tom,

The proposal says specifically that the future function use sample value.
I do not think that the LRM should specify the implementation, it does says that action blocks should be execute in the future so I don't see any evident that it is "very hard" to implement it.

Regards

Doron

-----Original Message-----
From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On Behalf Of Thomas Thatcher
Sent: Thursday, September 20, 2007 2:07 AM
To: Korchemny, Dmitry
Cc: johan.martensson@jasper-da.com; sv-ac@server.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.