Subject: [sv-ac] written proposal: issue 15
From: Cindy Eisner (EISNER@il.ibm.com)
Date: Wed Feb 26 2003 - 04:29:10 PST
all,
as per yesterday's meeting, here is my written proposal for issue 15:
----------------------------------------------------------------------------------------------------------------
proposal:
when a property is at the declarative level (not embedded in procedural
code), require one of either "initial" or "always"
when a property is embedded in procedural code, prohibit the use of both
"initial" and "always"
the bnf for a property would then read something like this:
prop_spec ::=
['initial' | 'always'] ['accept' '(' expression ')' ] ['not']
clocked_expr
| identifier ['(' expression_list ')']
while the above proposed restrictions would be semantic restrictions.
----------------------------------------------------------------------------------------------------------------
i have two concerns that prompt me to make this proposal:
1. readability
as steven mentioned in the minutes, i think that
always @(posedge clk)
(0)
if (abc)
assert always (x;y;z);
might be read as
assert @(posedge clk) always (abc => always (x;y;z));
(1)
whereas the extraction rules presented by steve give
assert @(posedge clk) always (abc => (x;y;z));
(2)
although (1) is not a legal assertion in sva, it does have an intuitive
meaning to users of other formal languages (like psl). coding as follows:
always @(posedge clk)
(3)
if (abc)
assert (x;y;z);
eliminates this problem. just as the single @(posedge clk) in (2) is
intuitively derived from the single @(posedge clk) in (3), the single
"always" in (2) can be understood as coming from the single "always" in
(3).
2. future expansion of sv assertions
if the sv assertions are to be expanded in the future in such a way as to
support more flexible kinds of properties (i.e., nesting of clocks,
negations, accept, always, etc.), then both (1) and (2) might be allowed in
the language. in this case, the extraction rules would need to be more
flexible as well, and would probably interpret (0) as (1). thus, in order
to get (2), we would have to allow (3).
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 Feb 26 2003 - 04:44:31 PST