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

Hillel,

I understand that one can do that for formal but you pay higher price for
the verification. Furthermore, the language is to be synthesizabel ass is,
to also run in an emulator. I am not convinced that the user would be happy
to provide this extra clock. In any case, the issue can be debated and we'll
see, but in any case, since it is an enhancement and not errata, it would be
considered for the next version of SV.

Best regards,

ed

PS I was glad to meet you too. Only pity that we could not talk more.
Perhaps next time if and when I come to Israel or you to the US.

> -----Original Message-----
> From: Miller Hillel-R53776 [mailto:r53776@freescale.com] 
> Sent: Thursday, April 07, 2005 8:01 AM
> To: 'Eduard Cerny'; Bustan Doron-DBUSTAN
> Cc: sv-ac@eda.org
> Subject: RE: [sv-ac] FW: P1800 AC issues
> 
> Ed,
> This is what we do for the formal implementation. 
> We do not want to restrict the designers ability to specify 
> things that cross over domains. Even 
> at the price of more complicated implementations. With 
> simulation there should not be any issues 
> with the implementation.
> 
> I left Dan after lunch. Glad to have met you in person.
> 
> Best Regards,
> Hillel
> 
> -----Original Message-----
> From: Eduard Cerny [mailto:Eduard.Cerny@synopsys.com]
> Sent: Thursday, April 07, 2005 2:56 PM
> To: Miller Hillel-R53776; 'Eduard Cerny'; Bustan Doron-DBUSTAN
> Cc: sv-ac@eda.org
> Subject: 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?
> > > >
> > > >----------------
> > > >
> > > >
> > > >  
> > > >
> > > 
> > > 
> > 
>