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.
> 

-- 
------------------------------------------------------------
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.