Proposal for Group H (Issue 21), Portable PSL - first detailed draft

Proposal for Group H (Issue 21), Portable PSL
===================================

Revised Sketch
============
30 Jan 2005

Requirements:
1. Allow a vunit written in a given flavor of PSL to be applied to a design module in any HDL.
2. Do not require an extra level of hierarchy, even if the vunit flavor and the module HDL are different.
3. Rely on de facto standards for mixed language simulation to define inter-language type translation.

To address item (1), we will have to decouple the flavor macro HDL_MOD_NAME from the flavor of the vunit, i.e., that flavor macro must either become a production or must be replaced with syntax that is not based upon the grammars of the various HDLs.

To address item (2), we can simply state that the type translation from signals S1, S2, ..., Sn in the design module to references S1, S2, ..., Sn in the vunit are done implicitly using the same conventions as for mixed language simulation, where such translations would occur via an instantiation of a module written in one HDL within a module written in a different HDL, but without any instantiation and therefore without an additional level of hierarchy.

Item (3) is a bit more difficult. Mixed-language simulation relies on translation between two declared signals, e.g., a signal in the instantiating module and a port in the instantiated module, where the types of both are known. In this case, we want to be able to refer to signals in the HDL module (effectively the 'parent' module) from within a corresponding verification unit (effectively the 'child' module) without declaring those signals in the verification unit. This means that the signal types assumed in the verification unit would have to be determined by analysis of the use of those signals, which won't work in all cases, especially given VHDL type determination rules (where the type must be known a priori in order to determine the meaning of operator symbols), and complicated by the PSL rules for interpretation of HDL types as members of PSL type classes.

The only way around this that I can see seems to be to redeclare in the verification unit those signals that are going to be referenced, so there are explicit types defined for those signals in the verification unit. Binding a verification unit to a module would then implicitly associate the local declarations with the objects of the same name in the corresponding module, and if necessary, establish an implicit translation between the module declaration and the verification unit declaration, according to the conventions for mixed-language simulation.

This means that simply redeclaring a signal in a verification unit would not make that signal a free variable for formal verification purposes; one would have to redeclare it AND assign it a non-deterministic value. This change would address part of one request to make such overriding assignments more explicit than they are today. This might also suggest that an additional nondet() function be defined - one that implicitly takes the set of all possible values of the variable to which it is being assigned - e.g.,

    bit foo;
    assign foo = nondet(); // equiv. to assign foo = ({0,1});

Detailed Proposal
==============
31 Jan 2005

4.3.2.2 HDL_MOD_NAME
 - remove this section

5.2.1 HDL Expressions
 - in Informal Semantics,
     - in the 2nd paragraph,
          - change "For each name" to "For each name and operator symbol"
          - change "meaning of the name" to "meaning of the name or operator symbol"
     - in each of the bullets following, change every instance of "this name" to "this name or operator symbol".
     - change bullet (a) to start out "Otherwise, if the current verification unit ..."
     - before bullet (a), add a new bullet that says

        "If this is an operator symbol that is predefined in the flavor of PSL used in this
         verification unit, then the operator symbol has its predefined meaning."

     [These changes acknowledge the fact that (VHDL) operators can be declared in the modeling layer.]

7.2 Verification units
 - in Box 90:
    - change the reference to HDL_MOD_NAME to HDL_Module_Name
    - delete the definition of flavor macro HDL_MOD_NAME
    - add the following production:

      HDL_Module_Name ::=
          /HDL_Module/_Name [ '(' /HDL_Module/_Name ')' ]

 - in the second paragraph following Box 90, change the sentence

    "If the Hierarchical HDL Name is present, then the verification unit is explicitly
     bound to the specified design module or module instance."

   to read as follows:

    "If the Hierarchical HDL Name is present, then the verification unit is explicitly
     bound to the design module or module instance indicated by the HDL module
     name(s) and HDL instance name(s) of the Hierarchical HDL Name. If only one
     HDL module name is given, then the design module with that name is indicated.
     If two HDL module names are given, then the pair of module names indicates a
     VHDL entity and architecture, respectively."

7.2.1 Verification unit binding
 - the second paragraph may need to be weakened a bit, to acknowledge the fact that HDL names and operator symbols may be defined locally, in the verification unit, or (in the case of VHDL) made visible in the verification unit via a use clause, rather than being necessarily defined in the instance to which the vunit is bound. ******

7.2.3 Verification unit scoping rules
[In PSL v1.1, this section does not say clearly what happens when a signal in the design is redeclared in the verification unit, but NOT assigned in the verification unit. Both examples given involve assignments. The proposed revision states that in the absence of an assignment, a redeclared signal implicitly gets the (possibly translated) value of the original signal. A new first example has been added to illustrate this. Also, a new final example has been added to show the use of the new nondet function to make a design signal act like a free variable in formal verification.]

Rewrite this section to read as follows:

7.2.3 Verification unit scoping rules

A verification unit may contain HDL declarations, including declarations of signal names that are also declared in the design module or instance to which the verification unit is bound. This allows a verification unit to import a design signal written in one HDL into a verification unit written using another HDL flavor. It also allows a verification unit to give new behavior to a signal in the design under verification.

/Informal Semantics/

