RE: [sv-ac] Errata 269: Asynchronicity of disable iff in relation to the sampling clock

Hi Bassam,
 
A similar issue has been raised when we designed ForSpec a few years
ago. The decision that was made there was the following. We defined a
special keyword that evaluates to the active clock (in ForSpec it is
called "clock"). Then, making the reset synchronous with the clock is
achieved by intersecting it with the clock keyword. For instance, the
ForSpec equivalence of
disable iff ( b && clock ) @(c) P
makes b a synchronous reset signal for the property P.
 
Note also that this solution works also in a multi clock domain. That
is because in every clock domain, the clock keyword is evaluated to the
active clock in that domain. You may wish to consider a similar
solution for the SVA.
 
Regards,
 Roy
 

________________________________

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of
Bassam Tabbara
Sent: Tuesday, October 26, 2004 2:20 AM
To: sv-ac@eda.org
Subject: [sv-ac] Errata 269: Asynchronicity of disable iff in relation
to the sampling clock

Hi all,

** I had said I'd look into how to accommodate "async disable" in the
other places in LRM, but I now think that's not warranted, it is better
to fix disable itself and give us:
- async ability same as before, with clearer meaning (to solve this
errata item)
- sync ability, which was seemingly prevented before because of a single
word ....
- better alignment with PSL's abort [in my opinion]

The simplest (textual and may be even semantic ...) proposed change I
could think of to address this is to separate the "disable" from its
clocking. The idea is to "undo" thinking of disable as a special case
that does not abide by the "clocking" [described early in chapter 17
(Assertions) and also in chapter 14 (Scheduling Semantics)] but rather
seemingly operates outside those boundaries while there is no real need
for this distinction. As a side-effect of the reining in of disable,
with this change, we would have both sync and async capabilities, and
useful folding in of disable behavior.

In a nutshell, I propose that: @(c) disable iff ( b ) P != disable iff
( b ) @(c) P

In LHS, disable iff would be clocked by c, while in RHS disable iff
would be "asynchronous" i.e. operates according to some other
granularity clock that can catch all the b's i.e. a smart implementation
would use a "b value change" clock ...In effect this fixes any
aberration here with the scheduling semantics chapter since now disable
does operate based on a "clock" regardless of what that "clock" is ..

Rather

@(c) disable iff ( b ) P == @(c) disable iff ( b ) @(c) P

I do not think there are serious side-effects, everything else e.g.
clock flow should not be affected at all... but I did add a small fix in
the proposal as well. I have added a proposal to make the changes [that
I am aware of] apparent. Primarily deleting the confusing "asynchronous"
wording to say that disable is always "clocked" ...

** Finally as far as 195, this change rather emphasizes that disable iff
can have a different clock (It is permitted to have disable with one
clock, property_expr another) .... so may be it is best to use triggered
(instead of matched/ended), you see how now that disable folds under the
regular "clocking" we can apply the multi-clock rules and iron things
out ... (e.g. ended disallowed in general if mix of clocks).

May I suggest this be added a discussion item (this meeting or next)
depending on the agenda ? Arif please also assign this to me. I will
shortly post a link to this message and the attached proposal on the
ticket...

** Question: Does anyone know how we can mark something for *indexing* ?
(Example In this case one extra use of disable iff in the clock flow
section, and add the new term "pre-emptive" in the index).

Thx.
-Bassam.

--
Dr. Bassam Tabbara
Architect, R&D
Novas Software, Inc.
(408) 467-7893