Subject: Accellera FV March 6th Meeting Minutes
From: Harry Foster (foster@rsn.hp.com)
Date: Wed Mar 07 2001 - 12:10:20 PST
Attached are the minutes for our March 6th meeting.
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);
(-aaaaa) Carl Pixley (Motorola) *
(araaa-) Cindy Eisner (IBM) *
(-aaaaa) Claudionor Coelho (Verplex)
(aaaaaa) Danny Geist (IBM) *
(-aaaaa) Ed Clarke (CMU) *
(-aaaaa) Erich Marschner (Cadence) *
(aaaaaa) Harry Foster (HP) *
(aaaaaa) Hillel Miller (Motorola) *
(--aaa-) Jayaram Bhasker (Cadence) *
(a.....) Limor Fix (Intel)
(aaaaa-) Matthew Morley (Verisity) *
(aaa...) Michael Siegel - Siemens CT
(-aaaa-) Mike McNamara (Verisity) *
(aa---a) Peter Flake (Co-Design)
(aaa...) Prakash Narain - RealIntent
(araaa-) Shoham Ben David (IBM) *
(araaaa) Tom Anderson (0-in) *
(--aaaa) Tom Fitzpatrick (Cadence) *
(aaaaar) Yaron Kashai (Verisity) *
(aaaaa-) Yaron Wolfstal (IBM) *
No longer active (skipped last three meetings):
(----aa) Arif Samad (Synopsys) #
(---a..) Chris Browy (Avery Design) #
(------) Ghassan Khoory (Synopsys) #
(----rr) K.C.Chen (Verplex) #
(------) Sudhir Kadkade #
(----rr) Swami Venkat (Synopsys) #
(-----a) David Giramma (Synopsys) #
(---a-a) Vassilios Gerousis (Infineon) #
Agenda
======
Meeting Agenda:
(1) Language Contribution Status
(2) Intel FTL Presentation
(3) Discussion of Usage Models
(4) Selection date goal
(5) Plans for face-to-face meeting at CAV'01
Summary
=======
General comment: Ed Clarke requested that we hold
future meetings on either Thursday or Friday, since
Monday, Tuesday and Wednesday conflict with his class
schedule. Friday is not a good time for the committee
members calling in from Europe or Israel. Hence, we
decided to hold future meetings on Thursday.
(1) Contribution Update
IBM has completed all the legal work concerning the Sugar
contribution. Harry distributed two documents: (1) Guide to Sugar
Formal Specification Language, and (2) The Syntax and Semantics
of Sugar.
The Verisity contribution documents were previously distributed,
which include: (1) 'e' Temporal Language Reference Manual,
and (2) Semantics of Temporal 'e'. Anyone who didn't receive these
documents should contact Harry.
The Motorola letter has now been signed. Hillel mentioned
that they will make the documentation available to the committee
soon.
(2) Intel FTL Presentation
Limor Fix presented Intel's position concerning why the
Accellera FV committee should consider their request, which
is to re-open the language contribution process to include Intel's
FTL (ForSpec Temporal Language).
Carl Pixley and Harry Foster previously had a phone conference
with Limor and explained that extending the offer to contribute
would require an approval vote from the committee. Limor
presented an overview of the language. A motion to vote
on this decision will be mailed to the entire group in early
March, and the committee will vote on this decision during its
April meeting.
=-=-=-=-=-=-= Limor's Presentation =-=-=-=-=-=-=-=-=-=-=
Reasons Intel Wishes to Donate FTL:
- 10 years of experience in Formal specification for FV and
DVA lot of effort and expertise into building second
generation language (10 man-year, 5 PhDs, +Prof.
Moshe Vardi, Dr. Rob Gerth.)
- Small, elegant and powerful languageIt is free
- Intel wants to donate
Brief history of Formal Specification in Intel
- First generation language – Proto
- Proto was developed 8 years ago
- Primary developed as a language for DV (Dynamic validation) checkers and
coverage goals
- In 94 a tableau was developed for a subset of the
language -> “Proto-SMV” system
- Over 20,000 properties were developed
- Second generation language – ForSpec
- ForSpec was developed 2-3 years ago
- ForSpec was design to meet both FV and DV needs
- ForSpec is being used by several design groups
Background on ForSpec
- ForSpec is used today in Intel for:
- Specifying properties and assumptions for model-checking
based FPV
- Specifying checkers for simulation.
- ForSpec short term plans (2001)
- Use ForSpec for specifying FEV assumptions
(formal equivalence assumptions)
- Develop proof-system for ForSpec (Theorem Proving)
- ForSpec longer term plans (2002)
- Extend ForSpec for specifying coverage goals
Requirements considered while developing ForSpec
- Expressiveness:
- Modeling
- To be able to develop reference-model as spec
- To be independent of any RTL language (since we have iHDL, Verilog and
VHDL designs)
- Temporal properties
- To be able to express events over time (temporal)
- HW related constructs: Multiple clocks, rest
- Efficiency
- Need to be efficient for model-checking
- Need to be efficient for checker (over simulation)
- Compositionality
- Need to allow Theorem Proving over the language
ForSpec Overview
- ForSpec has two main ingredients:
- Declarative: New Temporal Logic, FTL
- Operational: Modeling Language
- FTL is built in four layers
- Boolean expressions
- Events
- Extended Events
- Temporal formulas
-Boolean -> Events -> Extended Event -> Temporal Formula
- FTL is the set of all temporal formulas
Additional Characteristics
- Linear temporal language, based on LTL [Pnueli]
- Rich set of logical and arithmetic operations on bit vectors
- Includes Temporal connectives over time windows
- Includes Regular events
- Includes universal quantification over propositional variables
- Includes support for multiple clocks
- Includes reset
A paper titled "The ForSpec Temporal Logic: A New Temporal
Property-Specification Logic" was distributed to the committee
members for reference and more details.
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
A discussion followed the presentation -- concerns included
slowing the selection process by adding a new language for
consideration, especially since existing contributions might
already cover features offered by this new language. In
general, the group felt we are at a point where we could
accept a new language provided the legal details are resolved
soon. Harry promised to get Limor a copy of the
donation/contribution letters -- and asked Limor to provide a
time estimate prior to our next meeting on how long it
would take Intel to complete the legal work on the letter.
The committee will vote at the April meeting whether to allow
Intel to contribute FTL to Accellera.
(3) Discussion of Usage Models
In our February meeting, Carl Pixley presented an overview of models
of computation involving Kripke structures. During his discussion,
Carl touched on the Usage Model of CBV at Motorola.
During our March meeting, Yaron Wolfsthal gave an overview of
FoCs -- IBM's methodology for using Sugar in a simulation environment.
Yaron distributed a paper to the committee that covers more details
on this subject -- titled "FoCs - Automatic Generation of
Simulation Checkers from Formal Specifications."
Yaron Kashai discussed some of his ideas concerning Temporal 'e'
in simulation as well as model checking.
The group had a discussion about how to interpret branching time
In a simulation environment. Limited to checking linear part. At
the end of simulation, the status of verifying the property is
either (a) failed, (b) conclusive, or (c) undetermined.
Harry touched on the technique he is using in his lab for verifying
at the RT-level. This includes creating a library of assertion
modules, which are instantiated in the designer's RTL during
development. Property language details are abstracted away
from the design engineer. The methodology enables the HP lab
to switch seamlessly between many different proprietary, as well as
commercial, property languages and tools. The library modules
work in simulation, semi-formal and formal verification.
(4) Selection date goal
Harry discussed his goal to select one of the languages as a
starting point or "strawman" by our July meeting. Desirable
elements from the other contributions could be rolled into
our strawman language after that point. This led
to our discussion about having a face-to-face, 1- or 2-day
meeting immediately after CAV. (See next item.)
(5) Plans for face-to-face meeting at CAV'01
Harry had a meeting with Vassilios at HDLCon this
past week. Vassilios suggested that we schedule
a face-to-face one or two day meeting soon.
The committee also agreed that we need a serious
working meeting--and the suggestion was made that
since many of us would be attending CAV, we
schedule a meeting to occur immediately after CAV.
The timing works out with Harry's goal of selecting
a strawman language by July. Between now and the
July meeting, each donating company will present the
features to the committee. During our April meeting,
we will start the process of putting together an agenda
for the CAV meeting.
NEXT MEETING: For our next meeting, scheduled Thursday April
5, we plan to vote on accepting the Intel language proposal.
In addition, Cindy was originally scheduled to present the
Sugar language. Due to a schedule conflict, Cindy will not be
able to present in April. Hence, Harry is working the details
with Motorola (or Verisity) to present their language during this
meeting. Finally, the committee will discuss the agenda for
the July face-to-face meeting after CAV.
Concerning our July CAV meeting: It would be nice if we could
find an Accellera participating company willing to host us
(e.g., an office in Paris with a conference room we could use
for our meeting). If not--maybe we could rent a conference room
close to the CAV convention center and split the cost (e.g.,
everyone attending could add the partial cost of the room onto
their expense reports)? We can discuss the logistics as well
as agenda during our next meeting.
Best regards,
-Harry
This archive was generated by hypermail 2b28 : Wed Mar 07 2001 - 12:10:24 PST