Subject: Accellera Formal Verification -- November 2000 Meeting Minutes
From: Harry Foster (foster@rsn.hp.com)
Date: Wed Dec 06 2000 - 07:05:32 PST
================== NOVEMBER 2000 Accellera Meeting Minutes =================
Erich did an incredible job capturing the discussion. Erich suggested that
in the future we do a role call early to help associate voices with names.
This is a great idea.
I appreciate everyone contributions to our last meeting.
Best regards,
-Harry
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
OVI Formal Verification Working Group Meeting - 8 November 2000, 9-11am PDT
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)
(aaaa) Carl Pixley (Motorola) <pixley@adttx.sps.mot.com>
(a-??) Cindy Eisner (IBM) <...>
(-a??) Claudionor Coelho (Verplex) <coelho@verplex.com>
(aa??) Danny Geist (IBM) <Danny_Geist@il.ibm.com>
(-a??) David Giramma (Synopsys) <davidg@synopsys.com>
(aa??) Ed Clarke (CMU) <Edmund.Clarke@cs.cmu.edu>
(aa--) Erich Marschner (Cadence) <erichm@cadence.com>
(--??) Ghassan Khoory (Synopsys) <gkhoory@synopsys.com>
(aa??) Harry Foster (HP) <foster@rsn.hp.com>
(-a??) Hillel Miller (Motorola) <hillelm@msil.sps.mot.com>
(a-??) Jayaram Bhasker (Cadence) <jbhasker@cadence.com>
(rraa) K.C.Chen (Verplex) <kchen@verplex.com>
(a-??) Matthew Morley (Verisity) <...>
(a-??) Mike McNamara (Verisity) <mac@verisity.com>
(-a??) Peter Flake (Co-Design) <flake@co-design.com>
(a-??) Shoham Ben David (IBM) <...>
(--??) Sudhir Kadkade (Silicon Forest Research)
<Sudhir_Kadkade@sifr.com>
(rr??) Swami Venkat (Synopsys) <swamiv@synopsys.com>
(represented by Arif Samad (Synopsys) <arif@synopsys.com>
(aa??) Tom Anderson (0-in) <tla@0-in.com>
(aa--) Tom Fitzpatrick (Cadence) <tfitz@cadence.com>
(-a??) Vassilios Gerousis (Infineon) <Vassilios.Gerousis@infineon.com>
(ar??) Yaron Kashai (Verisity) <yaron@verisity.com>
(a-??) Yaron Wolfstal (IBM) <wolfstal@il.ibm.com>
A. Logistics
Erich - will take minutes
We will take roll call to determine attendance, representation, voting
members before the first vote.
Harry - got word on how to set up web page, establish email reflector -
but instructions run into HP security issues - will have IT solve the
problem in the next couple weeks
B. Previous Meeting's Minutes
Carl - noted correction to minutes - any member could request that an issue
be raised for vote by the whole group
Erich - mentioned question of "voting" member restriction
Harry - that was not what we discussed - let's vote on the unrestricted
form:
3a. Any member may request that a less significant question be reballoted
as a
more significant question, under the 80%, email procedure.
Harry proposed that we adopt the above amendment to the minutes for the
previous meeting - no objections.
C. Status of Language Proposals
C.1 Motorola?
Carl - called secretary: letter was given to attorney; called Dennis
Brophy, but no explanation - whole thing is stalled - hope to find out at
OVI board meeting tomorrow, but it is not on the agenda
C.2 IBM?
Danny - also stalled - many discussions in IBM - IBM forwarded a proposal
to Vasilios yesterday (relaxation of requirements in Transfer Letter, which
were understood to be in line with OVI basic intent) - not there yet, but
hope to get there
Carl - have IBM lawyers engaged with OVI lawyers? .... no
C.3 Synopsys?
Arif has no information from Swami
C.4 Verisity?
Yaron - as far as we know, we are done - we tried to modify OVI letter, to
no end; eventually signed letter essentially in original form (with minor
addition of OVI releasing rights back to Verisity). Ed - but negotiations
are complete, right? Y. yes.
Carl - OVI is being non-responsive - no communication.
Harry - will talk to board about this.
C.5 Language Summary
Harry - we are considering the following four languages:
IBM Sugar
Moto language shown at ICCAD
Verisity e
Synopsys language (from Swami Venkat)
Carl - any other companies that want to propose a language?
Tom Anderson - 0-in - we would have had we been members at the time
Carl - but I talked to Kurt Widdoes and .... last year - they said they
were not interested
TomA - yes, we had a change in thinking after we were notified about change
in leadership in September
Harry - any objection to another proposal?
.... - is this open-ended?
Harry - at some point we have to cut it off
Carl - 0-in should be grandfathered in
... - but we are having problems making progress anyway
Yaron - but we need to revise mechanism so we make progress
Harry - Any objections to 0-in being grandfathered in?
No objections.
Ed - what does proposing a language mean? if accepted, does that mean "as
is"? or as a starting point?
Harry - as a starting point, with proven technology around it - we would
try to improve it
Carl - it can be changed - idea is to converge on a standard, so changes
are appropriate
[further elaboration by various people]
TomA - we will end up with a composite, since all proposals are coming from
existing implementations .....
Ed - we should define Verilog semantics also,
Carl - some people think that's already defined ...
Yaron - we could partition the property language from the model language
Arif - this is a basic point - allowing the property language to be
separate from the model language
Erich - but we need to define the relationship between property and model
language semantics
Carl - there is a genuine issue here - e.g., multiple clocks in Verilog
.... - we shoujld form a subcommittee to look at building a semantic bridge
from property language to model language(s)
Harry - are we talking about an event-driven model or a cycle driven model?
Yaron - we need to consider both, as well as the formal model (more like
cycle model) - this does influence semantics of the language - would be
wrong to completely ignore it - e has many concepts that directly relate to
this - has components that are not used for formal verification
.... - lets focus on defining what we need -
Erich - we can define ideal event/cycle semantics as ideal Verilog semantic
model and map to that
Carl - are we all talking about FSM-based semantics?
... - there are other kinds of models ...
Ed - yes, there must be a state machine model - you can model asynch
systems by "stuttering" with a "standard Kripke model"
Carl - we have run into problems with asynchronous clocks - but model can't
be asynch - need fundamental clock (greatest common divisor of all
frequencies?)
Ed - asynch usually influences what queries you can ask - e.g., "next"
..... - but "next" has a reasonable interpretation - change view from
Kripke structure to a labeled transition structure ..
Ed - yes I agree - that can enable modeling of asynchronous systems - but
talking about a logic that allows for label(ed) transitions might become
quite complex
Yaron - we support that - if you abstract away some of the timing behavior,
you end up with an asynchronous system - no clock -
Ed - but in that case you don't want to maintain labels on transitions,
because then you couldn't do collapsing ...
Yaron - I think you have no choice
Ed - well you can use stuttering ... when people normally want to do state
reduction - eg., modal mu calculus - have to treat arcs specially - to
reduce number of states you need Kripke structures w/o labels on
transitions - you could also have a Kripke structure with labeled
transitions
Carl - are you proposing a semantics for the property language that
encompasses all of these things?
Yaron - yes
Ed - the property language might get out of control if too general
Matthew - are lable transition systems more expressive than Kripke
structures?
Ed - they can be - if you convert LTS into KS, that might trigger some
state splitting - but you could have both in one model
Matthew - this is not far-fetched - it is needed to allow the abstraction
of low level properties
Ed - Kripke structures with stuttering equivalence is fine for this - would
need "observational equivalence with tau actions" otherwise
Danny - can we structure the language to include a subset for synchronous
design, so that support for asynch design would not impact those doing
synch design?
Yaron - better to do the opposite - same operations for both synchronous
and asynchronous domains
Ed - that's the right idea - use Kripke structures and stuttering and omit
next operator (for asynchronous design)
Danny - e has a notion of sampling that is often implicit ....
Yaron - if it is really implicit, then you don't have a choice - sampling
expressions allow expression that signal functioning as clock varies from
state to state - way to implement stuttering or asynchronism - very
general, very low cost
Carl - what is the definition of "event" in e?
Yaron - you can define an event, can use that event to control sampling -
important because sampling needs to occur at times that are abstracted away
from the underlying synchronous clock
Danny - but for formal verification you want to focus on synchronous systems
Yaron - but this is still best, because it reduces state space
Carl - can you build transition relations with your event sampling
semantics?
Yaron - yes
Ed - it is a labeled transition system - labels are events
Cindy - but the events can be temporal expressions - doesn't that
complicate the issue?
Matthew - not a problem - they just define a state machine
Danny - but you really need to focus on synchronous design - sampling for
asynch should not affect synch properties
Yaron - fine - the sampling is just optimized out if it is not needed - but
you need the capability because many systems are not that simple
Ed - e.g., if you have multiple clocks, even in a synch system, you need
this kind of mechanism
Carl - relationship between formal engine and simulation semantics must be
equivalent
Erich - what about event-based simulation
Ed - but there is a problem - abstraction is conservative -
Erich - wont' be equiv unless we define event/cycle semantic relationship
Carl - if formal engine gives cex (in cycle model), then you must be able
to show it in (event) simulation of model
Erich - OK with that definition
Carl - we need to make a decision about whether to take a simple
synchronous approach or a "labeled transition" approach as Yaron is
suggesting.
Mathhew - the discussion came from considering the need for considering the
relationship between simulation/property semantics
TomA - is there a specification for what we are trying to accomplish here
as a group?
discussion about what question to try to answer:
Erich: can we poll preferences for supporting synch only, synch and asynch
equally, synch/asynch separate (to avoid asynch overhead affecting synch
design)
Yaron - issue is not synch/asynch, but rather whether properties are
defined in terms of one clock or multiple clocks
Danny - Yaron is depending too much on model checking
Ed - can IBM guys comment on Sugar?
Danny - We don't see multiple clocks often
Ed - Motorola?
Carl - for a single block, maybe only one clock; but when you put pieces
together, you see multiple clocks
Danny - but hide sampling from user
..... (Tom?) - can we just define a default sampling event?
Ed - what would models look like?
Yaron - you would end up with just Kripke structures
Ed - that simplifies things ...
......(Tom?) - compiler can make this decision (????)
Yaron - this is all just a front end issue
Carl - we glossed over one thing - OVI is supposed to propose standards
that vendors actually support, which in this case implies engines that can
support it
Yaron - we do run model checking ...
Carl - can I buy a model checker for e? if so, where?
Yaron - yes, people are doing this - most are public domain - Cadence
version is not out yet
Carl - I'm hearing that it is possible to compile e into a Kripke
structure, so you can use any model checker on it ...
Ed - but do you have to split states on this? i.e., pushing label into
operator (?) - can cause exponential blowup
Matthew - yes, tableaux construction ..... Formalcheck builds ....
Matthew - we don't have nested fixed point operators in temporal e
Yaron - there are some cases that would cause state explosion, but is not
common
Ed - occurs if you have arcs that are labeled with propositions that can be
negated - e.g., a, and not a, ...
Matthew - we use temporal e in a much more compositional manner - we define
events, then events became (part of) the lables on transitions - this keeps
the fsms small and minimizes complexity
Ed - but having a lot of small fsms can also cause state explosion
Ed - someone said they were'nt going to allow nested fixed points - what
about fairness constraints? that requires nested fixed points
Matthew - do you want the property language to express fairness constraints
Ed - sometimes it is outside of the language ...
Matthew - then it is not an issue
Cindy- our language is a superset of CTL - fairness constraints are used
sometimes, for liveness properties
Carl - almost everything we actually check are safety properties; we don't
need fairness at all
Bhasker - some of our customers have used fairness constraints
Ed - e.g., Req/Ack cycles are a natural for using liveness
Yaron - we are separating liveness from fairness - liveness and bounded
fairness are supported in temporal e, but not general fairness
Harry - does FC support unbounded fairness?
Bhasker -yes
Erich - we are discussiong eval criteria for examining proposals - can we
organize this discussion better?
Harry/Ed - general agreement that we need to look at language requirements
- revisit document that is on the web
D. Wrapup
Harry - proposing next meeting for 1st week of Dec - 5th of Dec (Tues) is
next meeting 9amPST.
Roll Call
Arif (for Swami)
Ed Clarke
Erich Marschner
Carl Pixley
Tom Anderson
Yaron IBM
Tom Fitzpatrick
Matthew Morley Verisity
Yaron Verisity
Mike McNamara self (not Yaron)
Bhasker
Cindy Eisner IBM
Shoham Ben David IBM
Danny Geist Danny_Geist@il.ibm.com
0-in intends to submit a proposal, subject to legal paperwork ...
next meeting will focus on requirements document
will try to get an outline worked out before next meeting, to be discussed
then
Harry will send out email to start this
This archive was generated by hypermail 2b28 : Wed Dec 06 2000 - 07:10:01 PST