Subject: Re: [sv-ac] written proposal: issue 15
From: John Havlicek (john.havlicek@motorola.com)
Date: Wed Feb 26 2003 - 06:02:36 PST
All:
I agree with all of Cindy's points.
Best regards,
John Havlicek
>
> 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 - 06:07:33 PST