Subject: Accellera FV -- December 2000 Meeting Minutes
From: Harry Foster (foster@rsn.hp.com)
Date: Thu Dec 14 2000 - 14:25:36 PST
OVI Formal Verification Working Group Meeting - 5 December 2000, 9-11am PDT
Chair: Harry Foster Co-Chair: Carl Pixley
Attendees:
=========
Meeting attendance shown in parens: (this mtg, prev(this mtg),
prev(prev(this mtg)), prev(prev(prev(this mtg))) ) .
('a'=attended in person; 'r'=represented by replacement;
"-"=neither; '?'=unknown)
(-aa--) Arif Samad (Synopsys)
(aaaaa) Carl Pixley (Motorola)
(aa-??) Cindy Eisner (IBM)
(--a??) Claudionor Coelho (Verplex)
(aaa??) Danny Geist (IBM)
(--a??) David Giramma (Synopsys)
(aaa??) Ed Clarke (CMU)
(aaa--) Erich Marschner (Cadence)
(---??) Ghassan Khoory (Synopsys)
(aaa??) Harry Foster (HP)
(aaa??) Hillel Miller (Motorola)
(aa-??) Jayaram Bhasker (Cadence)
(-rraa) K.C.Chen (Verplex)
(aa-??) Matthew Morley (Verisity)
(aa-??) Mike McNamara (Verisity)
(--a??) Peter Flake (Co-Design)
(aa-??) Shoham Ben David (IBM)
(---??) Sudhir Kadkade (Silicon Forest Research)
(-rr??) Swami Venkat (Synopsys)
(aaa??) Tom Anderson (0-in)
(aaa--) Tom Fitzpatrick (Cadence)
(a-a??) Vassilios Gerousis (Infineon)
(aar??) Yaron Kashai (Verisity)
(aa-??) Yaron Wolfstal (IBM)
Language Contribution Status:
=======================
IBM -- Submission made under modified technology
letter--waiting for Accellera board approval.
Motorola -- Two conference calls with Dennis Brophy
and Frank (OVI Attorney)--agreed with Motorola's
concerns--the attorney is in the process of drafting
a new letter.
Vassilios -- Any new letter must be agreed/approved
by the committee.
Yaron -- Everyone should sign the same letter.
Requirements:
===========
In this meeting, the committee began the process of
establishing requirements for a property specification
language. As a starting point for the discussion,
Harry sent out a draft copy of a Requirements Document.
The committee agreed that the references to the Open
Verilog International (OVI) should be dropped from the
requirements document--and the new name Accellera used
exclusively. Furthermore, the committee agreed that
the new Property Specification Language (PSL) should be
compatible with both Verilog and VHDL expressions. In
other words, the property language should not be tied
to any general HDL. The committee should focus on
designing a temporal language for expressing design
properties. Cindy pointed out that the syntax of
Boolean expressions is uninteresting.
A discussion followed concerning -- what the
computational model for our new language would be.
What would the language operators mean without semantics?
Ed recommended that people using the property language
could define their computational model--in other words
don't standardize the computational model. When there
are multiple models, no point in choosing one model
over the other.
Ed suggested that each company donating a language
propose an accompanying computational model.
The discussion then change directions. Erich raised the
questions -- how is a product going to use the language?
The Requirements document should contain a Usage Model
section. (NOTE: This is actually an excellent point.
Should we create a sub-committee to look into this?).
We then discussed goals vs. requirements contained
within the requirements document. The group agreed
that we should keep the section on property specification
language goals in the document. Harry agreed to work on
the wording for assume guarantee reasoning. Ed agreed to
work on a goal statement for the language's support of
abstraction. We agreed that work was needed on the language
compatibility between simulation and formal tools. (NOTE:
For our latest work on goals--and future discussions
please reference the online requirements document
at http://www.eda.org/vfv).
We then began discussing the requirements for the property
specification language. Erich suggested, for the committee
to be productive, we need to initially focus on gathering a
list of requirements for our language--without delving into
the technical issues related to each requirement. (NOTE:
I've captured the list of in our online requirements
document--please review and make corrections and to these
requirement by sending mail to our online mail reflector
vfv@eda.org. All discussions are welcomed and encouraged!).
Our next meeting will occur January 9-th at 9:00 PDT.
The conference access number will be mailed out to the group.
Please send corrections to the group -- vfv@eda.org.
Best regards,
-Harry
This archive was generated by hypermail 2b28 : Thu Dec 14 2000 - 14:29:39 PST