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

Hi,

The standard mentions that a boolean expression is evaluated
similarly to a procedural 'if':

"17.4 Boolean expressions

The outcome of the evaluation of an expression is boolean and is
interpreted the same way as an expression is interpreted in the
condition of a procedural if statement. In other words, if the
expression evaluates to X, Z, or 0, then it is interpreted as
being false. Otherwise, it is true."

If this reduction to boolean is applied to the SVA 'if' condition,
then there is no problem.

regards
Stig

Doron Bustan skrev:
> Yaniv,
> 
> the problem that you point has implications to SVA "if else".
> 
> "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.
> 
> Doron
> 

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