Group C.1 Issues
[3.2] vunit binding, reusable verification IP,
scope and visibility of names, overriding definitions:
Issues
5, 19, 64,
65, 75, 77,
92,
100, 101, 103
23, 30, 33,
54, 76, 93,
26, 56, 112,113,
114, 116, 119,
120.
Discussion
Minutes of meetings on group C.1:
Resolution
- The LRM should not prescribe a particular use model
- e.g., it should NOT say " ... the ONLY way to do so and so is ..."
- The LRM should specify what happens if you use certain features
- if vunit A inherits vunit B, or vunit A is bound to HDL module or
instance B, then
- the names visible in B become visible in A
- A may override assignments made to objects in B
- the LRM should nonetheless specify the following restriction, for
consistency:
- if vunit A inherits vunit B, and B is bound to module/instance M,
then A must also be bound to the same M
- furthermore, if A, B are both bound to M, and neither A nor B inherit
from the other, then
the names in A are not visible in B, and the names in B are not visible
in A
- tools are free to go beyond what the LRM requires, e.g.,
- to assume a given assertion in order to prove another assertion
- to verify an assumption in a containing context
- to check both assertions and assumptions in simulation
- the LRM should define a new kind of verification unit:
- a "vpkg" (for want of a better name) is a vunit that contains only
declarations
- (typically parameterized) sequence and/or property decls
- perhaps also HDL function, object decls (but these might limit
reusability)
- a "vpkg" can only inherit another vpkg
- a "vpkg" must not be bound to an HDL module/instance
- therefore a "vpkg" cannot contain a reference to an HDL design
- if a vpkg C can contain an object X, and C is inherited by two vunits
A, B, then
then a single global object C.X is visible in both A and B
- the LRM should refine the definitions of vmode and vprop
- a vmode is a vunit that defines the environment within which
assertions should be verified; therefore
- it may contain anything except assert/cover directives
- it may inherit a vmode iff neither are bound, or both are bound
to the same module/instance
- it may override (assignments to) an object whose name has been
imported via inheritance or binding
- it may instantiate any vunit provided that the instantiated
instance looks like a vmode
e.g., it may instantiate a bimodal vunit provided that it
selects the assumptions and not the assertions
- a vprop is a vunit that defines the design requirements to check;
therefore
- A vprop may contain anything except assume/restrict/fairness
directives
- it may inherit a vmode iff neither are bound, or both are bound
to the same module/instance
- it may NOT override (assignments to) an object whose name has
been imported via inheritance or binding
- it may instantiate any vunit provided that the instantiated
instance looks like a vprop
- e.g., it may instantiate a bimodal vunit provided that it
selects the assertions and not the assumptions
-
We do not need both binding and instantiation for the same vunit.
It is sufficient to achieve the two by composition. See details
(here)
- A parameterized vunit need not be in the same flavor as the
context in which it is used. Cross-language instantiation of a parameterized vunit
should work the same as cross-language instantiation of an HDL module.
Additional Notes
-->
LRM Changes
Erich's proposal for LRM changes can be found here
Changes required in the proposal:
- Add the definition of a default verification unit.
- Add examples
- 5.2.3 - add "original" to the keyword table and to the built-in functions
- 2.3 - vmode Add to 2nd paragraph that a vmode should be able to inherit.
- The restrictions on vprop should remain as in the current LRM (only assert and cover are allowed).
- Additional use models from Jan 21
should be described in the appendix.
- Change the restriction on binding to the same module: The inheriting vunit and the inherited
vunit should be bound either to the same module or to instances of the same module,
or not be bound to any module.
- Dotted names can be used to resolve conflicts and it is the responsibility
of the tool to detect the problematic cases and give an error in
these cases.
The LRM should describe the difference between accepting different
dotted names: when is it an instantiation and when is it an error.
- Overriding must be explcit. The keyword "override" will be added to the language.
It should be applied both to design signals and to input signals.
- extend the proposal to allow local variables:
- The scope of a local variable is the SERE in which it was declared.
Revised proposal by NSS
Required changes to the proposal:
vunit instantiation should be moved to section 7.2, after the definition of parameterized vunits.
add the following after the definition of parameterized
vunits:
It is an error if a vunit is both bound and instantiated or both inherited
and instantiated
Need to add the note: A parameter list can be empty
Add: a vunit with no binding is considered bound to the top module.
It is possible to define a vunit that is not bound to anything by adding the keyword "abstract" before the vunit keyword.
If there is more than one top module then it is an error to have an unbound vunit that is not abstract.
add the restriction that we cannot override design signals in a vprop.
Clarify: signals in an unbound
vunit that is inherited by a bound vunit
will get the binding of the inheriting vunit.
The proposal should say that an error message should be given
if after resolution of the inheritance tree duplicate driving
was produced for the same object, even when different
reference names were used
think of a way to change the proposal in a way that the overriding
affects only vunits in the same verification task/run.
Assume "X" is defined in vunit v1. Clarify how "x" should be refered to
in a vunit v2 in the cases 1) v1 instantiated in v2 2) inherited in v2.
In 1) "x" can be accessed only by its dotted name in
2) also by its direct name.
Make the instantiation label mandatory.
describe what happens if a named construct is overridden.
Need to remove the text about hidden names.
Last updated on 5 Feb 2008.