Subject: [sv-ac] Re: new syntax
From: John Havlicek (john.havlicek@motorola.com)
Date: Tue Mar 25 2003 - 09:41:25 PST
Cindy:
Yes, you understood exactly what I was getting at. I think we
need to define a formal syntax for something like what used to
be the declarative assertions. That way, our definition of the
semantics has something to apply to.
I also agree that we need to try to define the mapping from embedded
procedural assertions to the formal syntax. We really don't have much
time to accomplish this, and it is probably better to say nothing than
to say something wrong. I can envision having to use phrases like
"perturb all declared identifiers to be unique and perturb all
references correspondingly so that the declaration-reference binding
relations are preserved".
Best regards,
John H.
>
> john,
>
> >The semantics we have written is built in levels and based on
> >recursive forms. I do not want to destroy this structure.
> >Perhaps we can write the semantics for "elaborated" assertions
> >without too much disruption.
>
> if i understand you correctly, then i agree with this. what i understood
> you to mean was this:
>
> define separately a set of rules for extracting a declarative assertion
> from an embedded (procedural) assertion. then give semantics to the
> declarative assertions. the fact that the syntax of the language does not
> have declarative assertions does not mean we cannot use them as a concept
> in the formal semantics.
>
> 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
>
>
> John Havlicek <john.havlicek@motorola.com> on 25/03/2003 07:33:33
>
> Please respond to john.havlicek@motorola.com
>
> To: Cindy Eisner/Haifa/IBM@IBMIL, roy.armoni@intel.com,
> fhaque@cisco.com, stephen.meier@synopsys.com,
> surrendra.dudani@synopsys.com, john.havlicek@motorola.com
> cc: sv-ac@eda.org
> Subject: new syntax
>
>
>
> Dear Semantics Group:
>
> Please have look at the new syntax. I can't say I'm entirely
> happy about what it implies for our work. My understanding
> leads me to the following observations.
>
> 1. Notice that there are no longer any declarative assertions.
> Assertions must be put in procedural or combinational
> always/initial blocks. This is at odds with our basic
> strategy of defining the semantics for declarative assertions
> and relying on a mapping from procedural assertions to
> declarative assertions.
>
> 2. The properties that are asserted must be declared separately
> from the assertion. Only a property instance can be asserted,
> not an explicit property. "always" and "initial" are no longer
> part of the property declaration. They will be inherited from
> the context. Notice that this means that
>
> always @(c) a ##1 b |=> x ##1 y
>
> is not legal SVA syntax. You can see the unfortunate consequence
> that our property-level semantics can be applied only to illegal
> syntax.
>
> 3. From 1. and 2., it follows that there is a clear syntactic
> distinction of top-level from inner clocks. A top-level
> clock is one that appears outside a property declaration.
> This seems good to me.
>
> 4. "not" can appear only below the property declaration level.
> Therefore, "not" cannot appear outside a top-level clock.
> This seems good to me.
>
> 5. Concatenation of differently-clocked explicit sequences is
> not allowed. To achieve concatenation of differently-clocked
> sequences, you must declare each with its clock and
> concatenate instances of them.
>
> The semantics we have written is built in levels and based on
> recursive forms. I do not want to destroy this structure.
> Perhaps we can write the semantics for "elaborated" assertions
> without too much disruption.
>
> Comments welcome.
>
> Best regards,
>
> John Havlicek
>
>
>
This archive was generated by hypermail 2b28 : Tue Mar 25 2003 - 09:42:06 PST