Subject: RE: Accellera VFV November 14 Meeting Minutes
From: Armoni, Roy (roy.armoni@intel.com)
Date: Sun Nov 18 2001 - 22:47:01 PST
Hi,
The action item required from me in the meeting was: to explain Cindy what
is needed to prove that a language supports R71c and R71d.
We first need to define for a formula f the language L(f), which is the set
of all infinite traces that satisfy f.
For a Buchi automaton A, I hope that it is clear what is the language L(A).
Cindy claims that for every formula f in FL of Sugar, there exists a Buchi
automaton A s.t. L(f)=L(A). I believe that. Nevertheless, this is not the
requirement in R71c and R71d.
The requirement there is to show that for every Buchi automaton A, there
exist a formula f in the language s.t. L(A)=L(f). Moreover, R71c requires
that f would be able to be assumed. R71d requires that f would be able to
be asserted. I suspect that FL does not meet these requirements, let alone
the original Sugar that does not contain G, U and X linear operators. I
will be happy to be proved otherwise.
Regards,
Roy
-----Original Message-----
From: Harry Foster [mailto:harry@verplex.com]
Sent: Wednesday, November 14, 2001 11:47 PM
To: vfv@eda.org
Subject: Accellera VFV November 14 Meeting Minutes
Minutes for the Accellera meeting on 14 Nov
The following is the list of committee members who identified themselves at
the beginning of the meeting. There were a few addition people who joined
us during the first presentation--so please send me email and I'll add your
name to the list:
am2@transeda.com
Bassam@novas.com
bdeadman@sdvinc.com
bywang@verplex.com
cpixley@synopsys.com
dana@wisdom.weizmann.ac.il
dudani@synopsys.com
dvc@verisity.com
eisner@il.ibm.com
erichm@cadence.com
flake@co-design.com
geist@il.ibm.com
harry@verplex.com
havlicek@adttx.sps.mot.com
hillelm@msil.sps.mot.com
kareny@galileo.co.il
ken.albin@motorola.com
limor.fix@intel.com
mac@verisity.com
matthew@verisity.com
michael.siegel@mchp.siemens.de (represented)
roy.armoni@intel.com
shoham@il.ibm.com
tla@0-in.com
vardi@cs.rice.edu
wolfstal@il.ibm.com
yaron@verisity.com
1. Language Presentations
Short presentations from each donor, in reverse order:
1.1 Intel Presentation - Roy Armoni
- ForSpec 1.0 donated to Accellera
- ForSpec 2.0 developed with Synopsys, CoDesign, Verisity
- to be compatible with Verilog, SuperLog
- to address Accellera requirements
- continuing to address syntax issues in embedding into 'e'
- ForSpec 1.0 meets all requirements except
- R2a - binding to Verilog Boolean exprs
- R20a - support for && of regular expressions
- R37a - abstract clocks - end of sequential event
- all addressed in ForSpec 2.0
- see slides for further info
questions:
- definition of && - not the same as Sugar's && - implications?
- definition of 'latched end-of-event' not clear
- support for "more than one language" - Verilog and Superlog
Erich to pose question to Intel (IBM, etc.) re: meaning of && in
static/dynamic contexts - various examples
1.2 Motorola Presentation - John Havlicek
Plain text presentation of how CBV addresses requirements.
Note: comments that "CBV will not be modified to address" 25a, 52a, 65a,
71c, 71f was too strong; this statement may be true w.r.t. Motorola's
internal implementation, but it could be modified to address these
requirements as part of a standard.
Other requirements that are not met are straightforward to address.
see presentation
CBV Strengths - notes
4. - implication for model checking is that initial states have self-loops.
6a. - others can use their own stimulus mechanisms in place of "patented
Motorola mechanisms".
Extensions needed:
R1e - binding to VHDL expressions (or some other language) would be easy to
add.
R7b - easy to add.
R25a - "eventually" is not composable; don't want to make it so for
internal methodology; but this could be done for a standard. (no proposal
yet)
R27a - closure under negation - no negation operator in CBV, but (under a
different item) extensions can make it omega-regular, so this would follow.
R34a - level sensitive clocks - not clear what the requirement is
R46a
R52a - can handle checks at finest successive sampling points, but not in
between
R65a - efficient support for negation/complementation of properties -
R71b - assumptions for case splitting - can add this, as well as an
exhaustiveness check
R71c - CBV only supports simple assumptions, not assumption of general
formulae; this allows use of assumptions in various ways
R71d - not clear whether CBV does or does not support omega-regularity;
"limit task set" extension would be sufficient to ensure this
R71f - assuming every assertion - internal methodology wants simple
constraints for flexibility, so this is not currently supported
1.3 IBM Presentation - Cindy Eisner
see presentation (slides)
Notes:
Sugar FL will work with EDL just as original Sugar does.
questions:
slide 7 - will path quantifiers be dropped? No - they will be optional
slide 8 - so can I just drop the path quantifier? No - dropping E
quantifiers would
so now you are switching to LTL? No - support both CTL and LTL
[did Intel ever add an option to switch to branching time? No]
how does this meet R71e,f if the path quantifiers are still there? FL
supports this.
does FL include regular expressions? Yes
is the FL closed under negation? Yes
how will FL support omega-regularity? FL is omega-regular.
but 71c requires support for ANY omega-regular language.
Action item:
Roy to email Cindy re: how FL really supports ANY omega-regular language.
1.4 Verisity Presentation - David Van Campenhout
Presenting original donation (Temporal e) plus additional constructs from e
language that have been used in examples - appropriate because scope of the
committee's goal has broadened.
see presentation
Requirements are either met
- explicitly in language definition
- subjectively (indication is user base)
- via additional constructs in e
or could be met
except that R16b seems to be not useful and not supported
open to unification of various languages proposed - working with Intel,
IBM, etc.
Note that R12b was a tie and was dropped as a result.
===================
2. Requests for Accellera documents
Harry has had several requests for the examples document. After
discussion, we agreed that theyand the language definitions will not be
distributed outside the committee.
3. Voting process
What are we voting upon? original proposal or the proposed modifications
of the languages? We intended to consider not only how each language as
originally donated meets the requirements, but also how each language could
be extended to meet the requirements. Each of the four donors has
addressed this, some to the extent of proposing changes now. We should
consider these proposed changes in the ballot, and therefore should take
time to study them. (Motorola would also like to make a detailed proposal
regarding how it would extend CBV.)
We decided that all documents to be considered in the ballot must be
distributed to the committee by end of Monday 19 Nov. In particular this
will include a detailed response to each requirement from Intel and IBM
(along the lines of the responses by Verisity and Motorola). Motorola also
plans to submit additional information on extensions. Other submissions,
if any, will also be accepted up until the same deadline.
Schedule going forward:
19 Nov - all docs rec'd; email Q&A period begins
3 Dec - email discussion complete; round 1a ballot begins
10 Dec - round 1a ballot ends
11 Dec - Harry will summarize results
12 Dec - round 1b ballot begins
17 Dec - round 1b ballot ends
18 Dec - Harry will summarize results
19 Dec - next meeting
The votes will be cast as follows:
- round 1a
- each voter gets three votes, to be cast for three of the four
languages - no abstentions, no overlap
- round 1b
- each voter gets two votes, to be cast for two of the three
remaining languages - no abstentions, no overlap
Votes will be sent ONLY to harry@verplex.com. Harry will publish all votes
with the summary.
Big thanks to Erich for capturing the minutes. Thanks to all the presenters
at today's meeting. I feel that today was a very productive meeting.
Best regards,
-Harry
---------------------------------------------------------
Harry Foster Tel 972-423-3186
Chief Architect Cell 408-464-6406
Verplex Systems, Inc. mailto:harry@verplex.com
300 Montague Expwy, Suite 100 www.verplex.com
Milpitas, CA 95035 www.verifiableRTL.com
This archive was generated by hypermail 2b28 : Sun Nov 18 2001 - 22:48:25 PST