RE: [sv-bc] Re: if-else

The problem is not with if-else, but with the definition of equality
with how pessimism is reduced.


The LRM is clear that if(expr) is evaluated as if(expr!=0)

The LRM is not clear in its definition of equality how the result of
each bit-for-bit comparison is used to producer the final result. It
needs to say the individual results are reduction and'ed for ==, and
reduction or'ed for !=.

> -----Original Message-----
> From: owner-sv-bc@server.eda.org [mailto:owner-sv-bc@server.eda.org]
On
> Behalf Of Bresticker, Shalom
> Sent: Thursday, November 01, 2007 5:57 AM
> To: john.havlicek@freescale.com; sharp@cadence.com
> Cc: sv-ac@server.eda.org; sv-bc@server.eda.org
> Subject: RE: [sv-bc] Re: if-else
> 
> John,
> 
> Sorry I did not respond earlier.
> 
> The semantics of multi-bit equality comparison are explained in Mantis
> 1974.
> 
> As you say,
> > > If I use reduction or to get the semantics of the multi-bit
> > expression
> > > as a cond_predicate, then a bit with value 1 is enough to make the
> > > result known even if other bits may be x or z.
> 
> If any bit of the condition is 1, then the condition is true.
> 
> Does this help?
> 
> Regards,
> Shalom
> 
> > -----Original Message-----
> > From: owner-sv-bc@server.eda.org
> > [mailto:owner-sv-bc@server.eda.org] On Behalf Of John Havlicek
> > Sent: Thursday, November 01, 2007 12:37 PM
> > To: sharp@cadence.com
> > Cc: sv-ac@server.eda.org; sv-bc@server.eda.org
> > Subject: [sv-bc] Re: if-else
> >
> > Hi Steven:
> >
> > I am having trouble figuring out from the SV LRM the
> > semantics of multi-bit 4-state equality comparison and
> > multi-bit 4-state cond_predicate in procedural if-else.
> >
> > I have looked at 11.4.5 and 12.4, but what I find there does
> > not say clearly what to do with multi-bit 4-state expressions.
> >
> > Can you clarify?  Are there other sections of the LRM that
> > are relevant?  Is there a Mantis item on this subject?
> >
> > J.H.
> >
> > > Date: Wed, 31 Oct 2007 15:33:03 -0500
> > > Cc: doron.bustan@intel.com, john.havlicek@freescale.com
> > > From: John Havlicek <john.havlicek@freescale.com>
> > > Reply-To: john.havlicek@freescale.com
> > > X-OriginalArrivalTime: 31 Oct 2007 20:33:05.0803 (UTC)
> > > FILETIME=[3DD3DDB0:01C81BFD]
> > >
> > > Hi Shalom:
> > >
> > > We have Mantis 1786 in SV-AC to align the semantics of property
> > > if-else with the procedural if-else statement when 4-state
> > values are
> > > involved.
> > >
> > > Jonathan Bromley suggested using
> > >
> > >   !(bit'(b!=0))
> > >
> > > to get a condition for the "else" of  "if(b) .. else ..".
> > >
> > > I made a little table for this:
> > >
> > >   b   b!=0  bit'(b!=0)  !(bit'(b!=0))
> > >   -----------------------------------
> > >   0     0        0            1
> > >   1     1        1            0
> > >   x     x        0            1
> > >   z     x        0            1
> > >
> > > which shows that this works for 1-bit b.
> > >
> > > I am trying to convince myself that the same expression works for
> > > multi-bit.
> > >
> > > I am having trouble understanding the semantics of the procedural
> > > if-else when multi-bit expressions are used in the cond_predicate.
> > >
> > > If I use reduction or to get the semantics of the multi-bit
> > expression
> > > as a cond_predicate, then a bit with value 1 is enough to make the
> > > result known even if other bits may be x or z.
> > >
> > > I don't know what happens if I use the "b != 0" because the
> > > description of "!=" is not clear for multi-bit expressions.
> >  However,
> > > the LRM does say that
> > >
> > >    if (expression)
> > >
> > > is equivalent to
> > >
> > >    if (expression != 0)
> > >
> > >
> > > Can you clarify?  Is there a Mantis item on this?
> > >
> > > J.H.
> ---------------------------------------------------------------------
> Intel Israel (74) Limited
> 
> This e-mail and any attachments may contain confidential material for
> the sole use of the intended recipient(s). Any review or distribution
> by others is strictly prohibited. If you are not the intended
> recipient, please contact the sender and delete all copies.
> 
> --
> This message has been scanned for viruses and
> dangerous content by MailScanner, and is
> believed to be clean.
> 


-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.