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.Received on Sat Apr 21 09:27:49 2007
This archive was generated by hypermail 2.1.8 : Sat Apr 21 2007 - 09:28:16 PDT