Subject: Re: [sv-ac] specific proposal
From: John Havlicek (john.havlicek@motorola.com)
Date: Wed Feb 05 2003 - 13:24:11 PST
Hi Adam:
The original LRM definition allows nesting of sequence implications and
the use of the local variables in nested sequence implications, so my proposal
preserves them. Moving sequence implication to the clocked_sequence level
does not preserve these capabilities.
In practice, I think both nesting and allowing the local variables at various
points can be useful because the behavior that is being described may have
several different timepoints at which data need to be sampled.
One could argue that my proposal is too limited because other operators,
like "and" and "or", make perfect sense at the formula layer, but they are no
longer allowed on sequence implications.
My opinion is that if we have a formula layer, then we should be able to
declare named formulas. Personally I envision expansion of the formula layer
to admit more operators, at which point the ability to declare named formulas
should look less redundant.
I thought about trying to make "prop_expr" do the job of "formula_expr", but
I did not know what to do with the "initial", "accept", and "never" parts.
I think Surrendra's proposal follows this approach, but it changes the
old "prop_expr" to "prop_spec".
Best regards,
John H.
> Hi John;
>
> Questions, questions - no answers.
>
> This proposal creates another element, a formula, similar to sequences and boolean
> (declarations.)
>
> So we can declare
>
> formula a = (something);
> sequence b = (soemthing);
> bool c = (something);
>
> Is there value in the ability to declare all three?
> Would it be sufficient to just factor sequence implication up to the clocked_sequence
> level as in:
>
> clocked_sequence :== [event_control] sequence_expr
> | [event control] sequence_expr => sequence_expr
>
>
>
> For formulas, you allow:
>
> sequence => sequence
>
> Which we talked about. You also allow:
>
> sequence => sequence => sequence
> ((int somevar = something) formula)
>
>
> Is it valuable to have these two additional abilities (from one who has not worked
> with formulas)?
>
> Thanks.
>
> Adam Krolnik
> Verification Mgr.
> LSI Logic Corp.
> Plano TX. 75074
>
>
>
This archive was generated by hypermail 2b28 : Wed Feb 05 2003 - 13:25:43 PST