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

Hi Ed:

I'm not sure about the verbosity claim.  "boo_with_reset" has 11 more
characters than "boo", plus we save a comma and, likely, a following
space, for a total of 13 fewer characters per instance.  
"disable iff ()" adds 14 characters per instance, so the net is +1 
character per instance.  but we also save a "disable iff (rst)" and
"rst, " in the declaration.  So we're ahead on character count if
there aren't too many instances ... :)

Your last point seems really to be about any non-backward-compatible 
change.

J.H.


> X-MimeOLE: Produced By Microsoft Exchange V6.5.7226.0
> Content-class: urn:content-classes:message
> Date: Thu, 8 Jun 2006 08:09:12 -0700
> Thread-Topic: [sv-ac] placement of "disable iff"
> thread-index: AcaLDKJZp7DDJPePTLG9ooXwU4G8ywAALXYg
> From: "Eduard Cerny" <Eduard.Cerny@synopsys.com>
> Cc: <sv-ac@verilog.org>
> X-OriginalArrivalTime: 08 Jun 2006 15:09:13.0955 (UTC) FILETIME=[80DEAB30:01C68B0D]
> 
> 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=20
> 
> > -----Original Message-----
> > From: John Havlicek [mailto:john.havlicek@freescale.com]=20
> > 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"
> >=20
> > Hi Ed:
> >=20
> > You are right that this idea would eliminate the ability to
> > make the "disable iff" expression an argument.  But I don't=20
> > think that ability is all that useful because of the restriction
> > of the "disable iff" to the top level.=20
> >=20
> > Suppose I have
> >=20
> >    module foo;
> >      =20
> >       ...
> >      =20
> >       property boo_with_reset(rst, ...)
> >          disable iff (rst)
> >          ...
> >       endproperty
> >      =20
> >       a1:  assert property (boo_with_reset(rst1,...));
> >       a2:  assert property (boo_with_reset(rst2,...));
> >       a3:  assert property (boo_with_reset(rst3,...));
> >      =20
> >       ...
> >      =20
> >    endmodule
> >=20
> > Then I get the same effect with=20
> >=20
> >    module foo;
> >      =20
> >       ...
> >      =20
> >       property boo(...)
> >          ...
> >       endproperty
> >      =20
> >       a1:  assert property (disable iff (rst1) boo(...));
> >       a2:  assert property (disable iff (rst2) boo(...));
> >       a3:  assert property (disable iff (rst3) boo(...));
> >      =20
> >       ...
> >      =20
> >    endmodule
> >=20
> >=20
> > Best regards,
> >=20
> > John H.
> >=20
> >=20
> > > 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)=20
> > FILETIME=3D[FB5070B0:01C68B08]
> > >=20
> > > John,
> > >=20
> > > 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.
> > >=20
> > > The introduction of a default reset would be useful, however. =3D20
> > >=20
> > > ed
> > >=20
> > >=20
> > > > -----Original Message-----
> > > > From: owner-sv-ac@verilog.org=3D20
> > > > [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"
> > > >=3D20
> > > > All:
> > > >=3D20
> > > > We currently require that "disable iff" be placed only at the top
> > > > level.
> > > >=3D20
> > > > Discussions in P1800 about the relation of "disable iff"=20
> > to coverage
> > > > and action blocks seem to have converged (or be converging) to
> > > > treating a disabled evaluation as neither "true" nor "false".
> > > >=3D20
> > > > The formal semantics currently allows "disable iff" to be=20
> > nested.  The
> > > > main reason for this was to simplify the inductive=20
> > definition of the
> > > > semantics.
> > > >=3D20
> > > > In the past, I have had the vision of relaxing the rules=20
> > on "disable
> > > > iff" to make it nestable and an analog of PSL "abort". =20
> > However, this
> > > > will not work well with the "neither true nor false" treatment of
> > > > disabled evaluations.
> > > >=3D20
> > > > Now my vision is different--that "disable iff" be=20
> > restricted to the
> > > > top level eternally.  In the future, we can add=20
> > accept/reject as in
> > > > ForSpec, or the PSL abort syntax, to serve as the=20
> > nestable operators
> > > > that yield "true" or "false" results.
> > > >=3D20
> > > > Assuming that we will keep "disable iff" at the top level=20
> > eternally,
> > > > there is little or no use in putting it inside property=20
> > declarations.
> > > > To me, it seems we should think of "disable iff" as=20
> > attached to the
> > > > assertion directives.
> > > >=3D20
> > > > What do people think about making this change syntactically? =3D20
> > > >=3D20
> > > > The change would introduce a backwards compatibility=20
> > problem -- people
> > > > who have written "disable iff" expressions inside property
> > > > declarations would have to move them to the relevant assertion
> > > > directives.
> > > >=3D20
> > > > The benefit would be a syntactic enforcement of the=20
> > top-level rule.
> > > > And I think the usage of "disable iff" would be=20
> > simplified.  People
> > > > would not have to worry about not being able to=20
> > instantiate a property
> > > > with a "disable iff" inside another property.
> > > >=3D20
> > > > I think we should also add a default "disable iff" at the=20
> > module level
> > > > (and in other scopes where it makes sense) and have the=20
> > default apply
> > > > to all the assertion directives that do not have=20
> > otherwise specified
> > > > "disable iff" expressions.
> > > >=3D20
> > > > Best regards,
> > > >=3D20
> > > > John H.
> > > >=3D20
> >=20