Subject: [sv-ac] FW: notes on Q&A on the OVA presentation, subsequent discussion
From: Erich Marschner (erichm@cadence.com)
Date: Thu Sep 19 2002 - 18:19:12 PDT
Additional minutes that were left out of the first batch ...
-------------------------------------------
Erich Marschner, Cadence Design Systems
Senior Architect, Advanced Verification
Phone: +1 410 750 6995 Email: erichm@cadence.com
Vmail: +1 410 872 4369 Email: erichm@comcast.net
| -----Original Message-----
| From: Erich Marschner
| Sent: Thursday, September 19, 2002 1:28 PM
| To: 'Faisal Haque'
| Subject: notes on Q&A on the OVA presentation, subsequent discussion
|
|
|
| Notes on the OVA Presentation
|
| - Slide 2 : Synopsys donated OVA 2.0
| - Slide 3 : Synopsys support for OVA
| - Slide 4 : OVA Features
| - Slide 5 : Hierarchy of Temporal Assertions
| - Slide 6 : Boolean Expressions - Operators
| - Slide 7 : Expression Definitions
|
| AK: What does 'bool' definition provide additionally? Is it
| just to name a larger boolean expression?
| SD: Yes, it is just a macro, but more powerful/convenient.
| Discussion about whether it is really more powerful - can do
| the same thing with `defines
|
| - Slide 8 - Sequence Expressions
|
| Discussion about "* 8" - should be "* [8]"
|
| Discussion about "length [10]" - clarified.
|
| - Slide 9 : Sequence Expressions - Free variables
|
| Discussion of the example - confusing
| Essential point seems to be that dynamic information is used
| in the definition of the assertion. (Or perhaps just that
| you can build an auxiliary state machine and refer to it in
| a formula.)
|
| - Slide 10 : Formula Expressions - LTL Based
|
| - Slide 11 : Formula Expressions with Events
|
| Discussion about meaning of "followed by".
|
| - Slide 12 : Formula Expressions - Resets
|
| Discussion about the need for dual operators - SD says it is
| necessary to have duals for closure; CE says that it is not
| necessary because you can invert any property; SD says that
| it is easier having the dual, because you don't have to
| think; CE says that duals aren't always useful - e.g., no
| dual for implication; RA says that AND is the dual of
| implication; PN asked where this discussion is going ....
|
| - Slide 13 : Multiple Clock Definitions
|
| Discussion of synchronization mechanism
|
| - Slide 14 : Binding to Design Objects
|
| AK: any difference between module and scope construct?
| (I.e., could distinguish based on name rather than keyword)
|
| - Slide 15 : Assertion Directives
|
| AK: so if you delete a keyword, it only checks for one
| cycle? SD: yes - globally. AK: what is the value of that?
| SD: to write properties about the initial cycles
| AK: we are discussing whether assertions can be used as
| assumptions - what is the model here? SD: assertions and
| assumptions are specific; if you want you can use 'property'
| (which is not in the donation).
|
| EM: if 'property' is not in the donation, what is it in?
| what else is missing? SM: the donation is OVA 2.0; we are
| continuing to work beyond that.
|
| Discussion of difference between assumption and restriction
| - PN: is there a clear definition of what this means, that
| an assumption must be verified? SD: it is a control
| mechanism for the tool that people use.
|
| - Slide 16 Building library
|
| SM: to clarify - donation does not include checkers library
| - Synopsys has built them, but they are not part of the donation
|
| - Slide 17 : Template library - Simple Example
|
| AK: is this the simplest way to write something like this?
| SD: this is just an example.
|
| - Slide 18 : OVA Donation Summary
|
| AK: what kind of "users of verification tools"? SD: various
| tools ...
|
| AK: is the formal semantics definition part of the donation?
| SM: was not part of the documents that were donated. SD:
| we have it on the web site. AK: one of the requirements was
| that the language be formally defined. PN: final language
| must be formally defined. SM: the language will change -
| will take an action item to make the formal definition available.
|
| Faisal - any more discussion on the donation?
| Prakash - yes, so far the presentation has been one way
| Faisal - we can discuss in the next meetng
| Prakash - discussion in next meeting should be restricted to
| whether the donation meets the criteria for acceptance
|
| David Lacey: in the vote whether to accept the donation, if
| we accept, what is the result of that? just that we can use
| it as one of the pieces that forms the ultimate SV language?
| or that it is the basis for the ultimate language?
|
| Faisal: I understand it to mean that it is a resource for
| us to use; it is not guaranteed that it will be the only resource
|
| David: There was some discussion earlier about what OVA
| offers that Sugar does not - was that done? It would be
| nice to have a side-by-side comparison...
|
| Discussion about having a side-by-side presentation next week ...
|
| Resolution:
| - Cindy to give brief presentation on Sugar next week (30 minutes)
| - Steve and Erich to give side-by-side comparison next
| week (30 minutes)
| - finish discussion on remaining requirements
| - start both ballots (requirements, donation) by email
| right after that meeting
| - finish by the week after (Oct 2)
|
|
| -------------------------------------------
| Erich Marschner, Cadence Design Systems
| Senior Architect, Advanced Verification
| Phone: +1 410 750 6995 Email: erichm@cadence.com
| Vmail: +1 410 872 4369 Email: erichm@comcast.net
|
This archive was generated by hypermail 2b28 : Thu Sep 19 2002 - 18:24:55 PDT