Subject: RE: [vhdl200x] Implicit conversion, Overloading, & Strong Typing
From: Erich Marschner (erichm@cadence.com)
Date: Tue Dec 30 2003  10:49:32 PST
Evan,
 The LRM talks a lot about boolean conditions, but it defines
 the value of a Boolean expression as:

 > In a given flavor of PSL, the value of a Boolean HDL
 expression is interpreted as a logical value according to the
 > same rules that govern interpretation of that expression
 as the condition of an if statement in that flavor.

 This appears to be a Verilogcentric statement, and my guess is that
 it's there to handle Verilog x and z. Could the problem be fixed simply
 by changing this to:

 "For the VHDL flavor of PSL, the value of an expression is interpreted
 as a Boolean true if that expression evaluates to
 STD.Standard.Boolean'(True), or that expression is of an enumerated type
 and evaluates to the values '1' or 'H'. In all other cases, the
 expression is interpreted as a Boolean false."
Your proposal goes beyond the definitions of True and False in Section 3, by allowing values of types other than Boolean, Bit, and std_ulogic to be interpreted as True/False logical values. If we adopt what you've suggested, we also need to extend the definitions in Section 3 to match. (In any case, there is currently a mismatch, so we need to do something here.)
 There seem to be some getouts that might allow this: the PSL LRM states
 that it overloads the logical operators, and HDL_EXPR seems to be
 definable as a macro in some way. If this is possible, then we get
 conciseness in PSL expressions without changing the base language at
 all. Anyone who's using negative logic and is concerned that the PSL
 expression looks like an incorrect boolean can simply expand out their
 expression in the normal way.
I'm not sure what point you are making. The flavor macros, of which HDL_EXPR is one, are used only to enable us to define the common portions of PSL once, regardless of the HDL with which it is used. Flavor macros simply enforce the notion that, in a given PSL flavor, one must consistently use the syntax of the same HDL for the expressions that make up an assertion.

 You also quote the definitions of true and false in 3.1.20
 and 3.1.52:

 >  STD.Standard.Boolean'(False),
 >  STD.Standard.Bit'('0'), and
 >  IEEE.std_logic_1164.std_logic'('0')
 > are all interpreted as the logical value False, and the values
 >  STD.Standard.Boolean'(True),
 >  STD.Standard.Bit'('1'), and
 >  IEEE.std_logic_1164.std_logic'('1')
 > are all interpreted as the logical value True.

 Why is it necessary to leave out the metalogic values? This was
 presumably because Verilog's x and z are neither true nor false, but the
 'if' statement interpretation in the LRM makes 1 true, and 0,x,z false.
 If this is the case, then presumably there's no need to ignore the VHDL
 metalogic values, and they could also be defined as false? Does this
 mean that 3.1.20 and 3.1.52 are incorrect for Verilogflavor PSL?
I'm not a formal logician, so I probably cannot give you a complete and coherent answer, but I'll try to explain what I think I understand.
The fundamental point is that Boolean logic and multivalued logic are not generally equivalent, and mapping from a multivalued logic system to Boolean will inevitably lose information. We can define a reversible mapping between Boolean True / False and std_logic '1' / '0', so we can consider these pairs to be equivalent. With a small loss of information, we can even extend this to include 'H' and 'L', so that {'H','1'} reduces to {'1'} and {'L','0'} reduces to {'0'}, as the synthesis subset has done. This is acceptable because 'H' and 'L' are considered to represent weak versions of '1' and '0' respectively. But any other mappings are unacceptable because they lose too much information  all the rest of the metalogical values ('U', 'X', 'Z', 'W', '') are strongly associated with both '0' and '1'.
Consider the following example, supposing that S is of (sub)type std_logic, and 'to_boolean' converts std_logic '1' or 'H' to Boolean True:
if to_boolean(S)
then <case1a>
else <case2a>
end if;
if to_boolean(not S)
then <case2b>
else <case1b>
end if;
If S has a value in {'1', 'H', '0', 'L'}, then <case1a>=<case1b>, and <case2a>=<case2b>, as we would expect if S were of type Boolean. But if S has a value in {'U', 'X', 'Z', 'W', '' }, then both if statements will take the else branch. This implies that (S = not S), which is a contradiction in Boolean logic, though it is legal in multivalued logic. So we can consistently interpret std_logic values '1', 'H', '0', 'L' as Boolean values, for example, in the condition of an if statement. But the other (metalogical) values 'U', 'X', 'Z', 'W', '' do not admit consistent Boolean interpretations.
PSL semantics are based upon Boolean logic. This implies several things. First, the conditions in PSL constructs must have (or be consistently interpretable as) Boolean values. Second, if we want verification results to be valid, the set of assumptions and preconditions used in verification must not contain any contradictions. If contradictions occur in Boolean logic, they reduce to False. So if a contradiction occurs in the antecedent of an implication such as (stimulus > correct response), the implication reduces to (False > correct response), which is vacously true because False implies anything. (An implication a>b is equivalent to (not a or b), so an implication False > X is equivalent to (not False or X), which is clearly True, independent of X.) So, we need to do everything we can to avoid introducing contradictions through inconsistent interpretation of multivalued logic expressions. To that end, we decided to consistently give std_logic '1' and '0' their obvious** interpretations, and r
equire the user to explicitly convert any other value to Boolean (e.g., by comparison to a literal).
Note that inconsistent interpretation of metalogical values is also the root of the issue about positive vs. negative logic. If reset_n is a std_logic signal, there is a difference between (reset_n = '1') and (not reset_n = '0'). The first expression interprets metalogical values as False; the second expression interprets metalogical values as True. This is why automatic conversion of metalogical values to Boolean is problematic  it depends upon the values being converted should be interpreted as positive logic or negative logic signals.
**Some may argue that it is not obious that '1' should map to True and '0' to False  why not the other way round, or either way, depending upon whether positive or negative logic is involved? But the definitions in IEEE Std 1164 assume positive logic  e.g., in the truth table for AND  and for that matter the position numbers of True and False in type Boolean also suggest this mapping. In any case, the choice of mapping between True/False and '1'/'0' is independent of the notion of 'active' and 'inactive'. We assume that an expression such as (s='0') or its equivalent will be used to detect the active state of activelow signals, and similarly that an expression such as (s='1') or its equivalent will be used to detect the active state of activehigh signals.
No doubt there is a simpler, more concise explanation of the above, but that's the best I can do for now.
 On the separate issue of overloading +/ for conciseness, I have some
 code which does this in C++: I overload unary plus to get a value out of
 a complex class, to make it look like a simple builtin data type. It
 seemed like a good idea at the time, but it's confusing to read and
 leads to maintenance problems: it's only a matter of time before someone
 removes a '+' on the grounds that unary + 'does nothing'.
I can see the potential for dropping + because it appears superfluous. On the other hand, the compiler would immediately respond with a type mismatch error, so the value of the + would become evident quickly.
Regards,
Erich
This archive was generated by hypermail 2b28 : Tue Dec 30 2003  10:51:33 PST