Subject: RE: ccellera FV: Motion 2 -- Requirements adoption and prioritiza tion
From: Armoni, Roy (roy.armoni@intel.com)
Date: Sat Aug 04 2001 - 23:18:11 PDT
I vote YES for motion 2.
-----Original Message-----
From: Harry Foster [mailto:foster@rsn.hp.com]
Sent: Friday, August 03, 2001 2:35 AM
To: vfv@eda.org
Subject: ccellera FV: Motion 2 -- Requirements adoption and prioritization
Accellera Formal Verification Technical Committee - "Significant Issue"
Ballot
The following motion is being put forward for ballot by the current voting
members of the Accellera Formal Verification Technical Committe. These
motion was deemed "significant issues" in the August 2, 2001 meeting. The
ByLaws adopted in the September 2000 meeting of the Committee state that any
vote on a "significant issue" must be held by email, and 80% of the voting
membership must cast a 'yes' ballot for these motions to be accepted. This
vote is being held in accordance with that requirement.
For the record, both motions should be considered made by Erich Marschner,
seconded by Harry Foster.
According to the ByLaws, a Voting Member of the Committee is anyone who has
attended 3 of the last 4 Committee meetings, whether in person or by
telephone. The roll of Voting Members who are entitled to vote in this
ballot appears below.
Votes should be emailed to <vfv@eda.org> and must be received no later than
12:00 midnight PST on August 8th.
==========================
Please note that I've attached a new Excel file for the requirements. If
you need a copy of the Properties example document please send me e-mail.
==========================
Motion 2:
To adopt the requirements and prioritization of those requirements
(Essential, Nice-To-Have) that were reviewed in the Committee meeting in
Paris on July 17, 2001, except for any requirement specifically identified
in a ballot response as an issue that needs further discussion. Any
requirement identified as an issue will be moved to the Undecided category
and reviewed again in the next meeting. For reference, the requirements and
their prioritization at the end of the discussion in the July meeting, as
described in the minutes of the July meeting, are as follows:
>>>>
Essential
=======
1-8 Support rich data types and expressions with at least the expressive
power of VHDL and Verilog
13 [support for] Repeated sequences
14 Finite sequences with time windows with anchoring success to end of
sequence
16 [support for matching] only first occurrence of event
17 [support for matching] all occurrences of the event
18 [support for matching] overlapping sequences
19 [support for matching] 'or' combinations of sequences [to model multiple
outcomes of transactions]
20 [support for matching] 'and' combinations of sequences
21 [support for] Sequential composition of finite sequences followed by
formulae
22 [support for] Rich Safety properties
23 [support for] Minimal Liveness properties (e.g., eventually p)
26 Language must be easy to learn by designer
28 Enable finite time reasoning (static and dynamic) - partial path
computations (identify failure in simulation as soon as possible)
33 Allow Asynchronous modeling/properties
36 Support multiple clocks
38 Support discrete event and synchronous models (has semantics that can
handle event based simulator
44 [support both] property [specification] & modeling
49 [support for] blocks/instantiation/ name's scoping (a variable for each
instance and sometimes global variables)
50 [support for] for different instantiation of RTL blocks you may get
different instantiations of the corresponding properties
55 Well defined semantics and intuitive semantics
56 Well defined semantics for simulation
58 Vendor support in Formal Model checker
59 Vendor support in simulation
62 [avail]ability of [published] "Efficient" model checking algorithms
63 Full support of the assume/guarantee paradigm
64 Reasonable complexity of compilation
66 Compositionality Semantics of the formula is defined from the semantics
of its sub-formulas
68 Support hierarchical verification (for properties pertaining to
interfaces - ability to interchange constraints and properties)
70 Enable the definition of properties, constraints (assumptions) and events
(sequence)
73 Small and simple to use
74 Easy to use: learn, write, read
75 [the language should be] succinct [like this requirement]
Nice-to-have
==========
9 Expressions may include [explicit] reference to 'prior' times, i.e., refer
to PAST
10 Use of 'zero-time' "computational" functions in expressions
24 [support for] Rich Liveness properties (e.g., possibly: strong fairness
GFp -> GFp)
25 Allow arbitrary composition of formulae/temporal operator for simplicity
and elegance
27 Close assertions under negation (for efficient model-checking - allow
negation of a formula instead of complementing an automaton)
29 Explicit and short-hand notation for Finite State Machines (fsm) - need
to be supported for assume-guarantee (Roy)
31 Datapath properties specify the transformation of data over a period of
many cycles (e.g., parallel to serial conversion)
34 level sensitive clocks and rich set of edge-sensitive clocks
35 weak and strong clocks (weak clocks may not tick, strong clocks must
tick)
37 Support abstract clocks (even the occurrence of a sequence of events may
define the occurrence of the tick)
39 Inhibit of some or all rules during reset and/or re-sync ([reset] can
cause false assertion failures during simulation - Roy)
40 Suspend properties (via reset)
41 Check other property when reset
42 Reject or Accept on reset (you usually want to "accept" the property when
reset occurs, however when you have reset nested within negation you also
need reject)
45 Named sub-rules important for accuracy and clarity and for building
complex properties using other properties as building blocks
46 templates with parameters to allow user defined constructs
47 Ability to build library of properties parameterized lib.
48 recursive definition of templates
51 for-loops, parameterized signal names (succinct creation of similar
formulas)
52 shorthand for specifying signals are constant (most buses require signals
to be stable throughout a sequence)
53 shorthand for 'rose' and 'fell' (or posedge/negedge if you prefer)
54 Allow composition (non monolithic properties)
57 Allow Calls to procedural code during simulation (for support of datapath
checks in simulation - see exec in 'e')
61 Not specifically tied to a particular class of reasoning
65 efficient negation/complementation of properties (NOT mean
complementation of REs)
71 Support for checkers, assumptions with proof obligation, assumptions for
case splitting (no proof obligation), modeling with formulae
72 Introduce a minimal number of concepts
Undecided
========
32 Include existential path quantifier - AG EF (state=idle) AG(fram-fall ->
E[irdy U !trdy] - [or maybe CTL bypass option?] - split (7/7/6)
<<<<
A vote 'yes' with no exceptions for Motion 2 is a vote to reaffirm all
prioritizations determined at the Paris meeting. A vote 'yes' with
exceptions for Motion 2 is a vote to reaffirm prioritization for all but
those excepted requirements, which will then be moved to the Undecided
category. A vote 'no' for Motion 1 is a vote to revoke all prioritization
decisions taken at the Paris meeting.
Voting Members: (NOTE: If you feel this list is in error please gently send
me email....).
============
(aaa.........) Bassam Tabbara (Novas)
(aaaaaa......) Bernard Deadman (SDV) *
(aaaaaa-aaaaa) Ed Clarke (CMU) *
(aaaaaa-aaaaa) Erich Marschner (Cadence) *
(aaaaaaaaaaaa) Harry Foster (HP) *
(rraaaa----rr) K.C.Chen/BowYaw Wang (Verplex) *
(aaaaaa......) Moshe Vardi (Rice) *
(aaraa-aaa...) Michael Siegel - (Siemens) *
(aaraaaaa---a) Peter Flake (Co-Design) *
(a-aa........) Sandeep Shukla (UC Irvine)
(r-raaaaraaaa) Tom Anderson (0-in) *
(raaaararaaa-) Cindy Eisner (IBM) *
(a-aaaaaaaaaa) Danny Geist (IBM) *
(araaaaaraaa-) Shoham Ben David (IBM) *
(aaaaaaaaaaa-) Yaron Wolfstal (IBM) *
(aaraaaa.....) Limor Fix (Intel) *
(aaaaaa......) Avner Landver (Intel) *
(aaaaaa......) Roy Armoni (Intel) *
(aaaaaaaaaaaa) Hillel Miller (Motorola) *
(a-aaa--aaaa-) Mike McNamara (Verisity) *
(aaaaaaaaaaa-) Matthew Morley (Verisity) *
(a-aaaaaaaaar) Yaron Kashai (Verisity) *
(aaaa........) David Van Campenhout (Verisity) *
(aaa.........) Dana Fisman (IBM) *
Non-Voting Members:
================
(--aa........) Andreas Tiemeyer (Intel)
(--aaaa-aaaaa) Carl Pixley (Motorola)
(--a.........) John Havlicek (Motorola)
(aa..........) Atanas Parashkeven - Motorola
(-a---a---a-a) Vassilios Gerousis (Infineon)
(-a..........) Simon Davidman - (Co-Design)
(--a-aaaaa...) Prakash Narain - (RealIntent)
(--aa........) Axel Scherer (Cadence)
(a...........) E. Allen Emerson (UT)
(a...........) Karen Yorav (Galileo)
(a.a.a.......) Stephen Meier (Synopsys)
NOTE: The committee inactive members (i.e., haven't attended any of the last
four meetings yet are still on the mailing list) are not listed above.
This archive was generated by hypermail 2b28 : Sat Aug 04 2001 - 23:21:38 PDT