Subject: RE: [sv-ac] Sequential implication proposal
From: Erich Marschner (erichm@cadence.com)
Date: Fri Feb 07 2003 - 07:05:29 PST
John,
I think this is what I was suggesting yesterday - that initial/always/never should be applied at the directive level, not at the property level. I did not try to change this in the refinements I made to Surrendra's syntax; I just wanted to reflect the items we discussed yesterday that seemed to have been acceptable. (I also should have changed the implication RHS to sequence_expr, but forgot to do that.)
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
| -----Original Message-----
| From: John Havlicek [mailto:john.havlicek@motorola.com]
| Sent: Friday, February 07, 2003 9:18 AM
| To: Erich Marschner; sv-ac@eda.org
| Subject: Re: [sv-ac] Sequential implication proposal
|
|
| 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 - 07:06:54 PST