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

Hi Adam,

No, my suggestion is "whatever applies to other constructs" applies to
disable iff, so as far as the ordering dilemma, I do not think there is one,
again if you think "treat disable just like anything else", you will see
this is just an issue of proper bracketing ... If it can happen with disable
it can happen with anything else. Your example just lacks context, i.e.
clock resolution is not apparent. To see this, try to delete disable iff and
put any other sequence ...

** The proposal only has a deletion of an item from the rewrite rules (see
Annex H), not meant to imply anything beyond that.

The whole idea is NOT to have any special/odd/inferred-by-special-rule
behavior for disable iff in particular but work within what everything else
abides by. We already have inference rules for clocked properties. Disable
iff is just one measly construct, (should be) no different than any other
construct in the language ...

** Please see my last email to Roy, the discussion should not digress into
new ways of doing things ... The whole point is not to ...

Thx.
-Bassam.

--
Dr. Bassam Tabbara
Architect, R&D
Novas Software, Inc.
(408) 467-7893
-----Original Message-----
From: Adam Krolnik [mailto:krolnik@lsil.com] 
Sent: Tuesday, October 26, 2004 12:52 PM
To: bassam@novas.com
Cc: sv-ac@eda.org
Subject: Re: [sv-ac] Errata 269: Asynchronicity of disable iff in relation
to the sampling clock
Hi Bassam;
You suggestion is that the order will be used to specify a synchronous or
asynchronous reset (disable.) E.g.
// Asynchronous reset.
assert property ( disable iff (reset) @(posedge clk)
    an_expression)
    else $error("bad a");
// Synchronous reset.
assert property ( @(posedge clk) disable iff (reset)
   an_expression)
   else $error("bad a");
Is the order of the two elements (disable statement and clock specification)
too implicit, thereby causing user grief simply because they wrote the wrong
order, or added the disable statement "in the wrong place"?
Maybe a more explicit way to show an asynchronous vs a synchronous disable
would be better. I came up with the use of an edge specifier to denote
asynchronous disables.
E.g.
// Asynchronous reset.
assert property ( @(posedge clk) disable iff (posedge reset)
    an_expression)
    else $error("bad a");
// Synchronous reset.
assert property ( @(posedge clk) disable iff (reset)
    an_expression)
    else $error("bad a");
This more closely matches expectations of users who write inferred register
blocks.
always @(posedge clk or negedge rst_n)  // <<< Asynchronous reset.
   if (!rst_n)
     begin
     <reset state>
     end
   else
     begin
     <update state>
     end
vs.
always @(posedge clk)  // <<<  No edge on reset, thus Synchronous.
   if (!rst_n)
     begin
     <reset state>
     end
   else
     begin
     <update state>
     end
     Adam Krolnik
     Verification Mgr.
     LSI Logic Corp.
     Plano TX. 75074
     Co-author "Assertion-Based Design"