Subject: Summary of FVTC Requirements for Property/Assertion Languages
From: Erich Marschner (erichm@cadence.com)
Date: Fri Jul 26 2002 - 17:25:05 PDT
The following (drafted by Cindy Eisner, further edited by Erich
Marschner) is a summary of the requirements developed by the
FVTC in the process of reviewing donated assertion languages.
============================================================
colleagues,
at the last meeting erich marschner and i agreed to summarize the
requirements of the accellera fvtc for you. please find that summary
below. the entire document can be found in the archive of the fvtc
committee at:
http://www.eda-twiki.org/vfv/hm/att-0440/01-VFV_requirements.zip
the summary below is divided into seven sections, which match the
respective sections in the original document. (EM: Each requirement
in the original document has a unique designation such as R1a, R2b,
etc. The summary below is cross-referenced to the original document
via those designations. Note that the original document includes
all requirements that were proposed during the requirements
development process. The proposed requirements were individually
balloted, and those that were supported by more than 50% of the
FVTC membership were approved. This summary only mentions the
approved requirements.)
regards,
cindy
============================================================
requirements about expressiveness
the language must support :
a temporal layer (R1a)
more than one language binding (including verilog) (R1e, R2a)
various types/operations (boolean, enum, array/vector, etc.) (R7a-f, R8a-c)
reference to values a fixed number of cycles in the past (R9a)
no-delay, no-side-effect functions (R10a)
============================================================
requirements about temporal sequences
the language must allow :
- description of finite sequences including time windows and repeated
sequences (R13a, R14a-b)
- reference to the first, subsequent, and all occurences of an
event (R16a-b, R17a)
- overlapping occurences of the same sequence as well as of two difference
sequences (R18a-b)
- "or" and "and" between sequences (R19a, R20a)
- sequences as triggering events (R21a)
...also in this section, although not related to sequences, there appears:
the language must support:
- a rich set of safety properties as well as liveness properties (R22, R23a)
- arbitrary composition of formulae and temporal operators(R25a)
- easy to learn (R26a)
- closed under negation (R27a)
- finite time reasoning for both static verification and simulation (R28a-b)
- recognition of multiple, concurrent (overlapping) data-dependent
instances of the same behavior described by a single property (R31a)
- vacuity check (R32d)
============================================================
requirements about clocks
the language must support:
- various kinds of clocks, and clocked behavior, including
level-sensitive, edge-triggered, weak and strong,
multiple related, multiple unrelated, and abstract clocks
(R34a-d, R35a-b, R36a-d, R37a-b)
============================================================
requirements about reset
the language must support:
- selective inhibition of assertion checking during reset and/or re-sync,
in both simulation and formal verification (R39a-b)
============================================================
meta-language requirements
the language must support:
- the definitions of named assertions (R45a)
- composition of assertions to form more complex assertions (R45b)
- user-defined parameterized macro defintion and expansion (R46a)
- parameterized assertions (R47a)
- nested variables within a nested scope (R49a-b)
- instantiation of assertions within a nested scope (R49c)
- global variables (R49d)
- instance-specific application of properties (R50a)
- bounded iteration over compile-time constant (R51a)
- parameterization of signal names with iteration indices (R51b)
- specification that a signal is constant between success events or for
some number of cycles (R52a-b)
- shorthand for specifying rising/falling signal transitions (R53a)
============================================================
validation requirements
the following must hold:
- semantics for formal verification and for simulation must
be well-defined and intuitive (R55a-b, R56a-b)
- language must be both demonstrably verifiable via model checking
and demonstrably simulatable, with reasonable complexity, efficient
negation, and support for hierarchical verification (R58a, R59a,
R64a, R65a, R68a)
============================================================
other requirements
the language must (have/be):
- supply constructs for design/environment modeling, definition of
properties to be proven, constraints to be assumed with and
without proof obligation, sequences (R44a, R70a-c, R71a-b)
- support formula that can express any omega-regular language for both
assertions and assumptions(R71c-d)
- ability to assert every assumption and assume every assertion (R71e-f)
- consistent semantics over assumptions and assertions (R71g)
- small and simple language, easy to learn, write, and read (R72a, R73a,
R74a)
============================================================
Cindy Eisner
Formal Methods Group Tel: +972-4-8296-266
IBM Haifa Research Laboratory Fax: +972-4-8296-114
Haifa 31905, Israel e-mail: eisner@il.ibm.com
-------------------------------------------
Erich Marschner, Cadence Design Systems
Senior Architect, Advanced Verification
Phone: +1 410 750 6995 Email: erichm@cadence.com
Vmail: +1 410 872 4369 Email: erichm@comcast.net
This archive was generated by hypermail 2b28 : Fri Jul 26 2002 - 17:27:16 PDT