Subject: Re: [sv-ac] Sequential implication proposal
From: John Havlicek (john.havlicek@motorola.com)
Date: Fri Feb 07 2003 - 06:18:21 PST
Erich and All:
I am happy to withdraw my proposal for fixing the semantic
problem with sequential implication.
However, I do not understand the rationale in Surrendra's
proposal, modified below by Erich, for having property declarations
and not property expression declarations.
By not allowing declaration of property expressions,
this proposal does not allow me to use a property expression
instance in building properties. Rather, it forces me to
use only instances of property specs. If an explicitly unqualified
property spec is understood to have "always" as qualifier,
then the instantiated property spec is always qualified.
Thus, the syntax below seems to lead effectively to things like
always(initial((a;b)=>(never(c;d))))
through a series of property declarations like
property p1 = never (c;d);
property p2 = initial ((a;b)=>p1);
property p3 = always p2;
I don't think it was intended for this layer of the
language to work in this way. Wasn't the intention
for "always", "initial", "never" to be applied at
the outermost of a full property expression, not to
proper subexpressions?
Best regards,
John Havlicek
> Surrendra,
>
> Following is a slight revision of your proposed syntax, intended to address several issues we covered in the meeting today:
>
> 1. the discussion about merging 'initial' and 'never' (and the implicit 'always')
> 2. the need to allow the RHS of an implication be an instance of a named property
>
> I've also taken the liberty of spelling out 'property' in the nonterminals, inserted some blank space here and there for readability, and added the necessary quote marks around the semicolon.
>
> Revised Syntax:
> ============
>
> property_declaration ::=
> 'property' named_property { ',' named_property } ';'
>
> named_property ::=
> identifier [ '(' identifier { ',' identifier } ')' ] '=' property_spec
>
> property_spec ::=
> [ 'accept' '(' expression ')' ] [ qualifier ] clocked_expr
>
> qualifier ::= 'initial' | 'never' | 'always' // 'always' is still the default if no qualifier present - but also allowed explicitly
>
> clocked_expr ::=
> [ event_control ] '(' property_expr ')'
>
> property_expr ::=
> sequence_expr
> | implication
> | '(' property_expr ')'
> | identifier [ '(' expression_list ')' ] // identifier must be a property
>
> implication ::=
> sequence_expr => property_expr
>
> ============
>
> Substantive Changes:
>
> 1. moved 'initial' to be an alternative to 'never', before property_spec.
> 2. added 'always' as an explicit alternative to both, before property_spec.
> 3. moved property instantiation to be a variant of property_expr.
>
> Effect of Changes:
>
> 1. avoids situation where "initial" and "never" co-occur - these seem contradictory.
> - 'never' seems to mean 'always not', and 'always' and 'initial' are clearly contradictory
>
> 2. allows "always" to be stated explicitly - reinforces the idea of initial/never/always being alternatives
> - included for symmetry and clarity; I'll withdraw the suggestion if anyone objects
>
> 3. allows an implication to have an instance of a named sequence as its RHS - e.g.,
>
> property StartUp =
> initial (!reset[*] ; reset) => OK ;
>
> property OK =
> never (errorstate) => (1 ; errorstate) ; // stuck in errorstate
>
> Note that this would allow nested implication as well, but it requires a name for each level of nesting, so there is never more than one implication operator in any one property.
>
> Regards,
>
> Erich
>
> -------------------------------------------
> Erich Marschner, Cadence Design Systems
> Senior Architect, Advanced Verification
> Phone: +1 410 750 6995 Email: erichm@cadence.com
> Vmail: +1 410 872 4369 Email: erichm@comcast.net
This archive was generated by hypermail 2b28 : Fri Feb 07 2003 - 06:20:59 PST