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

Hi Roy,

Thx for the write-up. I think it's important for me to re-emphasize the
"motivation" of the ticket (even at the risk of repeating myself, excuse
that please). The ticket came out of the discussion of 195. We have agreed
that, as is, disable iff seems to have an air of inconsistency about it with
the rest of the assertion sampling and at least deserves a special
mention/accommodation in the scheduling semantics.
 
My bottom line suggestion here is that it is may be better to address the
disable iff itself rather than add this special case into the scheduling
description. The crux of the idea is to decouple the construct description
from the condition sampling, everything else does NOT mix the sampling with
the function ... This decoupling a) adds simplicity, b) makes the language
of the clocking in chapter 17, and the scheduling semantics of 14 applicable
to disable iff (it would fall into the same category as other
"un-explicitly-clocked" properties ... ), and c) accommodate a wider
interpretation of clocking by virtue of the decoupling of the construct and
the sampling of its condition.
 
Now (c) might seem extraneous (one could argue that... in fact we can split
the proposal into 2 parts even: cleanup + added interpretation ...), but I
feel that the wider interpretation makes disable iff fit even better in the
context of (b) above when it comes to default clocks, again removing any
oddities/specialties with this construct. This wider interpretation claims
that we already have the facilities to have 2 versions of disable (again,
sampling should not be a part of the construct description), we really need
not add any new keywords, just "assimilate" disable iff better into the rest
of assertions.

Thx.
-Bassam.

--
Dr. Bassam Tabbara
Architect, R&D
Novas Software, Inc.
(408) 467-7893
 
  _____  
From: Armoni, Roy [mailto:roy.armoni@intel.com] 
Sent: Tuesday, October 26, 2004 6:04 AM
To: bassam@novas.com; sv-ac@eda.org
Subject: 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