Subject: assertion requirements
From: Cindy Eisner (EISNER@il.ibm.com)
Date: Wed Jul 17 2002 - 09:06:36 PDT
colleagues,
below please find my initial list of proposed requirements.
===========================================================================
1. sv-assertions should have formally defined semantics
justification:
if we cannot define precisely what an assertion means, we cannot say
whether or not a
particular implementation is correct. in the same manner, the use of
assertions for
documentation purposes is compromised when the exact meaning of an
assertion is
not known.
downside:
this may be difficult because the semantics of the procedural code in
which assertions
are embedded are themselves not formally defined.
===========================================================================
2. sv-assertions should have semantics which are independent of a
particular
implementation
justification:
semantics should be defined in terms of what the assertion means,
leaving it up to the
tool to decide on a particular implementation.
===========================================================================
3. sv-assertions should have identical semantics in all types of
verification.
justification:
assertions are an aid to verification, not only an aid to simulation,
and should have
identical semantics whether verification is done by code inspection,
simulation,
emulation, formal analysis, or some other means.
===========================================================================
4. sv-assertions should have no side effects
justification:
we must ensure that the design itself complies with the assertions. if
an assertion has
side effects, then there is no way to know whether or not this is so.
===========================================================================
5. sv-assertions should be compatible with sugar
justification:
in the last meeting, simon (i believe it was) asked why this should be
so, given that
sv-verilog is a modeling language and sugar is a verification language
(actually, sugar
is technically a specification language, but that is beside the current
point). my answer
is that while sv-verilog is indeed primarily a modeling language,
assertions are there to
deal with verification issues, therefore, the aspect of sv-verilog that
this committee is
dealing with is verification, and it makes sense for sv-assertions and
sugar to be
mutually compatible. to put it another way: sugar provides a way to
make standalone
assertions about a design, while this sub-committee is dealing with
defining embedded
assertions. it would be extremely unfortunate if accellera were to
come out with
incompatible standards for these two extremely similar and intertwining
goals.
a note on what it means to be compatible:
there is syntactic compatibility and semantic compatibility. having
syntactic
compatibility without semantic compatibility is a recipe for confusion
and ultimately user
frustration.. therefore, by compatible we should mean "both
syntactically as well as
semantically".
regards,
cindy.
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
This archive was generated by hypermail 2b28 : Wed Jul 17 2002 - 09:07:21 PDT