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

From: Surrendra Dudani <Surrendra.Dudani@synopsys.com>
Date: Wed Oct 27 2004 - 10:45:12 PDT

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 
********************************************** Received on Wed Oct 27 10:45:00 2004