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

Surrendra,

Indeed, also Adam discussed how synchronicity can be obtained from status
quo. That's not surprising, you can always get a larger sample granularity
from a finer one ... Exactly why I see the proposed re-working in 269 as a
cleanup to dispel this rather misleading notion of "asynchronicity" and its
needless special handling.

As far as nesting of disable iff, 269 does not suggest or address that (nor
am I so sure it is needed anyway ...); I also agree with what you say below.

** Please do point out what exactly in 269 raised these flags in your mind,
or may be you were just adding some related comments ?

Thx.
-Bassam.

--
Dr. Bassam Tabbara
Architect, R&D
Novas Software, Inc.
(408) 467-7893
 
  _____  
From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of
Surrendra Dudani
Sent: Wednesday, October 27, 2004 10:45 AM
To: sv-ac@eda.org
Subject: Re: [sv-ac] Errata 269: Asynchronicity of disable iff in relation
to the sampling clock
I believe synchronous resets can already be expressed in 3.1a by using
$sampled in disable iff expressions for specifying synchronous
signals/expressions. For example,
assert @clk disable iff ($sampled(exp)) prop1;
Where exp is the reset expression and prop1 is a property.
I think allowing multiple disable iffs within a single property is an
enhancement that should be considered more thoroughly and should have formal
semantics worked out before adding to the language. Perhaps, we can discuss
this improvement after all errata have been completed.
Surrendra
At 05:20 PM 10/25/2004 -0700, you wrote:
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
 
**********************************************
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  
**********************************************