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.