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

Hi All,

I agree with most of the stated items, here's some additional input:

#284: LRM (Section 17.7.3 in D3) already states "number_of_ticks must be 1
or greater" , so this item is OK.

#241: I think there is some "mixup" here by author about sampling and
scheduling (within timestep). The question is really about sampling and I am
not sure what Ed/Surrendra are trying to say. Seems to me a clarification in
the LRM here would be to say that the *default* input skew for properties is
#1step same as clocking block default. If an assertion/property/sequence
lives in a clocking block it would follow whatever input skew sampling is
defined there for the inputs (and default is #1step in a clocking block).
Meaning if a property is not inside a clocking block it is inside a
"virtual" one with #1step. That's really it I think, no double resampling
and what not.

#128: Seems crossed out in D3...

#213: This keeps showing up over and over again, suggest we change these to
fill in actual stmt like $display success/fail seems adequate in the
context.

#219: I think you mean to say duplicate of #220 (and not needed...) plus
these are enhancements ...

**STU2: This needs to be addressed. Different tools are making different
interpretations about this issue e.g. tools with OVA legacy are assuming use
before def is ok, we need to decide either way.

#266: This needs to be addressed (not the font bit...). Champions intended
that each committee review all "note"s and see what they really mean. If
they add value they should not be "noted" but added in core and "note"
connotation removed.

Thx.
-Bassam.

--
Dr. Bassam Tabbara
Architect, R&D
Novas Software, Inc.
(408) 467-7893

-----Original Message-----
From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of Eduard
Cerny
Sent: Thursday, March 31, 2005 2:40 PM
To: sv-ac@eda.org; 'Faisal Haque'
Cc: Surrendra Dudani; 'Eduard Cerny'
Subject: [sv-ac] FW: P1800 AC issues

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?

----------------