Subject: Accellera FV -- January 2001 Meeting Minutes (Committee Productivity Discussion)
From: Harry Foster (foster@rsn.hp.com)
Date: Fri Jan 12 2001 - 08:43:12 PST
Thanks to Erich for creating these excellent minutes.
Also, I appreciate all the committee members' discussions
and contributions during our last meeting.
-Harry
OVI Formal Verification Working Group Meeting - 9 January 2001, 9-11am PDT
Chair: Harry Foster Co-Chair: Carl Pixley
http://www.eda.org/vfv.
Attendees:
=========
Meeting attendance shown in parens: (most recent leftmost).
Key: 'a'=attended in person;
'r'=represented by replacement;
'-'=skipped;
'.'=not yet participating;
'?'=unknown;
'*' indicates voting member
(by "3 of last 4 meetings attended" rule,
see October 2000 minutes for details);
'#' indicates participants who have skipped the last
two or more meetings in a row and therefore
may be "inactive".
(--aa) Arif Samad (Synopsys) #
(aaaa) Carl Pixley (Motorola) *
(-a..) Chris Browy (Avery Design)
(aaa-) Cindy Eisner (IBM) *
(-aaa) Claudionor Coelho (Verplex) *
(aaaa) Danny Geist (IBM) *
(---a) David Giramma (Synopsys) #
(aaaa) Ed Clarke (CMU) *
(aaaa) Erich Marschner (Cadence) *
(----) Ghassan Khoory (Synopsys) #
(aaaa) Harry Foster (HP) *
(aaaa) Hillel Miller (Motorola) *
(aaa-) Jayaram Bhasker (Cadence) *
(--rr) K.C.Chen (Verplex) #
(aaa-) Matthew Morley (Verisity) *
(a...) Michael Siegel - Siemens CT
(aaa-) Mike McNamara (Verisity) *
(---a) Peter Flake (Co-Design) #
(a...) Prakash Narain - RealIntent
(aaa-) Shoham Ben David (IBM) *
(----) Sudhir Kadkade (Silicon Forest Research) #
(--rr) Swami Venkat (Synopsys) #
(aaaa) Tom Anderson (0-in) *
(aaaa) Tom Fitzpatrick (Cadence) *
(-a-a) Vassilios Gerousis (Infineon)
(aaar) Yaron Kashai (Verisity) *
(aaa-) Yaron Wolfstal (IBM) *
Agenda
======
(1) Contribution Updates
(2) Discuss Language Contribution Review Process
- Establish structure for review process?
- Possibly split into sub-committees to
review the different contributions?
- Other ideas?
(3) Discuss Property Specification Language Requirements
- Establish process to complete requirements
- Gather list of high level requirements
- Possibly form a requirements specification
sub-committee, which will take our existing list
of requirements and complete the requirements
document?
- Possibly form a usage model sub-committee?
(4) Set 2001 Goals
Summary
=======
(1) Contribution Updates
No news. IBM is waiting for approval of their letter from OVI. Motorola
is also. Dennis Brophy may be waiting for OVI Board approval. Synopsys
has not been represented at meetings recently. Verisity is waiting for OVI
to come up with a standard letter; when that occurs, they will replace
their original letter with the new one.
Action: Harry will try to contact Swami Venkat to see if Synopsys is still
willing to propose a language.
(2) Discuss Language Contribution Review Process
Spreadsheet: We agreed to evaluate language proposals using a spreadsheet
approach, to ensure that all languages are considered from a consistent and
comprehensive point of view. We decided to have each language donor
present the salient features of that language, and from those derive
categories of features/capabilities that define the columns of the
spreadsheet (where the "rows" are the languages). This does not
necessarily mean that we want the language with the maximum feature set;
size and usability will also be a factor in the evaluation. We will define
weights for the columns as we learn about the languages and the issues.
The languages will be graded on how they address the feature/capability
categories, taking into account the weights assigned to each category.
Action: Harry will create a first cut at the spreadsheet based on current
requirements document.
(3) Discuss Property Specification Language Requirements
Harry raise the issue of whether we should create subcommittees to focus on
particular issues, in order to expedite the work. A long discussion
ensued. Some agreed that a few natural subcommittees could be formed,
e.g., usage model, computational model, syntax. Others felt that these
need to be addressed in sequence anyway, and/or that they would want to
participate in all of the subcommittees, so there is no point in
partitioning. There was general agreement that we need to find a way of
focusing the discussions, in any case.
To some extent our ability to progress now is limited by our dependence
upon OVI to complete the language donation process, but there are some
things we can do in the mean time. Ed suggested that we collect examples
of properties of interest; Carl agreed that Motorola could contribute
examples. Ed volunteered to assemble a repository for such examples and
put it up on the web. The examples should be expressed in English.
In addition, we agreed to hold focus discussions in the monthly meetings on
various topics. In particular, we agreed to focus on computational models
next time, with emphasis on capability more than on mechanics. Carl agreed
to present the computational model involved in Motorola's language; Yaron
and perhaps Matthew will present the Verisity compuational model. Harry
will mail out a list of references regarding the various models prior to
the next meeting.
Action: see above.
(4) Set 2001 Goals
We discussed briefly whether we should set goals for 2001, and if so, what
kind. Long-term schedules are likely to be revised, and we are dependent
upon OVI to be able to proceed with language evaluation - but perhaps a
long-term schedule, at least in general form, would help establish a
framework for the year. We at least need to establish goals each month for
the following month's meeting. For next meeting, we should have the goal
of determining whether we need to select a particular computational model
as part of the language evaluation, or whether either/any computational
model would be acceptable. We should also have a goal of measurable
progress on collecting example properties.
Action: Harry will send out proposed goals by January 26th.
(5) Schedule going forward.
The next meeting will occur on Wednesday 7 February 2001 at 9am PST. After
that, each successive meeting with occur on the first Tuesday of each month.
Discussion
========
(1) Contribution Updates
IBM:
Yaron update - no news since last time - waiting for OVI to get back to
them to approve letter - Dennis said that OVI would forward approval -
CP: probably needs board approval -
Moto:
Carl - had a conference call with OVI lawyers, Dennis Brophy, Frank Wiler,
- drafted a letter form that should be acceptable - have had reviewed by
Frank Wiler, waiting for approval
Synopsys:
no one present, this time or last - no response from Swami
Ed: at Synopsys with Jim Kukula's FV group - different from Swami's group -
Jim has not expressed interest in OVI WG
HF: will try to contact Swami and see if they want to proceed
Verisity:
Yaron: waiting for OVI to come up with "blessed" document, then will
substitute that document for existing one
(2) Discuss Language Contribution Review Process
HF: what kind of process should we put in place for review -
teleconference, email, subcommittees, ?
HF: Carl, what will you do when approved:
CP: distribute document with restrictions, for comments by committee members
HF: we are coming up with requirements document as criteria, but how do we
apply?
??: do we pick one language, or features from several?
YK: we need to become educated on the various languages first
YK there will be some similarities and outstanding features - need to
discuss strengths and weaknesses
HF - so we distribute documents, review, then set up a web presentation for
donors to go through high points
YK - yes we should get together and talk about these things - they are all
complex beasts
CP - went through similar effort at Motorola - wound up with a spreadsheet
comparison - finite number of attributes to compare
MM - defining a spreadsheet could weight the decision
EM - but requirements should be defined (and lead to spreadsheet
categories) independent of language
HF - to recap - we review languages first, then decide on categories, then
get together and grade languages
CP - grading will be hard, but idea is to be comprehensive - with
weightings provided later
EC - have each donor propose special features of his language
EM - objected to features vs. capabilities
EC - then propose capabilities instead
HF - I like the idea of proposing key features
YK - it is the users of the language who ought to be proposing the
capabilities/features that the language ought to provide; it is not the
role of the people who are pushing a given language
EC - still a good idea
EM - does this mean we are after maximum features in the language?
CP - not necessarily - we should decide, and many features sometimes
reduces usability
EC - agreed - examples are Algol and Ada
CP - but we do need to look at features that could be possible
HF - check: will donors agree to provide features?
CP: Yaron, can we do that?
YK - I would rather propose categories for the spreadsheet
HF - don't quite understand ...
YK - "the feature list I prepare should not play against me" (?)
CP - two ways to start: submit languages and derive lists; or submit lists
with languages
HF - should be both
EM - reqs and spreadsheet are identical but for form
CP - we decided last time to go down a different path - not clear we can
develop reqs independently
EC - last time I heard about Moto language was at DAC - ...
...
HF - I will make a first draft of spreadsheet based on what we have in reqs
now - will supplement as we go
(3) Discuss Property Specification Language Requirements
HF - some concerns about how we are collecting requirements - should we
split into subcommittees?
YK - cannot accelerate this - everyone is monitoring everything
CP - can we group requirements - syntax, computational model, others?
HF - yes, and usage model - so there is some opportunity for subcommittees
EM - has any separate discussion about this occurred?
HF - some email from D.Geist about usage model comments
DG - I expected some reaction - we don't have to limit ourselves to these
meetings
HF - subcomms will be effective - question is when
EM - subcomms will enable deadlines and encourage participation
HF - point - do we want to set some deadlines - e.g., by DAC?
EM - can we make progress before all language docs are available?
HF - we can address broad goals like finishing reqs. doc by DAC
YK - based on language features?
HF - yes - unless you think legal stuff will finish soon
YK - not in our control
CP - like the idea of setting goals, and smaller groups
EC - what would the subcoms do - study the until operator? - prop language
should be small
HF - so should we make some goals or just proceed without them ...
CP - we suggested 3 subcomms - syntax, comp model, usage model - would be
good to get requirements from each area and report from subcomm -
YW - how does subcomm report back to committee? does committee have to
accept, or discuss?
HF - committee as a whole must make decisions
YW - OK
JB - subcomm makes proposals, then committee considers proposals - leaders
are those with good ideas in these areas
YK - we have a small number of participants who have interests in all 3
areas - prefer to continue as is
JB - but we are not making ...
EC - but we can't break things up
EM - but let's get discussion focused in any case - non-membership, focused
topic meetings
HF -
EM -
HF - for focused meetings, we need leaders
CP - what is the proposal
EM - identify topics, hold separate discussions attended by anyone
interested (w/ no impact on voting), report back next month
CP - sounds good
YK - too aggressive - one a month - share your frustration, but we can't
accelerate immediately
HF - alternative - at every monthly meeting, we pick a topic and focus on
defining requirements in that area
JB - in synthesis group, task leaders often don't have time in a given
month to work on standards, so we need to be flexible - partition into
tasks, schedule monthly meetings to address whichever task has made progress
YK - don't see how it will work - any individual proposal will not be
acceptable to group
EM - are you saying ...
YK - no, focus discussions will be a good thing until we have all donations
available
HF - can we at least define important topics, with discussion leaders,
towards requirements definition?
EC - different suggestion re: reqs. definition - everyone propose
properties of HW (in English) that we ought to be able to check - then we
can evaluate how difficult it would be to express those properties in each
language
EM - nice idea - HFs is also -
EM - should do this survey as a reality check - real properties of real
hardware
PN - see this as an evaluation mechanism - doesn't replace analyzing syntax
or usage model
EM - agree
EC - agree - but we should undertake this exercise - more objective approach
PN - like Bhasker's proposal - split into subcommittees; make progress by
coming up with a proposal, then discuss and modify - person objecting to a
proposal should propose a solution
EC - don't see how that can work - most basic thing is model of computation
- must decide that before deciding e.g. operations
PN - not necessarily - can correct later if there is conflict between
subcommittees - proposals are not final
HF - if there is an order in which we should be trying to establish thes
reqs, Ed, should we start with model of computation?
PN - but what is the purpose of ex if we do not have examples of properties
that users want to express at the same time?
EC - I do agree that collecting properties that need expression - large
number of them - might give guidance even about model of computation
PN - is there necessarily an order - I think they can be started in
parallel - doing everything in parallel will keep us here for the longest
time
TF - need to go, but 2 cents - 3 tasks, should be 3 subcomms - I think
first subtask is to look into dependencies and determine ordering reqs.
CP - we have a lot of properties related to Motorola designs - can put them
into English
CP - only danger is that properties need to be grounded in reality ...???
HF - yes - but some properties (e.g., liveness) might be not expressed
because they are difficult or expensive
CP - yes but it should be OK to include any kinds of properties (of real
HW) that you would like to check, even if you can't
PN - can we come back to
MM - we should in any case set the agenda for the next meeting, so people
can do some homework - may be go around table ...
YK - but are we going to synthesize, or select, a computational model
CP - we've suggested a edge-labeled transition state transition graph, more
familiar with Kripke structures
HF - should we focus on computational model at the next meeting?
EM - yes, but requirements - use model issues - not on proposing a
computation model itself (some of us (I) don't have the needed expertise)
EC - what are requirements?
EM - for example, need for X and Z in properties
...
EC - we can start collecting properties and discussing computational model
(requirements) in parallel
MM - ...
HF - we need a mechanism to focus discussions
YK - pick one topic and discuss it in large group to the point where it is
detailed enough to hand off to a subcommittee
CP - I would be willing to submit some properties to discuss; would think
that IBM, Verisity, etc. would be able to do this also
CP - maybe this would be a good way to just START!
EC - would be willing to serve as a repository -
EM - could it be on the web?
EC - yes, we'll do that - will ask Synopsys, students, Moto, IBM, Verisity,
etc. - should be fairly clearly stated in English
HF - please send out email to committee summarizing this and explaining how
you would like the information submitted
EC will send email to HF who will forward
HF - what about next meeting - how to focus discussion?
CP - can someone lead a computational model discussion?
EM - Carl , can you present yours, and someone else present others?
EC - two major contendors - Kripke structure (Moto, IBM); edge-labeled
transition structure (Verisity)
PN - can we circulate some material before the meeting?
EM - there is some stuff on the web - search
HF - I'll mail out some references, including Ed's book
CP - is there any reference on edge-labeled transition structures from
Verisity?
YK - risk is that we will start a technical argument rather than addressing
real user requrements
EM - can we focus on power of different models instead of mechanism?
YK - will put together a little presentation on Verisity comp model
HF - summary:
EC will coordinate collecting properties
next meeting on models of comp
CP on Kripke Structures
YK (and Matthew?) on edge-labeled transition systems
(4) Set 2001 Goals
EM - need to establish deadlines, or goals
HF -
discussion
HF - by 26 Jan I will email out goals for next meeting, and goals for 2001
- for discussion
PN - what is timeframe for achieving something as a committee
EM - need to answer next time "does it matter which model we use, and if
so, why"
EM - also want to see report on collecting properties
MM - any progress on requirements document?
HF - no
Schedule for next meeting (Feb):
Wed 7th 9am PST.
All future meeting will occur on the first Tues of each month.
Roll Call:
Tom Anderson - 0-In
Erich Marschner - Cadence
Carl Pixley - Motorola
Cindy Eisner - IBM
Harry Foster - HP
Hillel Miller - Motorola
Yaron Kashai - Verisity
Yaron Wolfstahl - IBM
Shoham Ben David - IBM
Ed Clarke - CMU
Michael Siegel - Siemens CT
Danny Geist - IBM
Matthew Morley - Verisity
Tom Fitzpatrick - Cadence
Prakash Narain - RealIntent
Mike McNamara - Verisity
Bhasker - Cadence
This archive was generated by hypermail 2b28 : Fri Jan 12 2001 - 08:47:48 PST