Subject: Accellera FV -- February 2001 Meeting Minutes
From: Harry Foster (foster@rsn.hp.com)
Date: Mon Mar 05 2001 - 06:42:56 PST
Attached are the minutes from our February meeting. Thanks
Erich!!!
Also, I would like to propose an aggressive goal for selecting
the basis (i.e., a starting point) of our property
specification language from the various contributions by
our July meeting. That gives us five months. After we
select the basis of our language we would then decide what
elements from the other languages we would want to combine,
and work on the details of formalizing the final language.
We can discuss this in our next meeting.
-Harry
==============================================================
OVI Formal Verification Working Group Meeting
7 February 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);
(aaaaa) Carl Pixley (Motorola) *
(--a..) Chris Browy (Avery Design)
(raaa-) Cindy Eisner (IBM) * (Baruch Stein)
(a-aaa) Claudionor Coelho (Verplex) *
(aaaaa) Danny Geist (IBM) *
(aaaaa) Ed Clarke (CMU) *
(aaaaa) Erich Marschner (Cadence) *
(aaaaa) Harry Foster (HP) *
(aaaaa) Hillel Miller (Motorola) *
(-aaa-) Jayaram Bhasker (Cadence) *
(aaaa-) Matthew Morley (Verisity) *
(aa...) Michael Siegel - Siemens CT
(aaaa-) Mike McNamara (Verisity) *
(a---a) Peter Flake (Co-Design)
(aa...) Prakash Narain - RealIntent
(raaa-) Shoham Ben David (IBM) * (Abigail Orni)
(raaaa) Tom Anderson (0-in) * (Ping-You Sp?)
(-aaaa) Tom Fitzpatrick (Cadence) *
(--a-a) Vassilios Gerousis (Infineon)
(aaaar) Yaron Kashai (Verisity) *
(aaaa-) Yaron Wolfstal (IBM) *
No longer active (skipped last three meetings):
(---aa) Arif Samad (Synopsys) #
(-----) Ghassan Khoory (Synopsys) #
(---rr) K.C.Chen (Verplex) #
(-----) Sudhir Kadkade (Silicon Forest Research) #
(---rr) Swami Venkat (Synopsys) #
(----a) David Giramma (Synopsys) # (definite)
Agenda
======
Meeting Agenda:
(1) Language Contribution Status
(2) Ed Clarke's update on his effort to collect
properties that engineers might like to
express in a property.
(3) Overview of various model checking
models of computations:
(a) Carl on Kripke Structures
(b) Yaron (and Matthew) on edge-labeled
transition systems.
(4) Figure out how to apply these concepts
to our property specification language
requirements
(5) Decide what the focus of our next meeting
will be.
Summary
=======
(1) Contribution Update
No news from the IBM side. Motorola's letter has been signed by OVI;
internal approvals are being obtained. Once the submission is completed,
the document will be distributed to committee members for purpose of
standards work only, as with Verisity document. Harry will check into
status of other submissions.
(2) Ed Clarke's Property Library
We discussed the fact that Ed has not received much input from the group,
and the problems associated with getting approval to release IP (such as
property definitions) for use outside a company. Ed mentioned a web site
that has some good information about property specification - see
http://www.cis.ksu.edu/santos/spec-patterns/. Harry suggested a way around
the IP problem, by generalizing to templates rather than releasing specific
checks.
(3) Models of Computation
Carl described Kripke Structures and how they relate to Motorola's internal
language. (See Discussion, below, for details.) Yaron presented his
slides on Labeled Transition Systems. (see pdf file that was distributed).
We began to discuss whether the two models were equivalent, or if not,
whether it matters which one we use as the basis of a standard language.
Ed expressed some concerns about this. Matthew agreed to talk with Ed
about the tradeoffs involved in the two models and report on this at the
next meeting. It was also suggested that methodology goes hand-in-hand
with the computational model, and that we need to discuss this also.
Discussion
========
1. Update
?? - IBM - no news from board - assuming that terms of submission are those
in the letter that has been sent to OVI board...
CP - Motorola - letter sent to OVI has been signed by Dennis Brophy; being
FedExed back to Carl - in parallel, internal approvals have been obtained
CP - letter has to be signed internally (in Chicago), then donation and
letter will be sent to OVI
HF - we have Verisity donation already distributed; how will we handle Moto
contribution?
CP - same way - distribute to members of committee, for purpose of this
group only, no further distribution
HF - so we won't put it on the web page
YK - agree - also note that we have submitted paper on Sugar to (ICCAD?)
HF - will look into other submissions status
2. Property library
HF - Ed has not gotten much input; has found a web page - will email out
the URL
CP - a note - lack of input is not from lack of effort; proprietary issues
at Moto, IBM, HP are inhibiting
EC - it is important to collect a list of properties for judging languages
CP - we all agree; default in most companies for IP export is "NO"
EC - web site has a collection of properties on it -
CP - were these properties used in industry, or is it academic?
EC - were used for model checking, maybe more for sw than hw
HF - I have a design w/ 1500 properties - can't give out the specific
checks, but can create a class of checks ..
EC - yes, templates would be sufficient
PF - where is the web site?
HF - will email it to the group (see
http://www.cis.ksu.edu/santos/spec-patterns/)
3. Models of Computation
HF - Yaron, you sent a huge file to the group, but we are having computer
problems at cds.org ...
YK - that was a 390K pdf file
HF - got notice that it overflowed some buffer size - please send it to HF
directly for redistribution
HF - something generally wrong with the server - web pages are gone, etc.
CP - will start - no foils
Carl:
- Kripke structures
- a graph (states, arcs, with labels on states)
- assumes a global clock, even for asynch models
- samples signals, goes to another state
- for synchronous design some problems
- synch design assumes that all latches together determine state
- have to handle clock gating
- for larger systems need to handle several clocks
- handle today with "finest" clock
- experimenting with other methods
- paradigm is block structured language w/ prominent clock
- at IC level, dealing with synchronous designs
- can fake asynch by allowing non-determinism...
- like taking a snapshot of design at various times
-problems ...
- tools are model=checking, simulation based
- same info passed to both tools
- issues are
- capacity - problem if you model at a low (fine-grained) level
- comes up in running MC at the RTL level
- finer clock allows faking of asynch, but raises capacity problem in
RTL MC
- applies to MC of modules, blocks, units; less so at more abstract
levels
- want to check what is actually implemented in silicon
- so RTL is golden model
- paper (Mar 99) describes methodology
- requires 4 things
- design
- formulas (BCV - about to disclose)
- constraints (relate design current state to design inputs)
- paper ICCAD 99 for doing this
- set of initial states
- from this we can generate simulations ad inf., starting at initial
state, modulo constraints etc.
- also MC formulas to see if there is a violation
- uses constraints as assumptions
- questions:
- how is the non-determinism in constraints interpreted in simulation? as
random choice?
- if so, is this practical?
- most simulations are huge - much larger than formal verifiable
- yes, simulations derived from this methodology work in practice
- directed simulation not sufficient to get bugs out
- identify control-oriented parts and (apply this method)
- about 10/1 win over directed simulation
- simulation-based verification is more effective at early stages
- find a lot of bugs quickly
- when logic matures, formal verification works better at finding bugs
- HF - is there a concept of coverage related to this methodology? Sim?
MC?
- CBV language submission contains discussion of coverage
- block- str, hierarchical - makes sense to talk about coverage of
various branches
- FV tends to address one branch at a time
- coverage may be full or bounded
- there is no one perfect notion of simulation coverage
- EM - are constraints both combinational and sequential?
- constraints are all combinational, but may be dependent on auxiliary
FSMs (e.g., monitors)
- tool will accomodate either
- good methodology - write total spec with CBV, NOT reference internal
signals with properties
- implies instantiating monitors
- each clock cycle solves constraints efficiently - see paper
- yes, dead end states can occur - in which case we stop simulation
with error
- existence of dead end states is important debugging case
- dead end states indicate errors in constraints
- model checker also looks for this
- EC - will standard include a methodology along with the language?
- it would be to our advantage do so
- we need to demonstrate that the language works with at least some
methodology
- what do other people think?
- Y?: we view simulation and formal verification as part of the same
flow ...
- YK: methodology arises from combination of language and tool used;
a language can support many tools/methodologies
- YK: consider semi-formal methodology vs. fully-formal methodology
- important that we not limit ourselves to a single methodology/approach
- DG - can we contribute methodologies along with languages, and take
commonalities?
- yes,...
- a point - verification assets are mostly designer's knowledge
- tool/language/method must fit into flow easily
- CBV is Verilog-like for a good reason
- DG - but cross-fertilization is productive
- EM - significance of labels?
- Kripke structure is math model for defining semantics of a language
(inc. temporal languages)
- labels are usually properties of states
- kind of obscured ...
- lables represent properties - multiple per node
- also can have labels on edges
- HF - what about expressibility? difficulties expressing anything with
Kripke structures?
- MM - KS is just unlabeled directed graph -
- EM - what is the difference? does it matter? are they easily
transformable (one to the other
and vice versa)?
- EC - should pick the most general form
- EM - but what is essential semantic difference - mapping to language?
what impact?
- YK - classical MC uses KS with labels on states
- EC - if we select a language that has labels that are single atomic
propositions,
that would be too far away from general CTL/LTL
Yaron
- presented slides - see pdf file mailed to everyone
CP - design variability = design abstraction levels?
- yes e.g., 17 diff transaction types, but all trans. conform to general
protocol
...
CP - do you assume interleaving semantics to preclude simultaneous events?
- at the low level things are simultaneous, on finest clock
- at higher levels interleaving semantics apply nondeterministically
HF - are there properties that would be difficult to express this way?
- YK - a given property can be described in either system
- MM - labeled transition systems are more expressive than CTL ...
- e.g., modal mu calculus
- expressively complete
EM- - trying to get at basic question - does it matter what semantic model
we use?
CP - critical issue regarding which model is how it affects complexity of
MC iimplementation
MM - will converse with EC about what issues he has with some models ...
EM - can we come to some conclusions based upon today's presentations?
CP - perhaps MM and EC can discuss various models and report at next meeting
HF - we also need to discuss methodology?
YW - our methodology involves using Sugar to generate properties for model
checking and synthesized to monitors for use in simulation
Schedule for next meeting (Mar):
Tues 6th 9am PST.
- model checking and simulation combined
- continue discussion on computational model
All future meeting will occur on the first Tues of each month.
Roll Call:
Mike McNamara - Verisity
Matthew Morley - Verisity
Yaron Kashai - Verisity
Ping-You (Sp?) - 0in (representing Tom Anderson?)
Harry Foster - HP
Peter Flake - Co-Design
Danny Geist - IBM
Caudionor Coelho - Verplex
Yaron Wolfstahl - IBM
Hillel Miller - Motorola
Carl Pixley - Motorola
Abigail Orni - IBM (representing. Shoham Ben David)
Michael Siegel - Siemens CT
Baruch Sterin - IBM (representing Cindy Eisner)
Prakash Narain - RealIntent
Erich Marschner - Cadence
Ed Clarke - CMU
This archive was generated by hypermail 2b28 : Mon Mar 05 2001 - 06:43:31 PST