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

Hi John,

true, but
- little more verbose :-)
- does not remind the user , if it is a library of properties, to add a
reset (if any).
- there are libraries of properties which do have reset as argument,
legacy code...

ed 

> -----Original Message-----
> From: John Havlicek [mailto:john.havlicek@freescale.com] 
> Sent: Thursday, June 08, 2006 11:03 AM
> To: Eduard.Cerny@synopsys.COM
> Cc: john.havlicek@freescale.com; sv-ac@verilog.org
> Subject: 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
>