Subject: [sv-ac] Re: new syntax
From: Cindy Eisner (EISNER@il.ibm.com)
Date: Mon Mar 24 2003 - 22:57:13 PST
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 : Mon Mar 24 2003 - 22:54:26 PST