Re: [vhdl-200x] Implicit conversion, Overloading, & Strong Typin g

Subject: Re: [vhdl-200x] Implicit conversion, Overloading, & Strong Typin g
From: Andy D Jones (andy.d.jones@lmco.com)
Date: Tue Dec 30 2003 - 07:25:39 PST

Erich,

Thanks for clearing that up. I and possibly others have touched around the issue of where PSL came from, and exactly what it interprets.  I am troubled that it does not even interpret std_ulogic'('H') as True.

But I REALLY like the unary +/- operator overloading!!!  This gives us an intuitive, short(est)-hand way to test SUL (or bit) for oneness or zeroness, while avoiding the assumption of active high logic, without messing with the language, and, in my opinion, without weakening a foundational strength of VHDL.  This shows again that VHDL is strong enough to create useful solutions without resorting to weakening the language itself.  (There are other issues that do need to be addressed at the language level, but this is not one IMHO).

I like it so much, I may adopt it myself, even before the packages get created/updated!

Your example also illustrates another shortcoming of any single "to_boolean()" function: metavalues cannot be uniformly interpreted for both active high and active low logic.  Using "not -reset_n" is the correct way to state that "reset_n is not asserted", but "to_boolean(reset_n)", or it's implied equivalent, simply says "reset_n is '1' or 'H').  In the former, 'X' is interpreted as true, but in the latter, 'X' is interpreted as false.  For the original question (if reset_n is not asserted), the implied call does not return the "correct" result.  To get the correct result using implied conversion (the same result as if the reset signal was active high), you'd have to write:

if reset_n then
  null;
else -- reset not asserted
  just_do_it(swoosh);
end if;

Now which one is more verbose?

Andy Jones



Erich Marschner wrote:
I guess it is time for me to comment on this issue, in part because I'm the one who proposed the definitions for True and False in the PSL LRM, which Steve has cited below.  I hope the following helps clarify the situation rather than adding fuel to the debate.

1. Rationale for non-Boolean Conditions in PSL

PSL adopted somewhat liberal data type requirements for conditions for two reasons:

  a. We were required to define a Verilog 'flavor' of PSL first, and 
      Verilog interprets almost anything as a condition,  so this flexibility 
      was required for the Verilog flavor.

  b. PSL was defined as a separate language, so it was not necessary to 
      follow VHDL's strong typing constraints, and therefore for 
      consistency it seemed reasonable to extend this flexible interpretation 
      of conditions to the VHDL flavor.

In the context of PSL becoming a part of VHDL 200x, the first reason is perhaps irrelevant, and the situation upon which the second was predicated is no longer the case.  It is therefore quite reasonable to reevaluate the question of what kind of expressions should be allowed as conditions in PSL directives that are part of VHDL 200x.  

2. Implicit Conversion to Boolean in PSL in VHDL 200x

The main goal of this whole discussion is to make PSL directives easy to read and write.  Since one PSL directive may involve many conditions in a compact group, any simplification (while retaining clarity!) would potentially benefit PSL directives more than other constructs that involve conditions.  If conditions must always be written in the form "name = value", PSL directives in VHDL 200x will be longer, syntactically more complex, and somewhat more difficult to read, than they will be in other contexts.

The simplest form of implicit conversion would be to adopt what Accellera PSL v1.01 does today.  That is, in adopting portions of the PSL definition as part of VHDL 200x, include the statement that, in conditional expressions within VHDL 200x assert/cover directives derived from PSL, the values 
  - 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.  This would be consistent with the Accellera PSL definition, and it would not affect any existing VHDL constructs.

It has been suggested that implicit conversion should be user-definable and that it should be extended to other areas in which conditions occur.  The idea of an implicitly invoked 'cond' function is an interesting one, and not without precedent (in implicitly invoked resolution functions).  But I don't think it is possible to define a single function that maps from a std_logic expression to a Boolean value, whether that function is invoked implicitly or explicitly.  If such a function were possible, then it would have to map every value of std_ulogic to either True or False, yet that is not what PSL does today, nor is this consistent with the 1076.3 mapping for synthesis.  The values 'U', 'X', 'Z', 'W', '-' are not considered to be either True/1 or False/0.  So at minimum, two conversion functions are necessary - one that checks for a '1-ish' value, and one that checks for a '0-ish' value - and possibly additional functions to check for the above metalogical values.  Having 
t
 wo (or more) functions would also avoid the concern about inappropriately assuming positive logic.  At the same time, having two functions involved would preclude implicit invocation, or else would complicate the definition so much that it would be difficult to use.  

3. Explicit Conversion to Boolean in PSL in VHDL 200x

Someone suggested using simple conversion functions such as is1(...),  is0(...), isX(...), etc.  I get the impression that such short function names as these are still not acceptable to some, and I have to admit that I would find them getting in the way of reading and writing a PSL assertion.  Would they be acceptable if they were shortened to a single character?  If so, perhaps this could be accomplished (mostly) by overloading the unary +/- operators for type std_ulogic, as follows:

  -- 'high' function for std_ulogic:
  function "+" (v: std_ulogic) return boolean is
  begin
    return To_X01(v) = '1';     -- i.e., v='1' or v='H'
  end;  

  -- 'low' function for std_ulogic:
  function "-" (v: std_ulogic) return boolean is
  begin
    return To_X01(v) = '0';     -- i.e., v='0' or v='L'
  end;

These could be added to IEEE.Std_logic_1164, or defined in a separate package (with pros and cons for each of these two approaches).  With these definitions, one could write a PSL assertion such as the following:

    signal enable, reset_n, req, ack, int_n: std_logic;
      ...
    assert always ( +enable and not -reset_n -> ( ( +req -> eventually +ack ) abort -int_n ) ) ;