If a design signal name is redeclared in a verification unit bound to a given module or instance, and no assignment is made to that name in that verification unit, then the declaration in the verification unit is implicitly assigned the value of the corresponding design signal at all times. If the design is written in one HDL, and the verification unit is written in a different HDL flavor, then standard conventions for mixed-language simulation are used to translate from the type system of the design's HDL to the type system of the verification unit's HDL.

If a design signal name is redeclared in a verification unit bound to a given module or instance, and that name is assigned a value in that verification unit, then the declaration in the verification unit overrides the declaration in the design module or instance and in any inherited verification units bound to the same design module or instance, and the assignment to that name in the verification unit overrides all assignments to the signal that name in the design and in any inherited verification units bound to the same design module or instance.

/Examples/

Consider the following verification unit:

    vunit ex5a(top_block.i1) {
        wire reqa, temp;
        A5a: assert always (reqa -> next temp);
    }

Verification unit ex5a redeclares signals reqa and temp in a Verilog-flavor verification unit. If the instance to which this verification unit is bound (top_block.i1) is a VHDL design, and that instance contains declarations of signals reqa and temp, then the value of each VHDL signal will be implicitly assigned to the corresponding Verilog signal declared in the vunit, and in the process its value will be translated from the VHDL data type to the corresponding Verilog data type according to the conventions applied in mixed-language simulation.

Now consider the following verification unit:

    vunit ex5b(top_block.i1) {
        wire temp;
        assign temp = ack1 || ack2;
        A5b: assert always (reqa -> next temp);
    }

Verification unit ex5b declares wire temp and also assigns it a value. This could be just an auxiliary statement to facilitate specification of assertion A5b. However, if instance top_block.i1 also contains a declaration of a signal named ‘temp’, then the declaration in ex5b would override the declaration in the design, and the assignment to ‘temp’ in vunit ex5b would override the driving logic for signal ‘temp’ in the design.

Now consider the following verification unit:

    vunit ex5c(top_block.i1) {
        inherit ex5b;
        wire temp;
        assign temp = ack1 || ack2 || ack3;
        A5c: assert always ((reqa || reqb) -> next temp);
    }

Verification unit ex5c inherits ex5b. Both verification units are bound to the same instance and both declare wires named temp. The declaration of temp in the inheriting verification unit takes precedence, so the declaration of (and assignment to) temp in ex5c takes precedence when verifying assertion A5c, and the declaration of (and assignment to) temp in both the design and vunit ex5b are ignored.

Finally, consider the following verification unit:

    vunit ex5d(top_block.i1) {
        wire reqa;
        assign reqa = nondet({0,1});
        A5c: assert always ((reqa || reqb) -> next temp);
    }

Verification unit ex5d redeclares signal reqa, and it also assigns a nondeterministic value of 0 or 1 to the redeclared signal. This causes reqa to behave as a free variable, both in the design and in verifying the assertion A5d.

=============================================================================
=============================================================================

Proposal Sketch (Original)
=============
28 Dec 2004

In the past, we've discussed the possibility of interpreting a single PSL flavor in multiple HDL contexts. While such an approach seems feasible to a point, it would not be easy to apply to the modeling layer, and in any case it has not been widely accepted. This proposal suggests an alternative, which amounts to allowing a vunit written in one flavor to be bound to a design module written in another HDL, with an implicit interface between the two languages.

If a vunit V written in language flavor F is bound to a design module or instance D written in language L, and F/=L, then the effect is as follows:

 - if F is Verilog, then an implicit Verilog module M is created, with an input for each variable name referenced in V;
 - if F is VHDL, then an implicit entity M is created, with an input for each variable name referenced in V;
 - M is implicitly instantiated within D, with the formals of M associated with the same-named actuals;
 - V is bound to M, and therefore the directives in V are interpreted in the context of M.

We might also need to restrict the data types that could be used in such a situation, to stay within the limits of typical mixed-language simulators' ability to do cross-language instantiation. Or, we might just leave this undefined, to leave room for future expansion of those capabilities (e.g., as SystemVerilog comes on line, which will increase the potential for more complex types in cross-language instantiations).

Potential Issues
============

1. This approach depends upon common support for mixed-language design and verification in the underlying tools.

Although such support is not defined in any standard, it has evolved over time in commercial implementations, so this is probably not significant in practice.

2. This approach might require that the vunit 'flavor' be identified up front, to ensure that it is parsed correctly.

This might be necessary because the flavor would no longer be implied by the language of the design module to which the vunit is bound. One solution might be to require the user to specify the flavor of the vunit when compiling it. This might preclude putting vunits of different flavors in the same file, but that might be an acceptable limitation.

3. This approach might require that the design module language be identified up front, for the same reason.

This might be addressed by allowing an optional language identifier as part of the pathname - e.g.,

  vunit V1 (vhdl M) {
    ...
  }

  vunit V2 (verilog M2) {
    ...
  }

4. This approach would create an additional level of hierarchy that might complicate debugging.

This issue might be addressed by defining PSL so that this implicit, additional level of hierarchy is always present (even if F=L), so that it can be handled consistently in all cases - e.g., so that the implicit module or entity M can be ignored in all cases.
Received on Mon Jan 31 10:15:06 2005