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

erich,

>I think perhaps you meant "bit or bitvector", since we define both of
these type classes in PSL, whereas we don't
>define "boolean vector".

yes, that is what i meant.

>If you can suggest a way to determine reliably whether to default to Bit
or BitVector, I'd be happy to adopt it.

whether or not the signal is ever used with an index. if you want the code
to be portable, then always specify the range of a vector explicitly.

regards,

cindy.

--------------------------------------------------------------------
Cindy Eisner
Formal Methods Group
IBM Haifa Research Laboratory
Haifa 31905, Israel
Tel: +972-4-8296-266
Fax: +972-4-8296-114
e-mail: eisner@il.ibm.com

"Erich Marschner" <erichm@cadence.com> on 01/02/2005 17:25:05

To: Cindy Eisner/Haifa/IBM@IBMIL
cc: <ieee-1850-extensions@eda.org>
Subject: RE: Proposal for Group H (Issue 21), Portable PSL - first
       detailed draft

Cindy,

| 2. my understanding of your proposal is that if the vunit
| and the design are in the same flavor, then no signals need
| to be declared in the vunit, and that the only case in which
| a user must declare design signals is if the vunit and the
| design are going to be in different flavors. is that
| correct?

Almost. It would be appropriate to declare local signals any time the
vunit is intended to be portable, i.e., any time the vunit and the design
*might be* in different flavors.

| ... if so, then i propose that the default type be
| boolean or boolean vector. in other words, if a design
| signal is not declared, it is assumed to be a boolean or a
| boolean vector. this would eliminate 99% of the
| declarations, making the resulting psl code much easier to
| read and write.

I think perhaps you meant "bit or bitvector", since we define both of these
type classes in PSL, whereas we don't define "boolean vector".

I can see assuming that a signal is of PSL type class Bit, and therefore of
some distinguished HDL type in each flavor that is interpretable as type
class Bit - e.g., STD.Standard.Bit in VHDL, the built-in type in Verilog,
'bit' in SystemVerilog, 'sc_bit' in SystemC. (These are all two-valued
types; we could also default to four-valued types, to minimize potential
information loss through the conversion.) I agree that this would avoid
many declarations.

I have more difficulty seeing how we could define the default to be bit OR
bitvector. We need some decision procedure to pick one or the other. I
suppose you are suggesting that we pick the appropriate one of these to
match the structure of the HDL data type, and translate accordingly. But
this would require having the corresponding HDL code available when the PSL
is compiled, and I'm not sure we want to require that. We could also base
the decision on whether or not the signal in question is ever used with an
index, but that would not be guaranteed to give the right answer in all
cases. So I think I'd be inclined to stop at one default type - type class
Bit, with a distinguished HDL data type in that class for each flavor.

If you can suggest a way to determine reliably whether to default to Bit or
BitVector, I'd be happy to adopt it.

Regards,

Erich

| -----Original Message-----
| From: Cindy Eisner [mailto:EISNER@il.ibm.com]
| Sent: Tuesday, February 01, 2005 9:40 AM
| To: Erich Marschner
| Cc: ieee-1850-extensions@eda.org
| Subject: Re: Proposal for Group H (Issue 21), Portable PSL -
| first detailed draft
|
|
|
|
|
| erich,
|
| two things:
|
| 1. avigail and i both like the idea of nondet() (without
| parameters) very much.
|
| 2. my understanding of your proposal is that if the vunit
| and the design are in the same flavor, then no signals need
| to be declared in the vunit, and that the only case in which
| a user must declare design signals is if the vunit and the
| design are going to be in different flavors. is that
| correct? if so, then i propose that the default type be
| boolean or boolean vector. in other words, if a design
| signal is not declared, it is assumed to be a boolean or a
| boolean vector. this would eliminate 99% of the
| declarations, making the resulting psl code much easier to
| read and write.
|
| cindy.
|
| --------------------------------------------------------------------
| Cindy Eisner
| Formal Methods Group
| IBM Haifa Research Laboratory
| Haifa 31905, Israel
| Tel: +972-4-8296-266
| Fax: +972-4-8296-114
| e-mail: eisner@il.ibm.com
|
| "Erich Marschner" <erichm@cadence.com>@eda.org on 31/01/2005 20:14:59
|
| Sent by: owner-ieee-1850-extensions@eda.org
|
|
| To: <ieee-1850-extensions@eda.org>
| cc:
| Subject: 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 Tue Feb 1 07:51:37 2005