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