Subject: [sv-ac] new syntax
From: John Havlicek (john.havlicek@motorola.com)
Date: Mon Mar 24 2003 - 21:33:33 PST
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 - 21:34:21 PST