Subject: Analysis of ForSpec with respect to Accellera requirements
From: Armoni, Roy (roy.armoni@intel.com)
Date: Sun Nov 18 2001 - 08:29:43 PST
R1a The language must define a temporal 'layer'.
met by ForSpec
R1e The language must define more than one language binding.
not met by ForSpec. ForSpec 1.0 has its own Boolean expressions.
ForSpec 2.0 will be binded to Verilog, which is the only required choice out
of R2a-R4c.
R2a The language must define how Verilog expressions may be used in its
statements.
not met by ForSpec 1.0. Will be met by ForSpec 2.0.
R7a The language must allow use of boolean types.
met by ForSpec
R7b The language must allow use of enumeration types.
met by ForSpec
R7c The language must allow use of array/vector types.
met by ForSpec - allows vector expressions.
R7d The language must allow use of structure/class types.
met by ForSpec - by means of vector/Boolean expressions defined
within blocks.
R7e The language must allow use of integer types.
met by ForSpec
R7f The language must allow use of integer types >32 bits.
met by ForSpec - bit vector width is limited by 2^31.
R8a The language must allow use of standard integer arithmetic operations
(+,-,*,/,mod,rem).
met by ForSpec, except for mod and rem.
R8b The language must allow use of standard logical operations
(=,/=,<,<=,>=).
met by ForSpec
R8c The language must allow use of standard vector operations (indexing,
slicing, concatenation).
met by ForSpec
R9a The language must allow reference to values of objects in the design at
a fixed number of cycles in the past.
met by ForSpec - the past operator
R10a The language must allow use of no-delay, no-side-effect functions in
expressions.
met by ForSpec - templates
SEQUENCES (temporal)
R13a The language must allow description of repeated finite sequences of
behavior.
met by ForSpec - for instance:
e*
e+
e & (e+ triggers next e)
R14a The language must allow description of finite sequences.
met by ForSpec - regular events
R14b The language must allow description of finite sequences with time
windows.
met by ForSpec - {n} and {n,m} are allowed in regular events. [n]
is allowed for next and wnext. [n,m] is allowed for until, wuntil, always
and eventually.
R16a The language must allow description/recognition of the first occurrence
of an event.
met by ForSpec - for an event f, use "true*,f" or "eventually f".
R16b The language must allow description/recognition of subsequent
occurrences of an event.
met by ForSpec - the next operator
R17a The language must allow description/recognition of all occurrences of
an event.
met by ForSpec - for an event e, use "true*, e TRIGGERS ..."
R18a The language must allow description/recognition of overlapping
occurrences of a given sequence.
met by ForSpec - for a sequence e, use "true*, e TRIGGERS ..."
R18b The language must allow description/recognition of overlapping
occurrences of two different sequences.
met by ForSpec - for two sequences e1 and e2, use "(true*,e1) |
(true*, e2)".
R19a The language must allow description/recognition of the 'or' of two
finite sequences.
met by ForSpec - the regular events are closed under the | operator.
R20a The language must allow description/recognition of the 'and' of two
finite sequences.
not met by ForSpec - In ForSpec 1.0, & between regular events
results in a formula. In ForSpec 2.0 we plan to add it with the following
semantics:
L(e1 && e2) =
{ (w1&&u1 … wm&&um wm+1 … wn) :
m*n, (w1 … wn)*L(e1), (u1 …
um)*L(e2) } *
{ (w1&&u1 … wn&&un un+1 … um) :
n*m, (w1 … wn)*L(e1), (u1 … um)*L(e2) }
R21a The language must allow a triggering event to be sequential, not just
boolean.
met by ForSpec
R22 The language must support a 'rich set of safety properties'.
(Subjective)
met by ForSpec
R23a The language must support liveness properties.
met by ForSpec
R25a The language must allow arbitrary composition of formulae and temporal
operators.
met by ForSpec - The class of Boolean expression is closed under all
Boolean/vector operators. The class of regular events is closed under
regular operators. The class of formulae is closed under formula operators.
R26a The language must be easy for designers to learn. (Subjective)
met by ForSpec - under use by RTL designers
R27a The language must be defined such that properties are closed under
negation.
met by ForSpec
R28a The language must support finite-time reasoning for static
verification.
met by ForSpec
R28b The language must support finite-time reasoning for simulation.
met by ForSpec
R31a The language must support the recognition of multiple, concurrent
(overlapping), data-dependent instances of the same behavior described
by a single property.
met by ForSpec - data dependency is achieved by deterministic
modeling.
R32d The language must support a vacuity check.
met by ForSpec - it is possible to check for a subformula f of a
formula g whether f affects g, even if f appears multiple times in g,
possibly with different polarity. See the discussion between Cindy and
myself on the difference between how ForSpec and Sugar handle vacuity.
CLOCKS
R34a The language must support description/use of level-sensitive clocks.
met by ForSpec
R34b The language must support description/use of after-rising-edge clocks.
met by ForSpec
R34c The language must support description/use of after-falling-edge clocks.
met by ForSpec
R34d The language must support description/use of after-any-edge clocks.
met by ForSpec
R35a The language must support description/use of weak clocks.
met by ForSpec
R35b The language must support description/use of strong clocks.
met by ForSpec
R36a The language must support description/use of multiple related clocks.
met by ForSpec
R36b The language must support description/use of multiple unrelated clocks.
met by ForSpec
R36c The language must support description/recognition of a single behavior
that involves multiple related clocks.
met by ForSpec
R36d The language must support description/recognition of a single behavior
that involves multiple unrelated clocks.
met by ForSpec
R37a The language must support definition of abstract clocks that 'tick'
when a given sequence occurs.
not met by ForSpec - ForSpec 1.0 uses Boolean expressions as clocks
while end of sequences may be used only to trigger or followed-by a formula.
ForSpec 2.0 defines the "ended(e)" operator that translates the end of a
sequence into a Boolean expression, which in turn may be used as a clock.
R37b The language must support use of abstract clocks anywhere any other
clocks can be used.
met by ForSpec
RESET
R39a The language must support selective inhibition of assertion checking
during reset and/or re-sync, in simulation.
met by ForSpec
R39b The language must support selective inhibition of assertion checking
during reset and/or re-sync, in formal verification.
met by ForSpec
META-LANGUAGE REQUIREMENTS
R45a The language must support the definition of named assertions
(/sub-rules/properties).
met by ForSpec
R45b The language must support composition of assertions to form more
complex assertions.
met by ForSpec
R46a The language must support user-defined parameterized macro definition
and expansion.
met by ForSpec
R47a The language must support definition of parameterized assertions.
met by ForSpec
R49a The language must support definition of a block representing a nested
scope.
met by ForSpec
R49b The language must support declaration of local variables within a
nested scope.
met by ForSpec
R49c The language must support instantiation of an assertion definition
within a nested scope.
met by ForSpec
R49d The language must support global variables.
met by ForSpec
R50a The language must support instance-specific application of properties.
met by ForSpec
R51a The language must support bounded iteration over a constant range known
at compile time.
met by ForSpec
R51b The language must support parameterization of signal names with
iteration indices.
met by ForSpec
R52a The language must support specification that a signal is constant
between successive events (e.g., clock edges).
met by ForSpec - "x=past(x,1,clk)"
R52b The language must support specification that a signal is constant for
some number of cycles.
met by ForSpec - "(x=past(x)){8}"
R53a The language must support a 'shorthand' notation for specifying
rising/falling signal transitions.
met by ForSpec
VALIDATION REQUIREMENTS
R55a The language semantics for formal verification must be well-defined.
met by ForSpec
R55b The language semantics for formal verification must be intuitive.
(Subjective)
met by ForSpec
R56a The language semantics for simulation must be well-defined.
met by ForSpec
R56b The language semantics for simulation must be intuitive. (Subjective)
met by ForSpec
R58a The language must be demonstrably formally verifiable via model
checking (i.e., some path must exist from the language into a formal model
checker).
met by ForSpec
R59a The language must be demonstrably simulatable (i.e., some path must
exist from the language into a simulator).
met by ForSpec
R64a The language must be compilable with reasonable complexity.
(Subjective)
met by ForSpec - PSPACE
R65a The language must support efficient negation/complementation of
properties. (Subjective)
met by ForSpec
R68a The language must support hierarchical verification, in which a given
property is first assumed (e.g., as an interface constraint) and then later
proven.
met by ForSpec
R44a The language must include constructs that support design/environment
modeling.
met by ForSpec - bit definitions
R70a The language must support the definition of properties (to be proven).
met by ForSpec
R70b The language must support the definition of constraints (assumptions).
met by ForSpec
R70c The language must support the definition of events (sequences).
met by ForSpec
R71a The language must support assumptions with proof obligation (e.g.,
interface constraints).
met by ForSpec - the assume directive
R71b The language must support assumptions with no proof obligation (e.g.,
for case splitting).
met by ForSpec - the restrict directive
R71c The language must support formulae (to be assumed) that can specify any
omega-regular language.
met by ForSpec
R71d The language must support formulae (to be checked) that can specify any
omega-regular language.
met by ForSpec
R71e The language must support asserting every assumption.
met by ForSpec
R71f The language must support assuming every assertion.
met by ForSpec
R71g The meaning of a given formula must be the same, regardless of whether
it is assumed or asserted.
met by ForSpec
R72a The language must introduce a minimal number of concepts. (Subjective)
met by ForSpec
R73a The language must be small and simple to use. (Subjective)
met by ForSpec
R74a The language must be easy to learn, write, and read. (Subjective)
met by ForSpec
This archive was generated by hypermail 2b28 : Sun Nov 18 2001 - 08:30:51 PST