RE: [sv-ac] Inline properties proposal

Subject: RE: [sv-ac] Inline properties proposal
From: Cindy Eisner (EISNER@il.ibm.com)
Date: Sun Mar 30 2003 - 06:24:04 PST

all,

i agree with bassam and support adam's proposal 2.

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

"Bassam Tabbara" <bassam@novas.com>@eda.org on 28/03/2003 03:14:29

Please respond to <bassam@novas.com>

Sent by: owner-sv-ac@eda.org

To: "'Adam Krolnik'" <krolnik@lsil.com>, <sv-ac@eda.org>
cc:
Subject: RE: [sv-ac] Inline properties proposal

Adam, I'd go with proposing (2) for a vote to all AC i.e. a "simple"
projection of the capabilities. It's not just an issue with local vars,
the other restrictions would be this is not named, so you can't do
ended/matched .... i.e. if you need a complex property you go to full
blown declaration ...

Fair enough ?

-Bassam. 

--
Dr. Bassam Tabbara
Technical Manager, R&D
Novas Software, Inc.

http://www.novas.com
(408) 467-7893

> -----Original Message-----
> From: owner-sv-ac@server.eda.org
> [mailto:owner-sv-ac@server.eda.org] On Behalf Of Adam Krolnik
> Sent: Thursday, March 27, 2003 3:22 PM
> To: sv-ac@server.eda.org
> Subject: [sv-ac] Inline properties proposal
>
>
>
>
>
> Hi all;
>
> With an inline property there are no needs for parameters
> being passed. Removing this, I add the remainder of the
> property definition after the keywords "assert property" or
> "cover property".
>
> This is a minimal change - I have not added anything or
> removed anything else. For simplicity, i submit these as the
> two proposal from which to pick.
>
> In the interest of time, would those that agreed with this
> issue give their opinions on these proposals.
>
>    Thanks.
>
>    Adam Krolnik
>    Verification Mgr.
>    LSI Logic Corp.
>    Plano TX. 75074
>
>
> -----------------------------------------------------------
> Proposal 1 (w/ dynamic variables)
>     Declare variables within parenthesized list attached to
> property keyword.
>     These variables are valid until the end.
>
> Add this production to concurrent_assert_statement.
>
>     | assert property [ '(' variable_declaration {,
> variable_declaration} ')' ]
>         [disable iff expression] [not] '(' propert_expression ')'
>         action_block
>
> Add this production to concurrent cover statement.
>
>     | cover property [ '(' variable_declaration {,
> variable_declaration} ')' ]
>         [disable iff expression] [not] '(' property_expression ')'
>         action_block
>
> Examples.
>
> assert property (int x)
>       (a ##1 b, x = c |=> [2:10] c ##0 d == x)
>     else $error(" Missing c or d not correct value.");
>
> assert property (int x, reg [3:0] z)
>       disable iff (abort & flush)
>       not (a ##1 b, x = e ##2 c, y = tag ##[2:5] d ##0 x+y != g)
>     else $error("Result invalid %0h vs %0h.", g, x+y);
>
> cover property (a ## [1:3] b& !c ##[2:5] d);
>
>
>
> --------------------------------------------------------------
> ---------------
>
> Proposal 2 (w/o dynamic variables)
>     Take inside of property declaration, minus dynamic
> variables and sequences.
>
>
> Add this production to concurrent_assert_statement.
>
>    |  assert property [disable iff expression] [not]
> (property_expression)
>         action_block
>
>
> Add this production to concurrent_cover_statement.
>
>    |  cover property [disable iff expression] [not]
> (property_expression)
>         action_block
>
> E.g.
>
>     assert property (a == 2 => b ##1 !c ## [2:5] d)
>        else $error("Bad sequence.");
>
>     assert property
>        disable iff (flush && abort)
>        not @(posedge nclk) (a ##1 !b ##[2:5] c)
>        else $error("Found illegal c afterward.");
>
> --------------------------------------------------------------
> ------------
>
>
>

This archive was generated by hypermail 2b28 : Sun Mar 30 2003 - 06:20:50 PST