Subject: RE: [vhdl-200x] 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 Verilog-centric 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 get-outs 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 Verilog-flavor 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 multi-valued logic are not generally equivalent, and mapping from a multi-valued 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 multi-valued 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 multi-valued 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 active-low signals, and similarly that an expression such as (s='1') or its equivalent will be used to detect the active state of active-high 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 built-in 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