i.e., "whenever enable is high and reset_n is not low, if req is asserted (high), then eventually ack must also be asserted (high), unless int_n goes low".

4. PSL Assertions in a Mixed-Language Context

All of the above notwithstanding, the larger problem we have been discussing recently is how to write PSL assertions that can apply to either a VHDL description or a Verilog description, or even to a mixed-language description.  We might want to write an assertion that could potentially apply to either a VHDL implementation (using std_ulogic as the typical signal type) or to a Verilog implementation (using the base Verilog data type).  If the language environment within which the assertion is to be interpreted might change, we can't be too particular about the data types of the conditions involved.  Ideally, it should be possible to write a set of assertions that comprise an abstract specification, even before we decide whether to implement the spec in VHDL or in Verilog.  To accomplish this, we need to avoid building in language dependencies that will tie the assertions too strongly to the underlying implementation language.  There are many issues to address here, and any s
o
 lution is bound to have limitations - e.g., such assertions may need to refer only to named conditions, or use generic Boolean operators rather than HDL-specific operators.  

I don't know yet whether the VHDL 200x effort can or should even try to do anything to enable this more general use of PSL, but it would be nice if the addition of PSL to VHDL 200x does not hinder cross-language use of PSL assertions.  For example, overloading unary +/- as mentioned above might make it easier to write/read PSL assertions in VHDL 200x, but requiring the use of those functions - or the equivalent, VHDL-specific comparison operators - would make assertions written for VHDL 200x non-portable to Verilog, where those facilities do not exist.  So, whether or not overloading unary +/- makes sense for VHDL 200x users, if we want to achieve cross-language portability of assertions, we probably need to build in flexible data type rules for conditions, of the sort that exist today in PSL v1.01.  Even so, this flexibility need not affect constructs other than those derived from PSL.

Regards,

Erich


-------------------------------------------
Erich Marschner, Cadence Design Systems
Senior Architect, Advanced Verification
Phone: +1 410 750 6995   Email: erichm@cadence.com
Cell:    +1 410 294 2599   Email: erichm@comcast.net 

|  -----Original Message-----
|  From: Bailey, Stephen [mailto:SBailey@model.com]
|  Sent: Friday, December 19, 2003 7:14 PM
|  To: 'vhdl-200x@eda.org'
|  Subject: RE: [vhdl-200x] Implicit conversion, Overloading, & Strong
|  Typin g
|  
|  
|  PSL defines boolean equivalence for std_ulogic.  From the 
|  1.01 version of the PSL LRM:
|  
|  "3.1.20 False: An interpretation of certain values of 
|  certain data types in an HDL.
|  In the Verilog flavor, the single bit value 1'b0 is 
|  interpreted as the logical value False.
|  
|  "In the VHDL flavor, the values 
|  STD.Standard.Boolean'(False), STD.Standard.Bit'('0'), and 
|  IEEE.std_logic_1164.std_logic'('0') are all interpreted as 
|  the logical value False.
|  
|  "In the GDL flavor, the Boolean value 'false' and bit value 
|  0B are both interpreted as the logical value
|  False.
|  
|  "3.1.52 True: An interpretation of certain values of certain 
|  data types in an HDL.
|  In the Verilog flavor, the single bit value 1'b1 is 
|  interpreted as the logical value True.
|  
|  "In the VHDL flavor, 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.
|  
|  "In the GDL flavor, the Boolean value 'true' and bit value 
|  1B are both interpreted as the logical value True.
|  
|  "5.1 HDL expressions
|  
|  A Boolean HDL expression, shown in Box 11 [this is the 
|  syntax productions], is any HDL expression that the HDL 
|  allows to be used as the condition of an if statement."
|  
|  NOTES:
|  1.  I added some formatting (vertical white space) to 
|  increase readability.
|  
|  2.  Ben Cohen has written in an earlier post that he has a 
|  proposal to modify the 1.1 LRM currently being written to 
|  include the meta-logic values of std_ulogic in the 
|  definition of false.
|  
|  3.  For those who may not be aware:
|  
|    - Boolean expressions are the fundamental building block 
|  of sequences and properties (that is, they are prevalent 
|  throughout a PSL specification).
|  
|    - There are tools today (Safelogic, NC, ModelSim, others) 
|  that already support VHDL-flavor of PSL.
|  
|    - You can embed PSL inside the HDL and include arbitrary 
|  HDL within your PSL sections.  (Again, the tools already 
|  support this.)
|  
|  PSL does not require COND as they have already defined a 
|  boolean equivalence.  VHDL needs the COND proposal to be 
|  consistent with PSL and to improve language efficiency in 
|  expression (or whatever you wish to call "typing efficiency").
|  
|  -Steve Bailey
|  
|  > -----Original Message-----
|  > From: owner-vhdl-200x@eda.org 
|  > [mailto:owner-vhdl-200x@eda.org]On Behalf
|  > Of Hamish Moffatt
|  > Sent: Friday, December 19, 2003 4:30 PM
|  > To: 'vhdl-200x@eda.org'
|  > Subject: Re: [vhdl-200x] Implicit conversion, Overloading, & Strong
|  > Typin g
|  > 
|  > 
|  > Bailey, Stephen wrote:
|  > > - Do nothing to address an enhancement request that is 
|  elevated in
|  > > priority due to the desire to incorporate PSL as the property
|  > > specification capability in VHDL.  (I already pointed out 
|  > the obvious
|  > > language inconsistencies that arise if we do nothing.)
|  > 
|  > Why is the COND operator required for PSL?
|  > 
|  > 
|  > Hamish
|  > 
|

This archive was generated by hypermail 2b28 : Tue Dec 30 2003 - 07:29:44 PST