Subject: Re: [sv-ac] assertions embedded in procedural code
From: Stephen Meier (Stephen.Meier@synopsys.com)
Date: Sun Feb 16 2003 - 15:04:31 PST
Cindy:
All concurrent assertions are sampled assertions.
Yes both module_item and statement_item will get an additional production
rule so that each goes to concurrent_assertion_item.
When concurrent assertions appear in module then any procedural context
is extracted and used as sampling condition and/or the antecedent of a
boolean implication. The LRM is light on this explanation, we will discuss
more details at next SV-AC meeting.
If there is a glitch in combinational always block and the triggering
signals are not enabled at the sampling clock, then the entire glitch is
ignored.
Steve
---------
At 11:29 AM 2/16/2003 +0200, Cindy Eisner wrote:
>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
Steve Meier (stephen.meier@synopsys.com) W: 650-584-4476, Cell: 408-393-8246
This archive was generated by hypermail 2b28 : Sun Feb 16 2003 - 15:05:29 PST