RE: [sv-ac] "if else" definition needs corrections - mantis 1786

Hi,

But this would select (the right-most) a bit from the argument and thus
not compatible with  Verilog if - else. I think that it should have the
same interpretation and Verilog.

ed


> -----Original Message-----
> From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On 
> Behalf Of Korchemny, Dmitry
> Sent: Sunday, April 22, 2007 10:32 AM
> To: john.havlicek@freescale.com; jonathan.bromley@doulos.com
> Cc: dbustan@freescale.com; Yaniv.Fais@freescale.com; sv-ac@eda.org
> Subject: RE: [sv-ac] "if else" definition needs corrections - 
> mantis 1786
> 
> Hi all,
> 
> Would it be appropriate to say that if (b) P1 else P2 needs to be
> defined as (bit'b |-> P1) and (!(bit'b) |->P2)?
> 
> Thanks,
> Dmitry
> 
> -----Original Message-----
> From: owner-sv-ac@server.eda.org 
> [mailto:owner-sv-ac@server.eda.org] On
> Behalf Of John Havlicek
> Sent: Saturday, April 21, 2007 7:27 PM
> To: jonathan.bromley@doulos.com
> Cc: dbustan@freescale.com; Yaniv.Fais@freescale.com;
> sv-ac@server.eda.org
> Subject: Re: [sv-ac] "if else" definition needs corrections - mantis
> 1786
> 
> Hi Jonathan:
> 
> I think your comments about whether "b" is 1-bit are relevant.
> 
> I also agree that if we align property "if..else" with the 
> Verilog "if..else", then we get whatever is good or bad about
> that (e.g., "if (b) P else Q" is not equivalent to "if (!b) Q 
> else P").
> 
> My opinion is that it is probably better to align property 
> "if..else" semantics with Verilog semantics so that people
> will know that they have to use the same devices to deal with
> 4-state conditions.
> 
> After some revisions, I think we should be able to get a satisfactory
> rewrite rule, perhaps by using some explicit casting, that keeps us
> aligned with Verilog "if..else" semantics.
> 
> J.H.
> 
> > > "if (b) P1 else P2" is defined in annex E as a shortcut to
> > > "(b |-> P1) and (!b |-> P2)". The problem with this definition
> > > is that b = X, neither P1 nor P2 are required to hold. This is
> > > inconsistent with SV procedural "if else" where the else block
> > > should be executed.
> > >
> > >  I enter a mantis item 1786.
> > > 
> > > A simple correction that will fix that is to define "if (b) 
> > > P1 else P2"
> > > as a shortcut to "((b ===1) |-> P1) and ((b!==1) |-> P2)".
> > > 
> > > But with this definition, "if (b) P1 else P2" is not equivalent to
> > > "if (!b) P2 else P1", so I am not sure what do we need.
> > 
> > I don't think there is anything you can do about this. 
> > Unknown conditionals in the bifurcating "if...else" have
> > always been handled like this in Verilog...
> > 
> >   if (b) P1 else P2;  ===>  if (b) P1 else P2 maybe P2;
> > 
> > and if you invert the test, of course you get
> > 
> >   if (!b) P2 else P1 maybe P1;
> > 
> > which is not exactly the same.  Since we cannot specify the
> > "maybe" branch explicitly in a single "if" clause, it seems 
> > to me that there is no way out of this.
> > 
> > Note that your "b===1" formulation is correct only if b
> > is a single bit.  It might be preferable to say
> > 
> >   ( ((b!=0)===1) |-> P1 ) and ( ((b!=0)!==1) |-> P2 ).
> > 
> > (Or is this in a context where b is known to be only
> > one bit wide?  If so, apologies for the irrelevance.)
> > -- 
> > Jonathan Bromley, Consultant
> > 
> > DOULOS - Developing Design Know-how
> > VHDL * Verilog * SystemC * e * Perl * Tcl/Tk * Project Services
> > 
> > Doulos Ltd. Church Hatch, 22 Market Place, Ringwood, Hampshire, BH24
> 1AW, UK
> > Tel: +44 (0)1425 471223                   Email:
> jonathan.bromley@doulos.com
> > Fax: +44 (0)1425 471573                           Web:
> http://www.doulos.com
> > 
> > The contents of this message may contain personal views which 
> > are not the views of Doulos Ltd., unless specifically stated.
> > 
> > -- 
> > 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.
> 
> -- 
> 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.