Subject: [sv-ac] vote to include semnatics document as an appendix to SVA
From: Faisal Haque (fhaque@cisco.com)
Date: Tue May 20 2003 - 07:54:38 PDT
The results are in The following companies voted::
Cadence
IBM
Intel
Motorola
Mentor
Novas
Sun
Synopsys
Zero-in
The result is 9 yes
0 no
0 abstains
Comments:
Erich :
"I would suggest that the new appendix actually be an appendix of the entire SV 3.1 document, rather than an appendix to the SVA section of the LRM, since appendices usually apply to documents, not sections - but exactly how this is done doesn't influence my response.
I would like to point out that inclusion of the formal semantics document is necessary, but not sufficient, to complete the definition of SVA semantics. In particular, at least the following definitional issues seem to me to be remaining:
- how procedural enabling conditions are extracted
- how clock domains and sampling rules interact with assertion semantics
- how disabling of named blocks interacts with procedural assertions in those blocks
- how unclocked semantics (in the formal definition) is represented (if at all) in the LRM semantics.
I would also like to suggest that the SVA section of the LRM needs to be rewritten based upon the formal semantic definition, so that the LRM section becomes firmly grounded in the formal semantics. This would make the LRM section much more crisp than it is today. "
Bassam:
"Agree with Eric, it should be where appendices to the whole LRM are..."
This archive was generated by hypermail 2b28 : Tue May 20 2003 - 08:01:16 PDT