Subject: Re: [sv-ac] written proposal: issue 15
From: Surrendra Dudani (Surrendra.Dudani@synopsys.com)
Date: Wed Feb 26 2003 - 07:13:12 PST
Hi Cindy,
What happens when a property is defined declaratively, and used in a
procedural block such as,
property always p1 = @clk (a;b);
property initial p2 = @clk (a1;b1);
always @(clk) begin
d <= in1;
r1: assert p1;
r2: assert p2;
end
initial begin
in2 = 0;
r3: assert p1;
r4: assert p2;
end
Surrendra
At 02:29 PM 2/26/2003 +0200, you wrote:
>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
**********************************************
Surrendra A. Dudani
Synopsys, Inc.
377 Simarano Drive, Suite 300
Marlboro, MA 01752
Tel: 508-263-8072
Fax: 508-263-8123
email: Surrendra.Dudani@synopsys.com
**********************************************
This archive was generated by hypermail 2b28 : Wed Feb 26 2003 - 07:17:14 PST