Subject: [sv-ac] Re: new syntax
From: Surrendra Dudani (Surrendra.Dudani@synopsys.com)
Date: Tue Mar 25 2003 - 12:08:46 PST
I agree. We should use the declarative form for defining semantics. The
rules of inference for procedurally embedded assertions are expected to
provide syntactic transformations to declarative form.
Surrendra
At 11:41 AM 3/25/2003 -0600, John Havlicek wrote:
>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
> >
> >
> >
**********************************************
Surrendra A. Dudani
Synopsys, Inc.
377 Simarano Drive, Suite 300
Marlboro, MA 01752
Tel: 508-263-8072
Fax: 508-263-8123
email: Surrendra.Dudani@synopsys.com
**********************************************
This archive was generated by hypermail 2b28 : Tue Mar 25 2003 - 12:09:36 PST