Subject: [sv-ac] assertions embedded in procedural code
From: Cindy Eisner (EISNER@il.ibm.com)
Date: Sun Feb 16 2003 - 01:29:55 PST
all,
prakash's notes on check got me started on thinking about what it means for
an assertion to be embedded in sequential and combinational always blocks.
i seem to remember that some previous document (perhaps it was the 3.0
version of assertions?) talked about what happens when an assertion is
triggered by a glitch in a combinational always block. but revision 0.79
doesn't seem to discuss this anywhere.
or does revision 0.79 disallow assertions in combinatorial always blocks?
it doesn't really say, but reading the grammar it appears that this is the
intention. (appendix b says "concurrent_assertion_item can be a
module_item or a statement_item". i think it means to say that both
module_item and statement_item get an additional grammar production rule so
that each goes to concurrent_assertion_item.)
if assertions in combinatorial always blocks are allowed, there should be
some informal discussion of what that means, in addition to any formal
definition we make in the semantics sub-committee.
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 : Sun Feb 16 2003 - 01:27:44 PST