RE: [sv-ac] FW: P1800 AC issues

Hillel,

The prol\blem with doing so is that you force the use of a fast master clock
(time step). I do not believe that you can compile the assertion to a
synthesizable code that detects coincidence of clock edges w/o a fasster
master clock. That is then also a limitation and usually not worth the
trouble.

Hillel, if youu are still around the Dan hotel, let's talk about it. 

bestest
ed


> -----Original Message-----
> From: Miller Hillel-R53776 [mailto:r53776@freescale.com] 
> Sent: Thursday, April 07, 2005 7:49 AM
> To: 'Eduard Cerny'; Bustan Doron-DBUSTAN
> Cc: sv-ac@eda.org
> Subject: RE: [sv-ac] FW: P1800 AC issues
> 
> Ed, Doron
> Just as a remark, I think we should consider changing this 
> restriction in the future.
> In CBV, I have seen assertions that cross over domains 
> without the need to add an additional 
> cycle inbetween.
> Thanks
> Hillel
> 
> -----Original Message-----
> From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org]On 
> Behalf Of Eduard Cerny
> Sent: Thursday, April 07, 2005 2:30 PM
> To: Bustan Doron-DBUSTAN; 'Eduard Cerny'
> Cc: sv-ac@eda.org
> Subject: RE: [sv-ac] FW: P1800 AC issues
> 
> 
>  Hi Doron,
> 
> Hmm... I picked it up from the spread sheet, but, as you 
> probably did, I
> cannot locate it on the mantis errata web page.... 
> Actually, I cannot find most of the errata on the web page.
> http://www.eda-twiki.org/svdb/view_all_bug_page.php
> 
> I uess the issue number is the ballot issue # and not the 
> mantis number.
> Probably iy has to be entered first by us.
> 
> >From the spread sheet:
> 
> 217: The title says:
> Contradictory definition of the clocking rules of the 
> implication operator.
> Please clarify
> 
> The text says:
> 
> It is written in 18.12 that it is legal to use different clocks in the
> non-overlapping implication operator, but it is illegal to do 
> so in the
> overlapping implication operator:
> 
> The non-overlapping implication operator |=> can be used 
> freely to create a
> multiply-clocked property from an
> antecedent sequence and a consequent property that are differently- or
> multiply-clocked. The meaning of multiply-
> clocked non-overlapping implication is similar to that of 
> singly-clocked
> non-overlapping implication. For
> example, if s0, s1 are sequences with no clocking event, then in
> @(posedge clk0) s0 |=> @(posedge clk1) s1
> |=> synchronizes between posedge clk0 and posedge clk1. 
> Starting at the
> point at which the implication is
> being evaluated, for each match of s0 clocked by clk0, time 
> is advanced from
> the end point of the match to the
> nearest strictly future occurrence of posedge clk1, and from 
> that point
> there must exist a match of s1 clocked by
> clk1.
> .
> Since |-> overlaps the end of its antecedent with the beginning of its
> consequent, the clock for the end of the antecedent
> must be the same as the clock for the beginning of the consequent. For
> example, if clk0 and clk1 are not
> identical and s0, s1, s2 are sequences with no clocking events, then
> @(posedge clk0) s0 |-> @(posedge clk1) s1 ##1 @(posedge clk2) s2
> is illegal, but
> @(posedge clk0) s0 |-> @(posedge clk0) s1 ##1 @(posedge clk2) s2
> is legal.
> 
> >From the other hand, in the Annex H it is written:
> 
> H.2.3.1 Derived non-overlapping implication operator
> . ( R1 |=> P ) (( R1 ##1 1 ) |-> P ) .
> . ( S1 |=> Q ) ((S1 ##1 @(1) 1 ) |-> Q ) .
> Which means according the clocking rules stated above for the 
> operator '|->'
> that the consequence of the non-overlapping implication 
> operator should be
> always operated by the clock = 1
> 
> ------------------
> 
> Best regards,
> 
> 
> ed
> 
> 
> > -----Original Message-----
> > From: Doron Bustan [mailto:dbustan@freescale.com] 
> > Sent: Wednesday, April 06, 2005 2:56 PM
> > To: Eduard Cerny
> > Subject: Re: [sv-ac] FW: P1800 AC issues
> > 
> > Hi Ed,
> > 
> > can you say what is the mentis number of #217
> > 
> > Thanks
> > 
> > Doron
> > 
> > Eduard Cerny wrote:
> > 
> > >Hello Faisal and all,
> > >
> > >We went (Surrendra and I) through the issues listed under AC 
> > on the spread
> > >sheet. Please find below an initial analysis.
> > >
> > >Best regards,
> > >
> > >ed
> > >
> > >----------------
> > >#20: The return value should be defined as a single bit 
> > unsigned bit type
> > >with
> > >the value 0 as false and 1 as true.
> > >True and false are defined in the first paragraph of 18.4 for other
> > >purposes. 
> > >Also, 'define true 1 is defined on pp. 215.
> > >
> > >#92: There seems to be no issue here. Please see mantis item 508.
> > >
> > >#209: Change the example to use "assert property" instead of 
> > "assert" only.
> > >
> > >#217: Since it deals with formal semantics, perhaps John 
> > could look at
> > >this... :-)
> > >
> > >#218: I think that the author has a confusion in how 
> > properties are used.
> > >The property in itself does not imply either always or once 
> > only, it is only
> > >when placed in an assert and then in either initial or 
> > optionally always
> > >where it gets its evaluation quantifier.  
> > >I am not convinced that these additional verification 
> > statements are needed.
> > >
> > >#220: This is a syntactic sugar which could be added. But, 
> > the user has the
> > >option to define p_imply(p1, p2) as (not p1) or p2, and 
> use that as a
> > >primitive. Since it is an enhancement, it should be done in 
> > the future.
> > >
> > >#221:  @(1'b1) would never trigger. Also, to refer to the 
> > context clock can 
> > >be achieved by passing the external clock name as the actual 
> > argument 
> > >to a property instance. It seems that this enhancement is 
> not needed.
> > >
> > >#222: This is already allowed. tf_port_list includes this.
> > >
> > >#284: The value of the number of clock ticks should be 
> non-negative.
> > >Correction is needed.
> > >
> > >#241: It seems that any other sampling than #1step (the 
> > default) should
> > >produce an error. Resampling a sampled value could lead to 
> > confusion of what
> > >exactly the value is.
> > >
> > >#128: I could not find what the problem is in 8.4.1. Please 
> > refer to mantis
> > >item 408. Perhaps John could look at it...
> > >
> > >#210: This is already corrected in D4.
> > >
> > >#211: Already corrected in D4
> > >
> > >#212: Corrected in D4, also the proposed correction is 
> > actually incorrect.
> > >
> > >#213: I do not think that the ; is missing because pass_stat 
> > could be begin
> > >... end with no ;. Perhaps define that pass_stat and 
> > fail_stat are general
> > >statements? Or add the ; ?
> > >
> > >#214: Should be corrected.
> > >
> > >#219: Editorial correction?
> > >
> > >#266: Editorial correction?
> > >
> > >----------------
> > >
> > >
> > >  
> > >
> > 
> > 
>