Re: [sv-ac] placement of "disable iff"

Hi Ed:

You are right that this idea would eliminate the ability to
make the "disable iff" expression an argument.  But I don't 
think that ability is all that useful because of the restriction
of the "disable iff" to the top level. 

Suppose I have

   module foo;
      
      ...
      
      property boo_with_reset(rst, ...)
         disable iff (rst)
         ...
      endproperty
      
      a1:  assert property (boo_with_reset(rst1,...));
      a2:  assert property (boo_with_reset(rst2,...));
      a3:  assert property (boo_with_reset(rst3,...));
      
      ...
      
   endmodule

Then I get the same effect with 

   module foo;
      
      ...
      
      property boo(...)
         ...
      endproperty
      
      a1:  assert property (disable iff (rst1) boo(...));
      a2:  assert property (disable iff (rst2) boo(...));
      a3:  assert property (disable iff (rst3) boo(...));
      
      ...
      
   endmodule


Best regards,

John H.


> X-MimeOLE: Produced By Microsoft Exchange V6.5.7226.0
> Content-class: urn:content-classes:message
> Date: Thu, 8 Jun 2006 07:36:50 -0700
> Thread-Topic: [sv-ac] placement of "disable iff"
> thread-index: AcaLCBh6n7qyAi0+QxCCzBzVIY8ARgAAKZbQ
> From: "Eduard Cerny" <Eduard.Cerny@synopsys.com>
> X-OriginalArrivalTime: 08 Jun 2006 14:36:51.0899 (UTC) FILETIME=[FB5070B0:01C68B08]
> 
> John,
> 
> a problem may be that you cannot write a property in which the reset
> condition is a formal parameter because verif. statements are not
> parameterizable.
> 
> The introduction of a default reset would be useful, however. =20
> 
> ed
> 
> 
> > -----Original Message-----
> > From: owner-sv-ac@verilog.org=20
> > [mailto:owner-sv-ac@verilog.org] On Behalf Of John Havlicek
> > Sent: Thursday, June 08, 2006 10:29 AM
> > To: sv-ac@verilog.org
> > Subject: [sv-ac] placement of "disable iff"
> >=20
> > All:
> >=20
> > We currently require that "disable iff" be placed only at the top
> > level.
> >=20
> > Discussions in P1800 about the relation of "disable iff" to coverage
> > and action blocks seem to have converged (or be converging) to
> > treating a disabled evaluation as neither "true" nor "false".
> >=20
> > The formal semantics currently allows "disable iff" to be nested.  The
> > main reason for this was to simplify the inductive definition of the
> > semantics.
> >=20
> > In the past, I have had the vision of relaxing the rules on "disable
> > iff" to make it nestable and an analog of PSL "abort".  However, this
> > will not work well with the "neither true nor false" treatment of
> > disabled evaluations.
> >=20
> > Now my vision is different--that "disable iff" be restricted to the
> > top level eternally.  In the future, we can add accept/reject as in
> > ForSpec, or the PSL abort syntax, to serve as the nestable operators
> > that yield "true" or "false" results.
> >=20
> > Assuming that we will keep "disable iff" at the top level eternally,
> > there is little or no use in putting it inside property declarations.
> > To me, it seems we should think of "disable iff" as attached to the
> > assertion directives.
> >=20
> > What do people think about making this change syntactically? =20
> >=20
> > The change would introduce a backwards compatibility problem -- people
> > who have written "disable iff" expressions inside property
> > declarations would have to move them to the relevant assertion
> > directives.
> >=20
> > The benefit would be a syntactic enforcement of the top-level rule.
> > And I think the usage of "disable iff" would be simplified.  People
> > would not have to worry about not being able to instantiate a property
> > with a "disable iff" inside another property.
> >=20
> > I think we should also add a default "disable iff" at the module level
> > (and in other scopes where it makes sense) and have the default apply
> > to all the assertion directives that do not have otherwise specified
> > "disable iff" expressions.
> >=20
> > Best regards,
> >=20
> > John H.
> >=20