Subject: Small correction regarding label names
From: Avigail Orni (ORNIA@il.ibm.com)
Date: Thu Jan 29 2004 - 08:21:03 PST
In my previous message I made a mistake regarding label names in
an unbound vunit:
In the example described, the three copies of label L in V would have
names that include the vunit name V, and not the vunit names A,B,C.
This follows the rule that the label name includes the name of the vunit
in which the label _appears_. So the correct names would be:
a1.a2.a3.V.L
b1.b2.b3.V.L
(pathname of C's binding).V.L
________________________________________________________
Avigail Orni
Formal Methods Group
IBM Haifa Research Laboratory
Tel: 972-4-829-6396 ornia@il.ibm.com
----- Forwarded by Avigail Orni/Haifa/IBM on 29/01/2004 18:13 -----
Avigail Orni
To: vfv@server.eda.org
29/01/2004 14:37 cc:
From: Avigail Orni/Haifa/IBM@IBMIL
Subject: Re: Extensions Subcommittee Meeting - Thursday 22 Jan 2004 - Minutes(Document
link: Avigail Orni)
We have discussed the proposals from last week's meeting in our
group, and as a result we have some comments and questions to be
considered.
1. Flavor macros
In considering whether relaxation of flavor macros might lead to ambiguity,
we have come up with the following example of a Verilog flavor expression:
a ? b : c : d
this has two possible parsings: a ? (b : c) : d and a ? b : (c :
d)
Although a pathname such as b:c might not be allowed in VHDL in such
a context, it would be allowed in a Verilog flavor expression in a PSL
property.
Does this type of ambiguity already exist in the context of mixed
VHDL/Verilog
designs? Does any tool allow mixing VHDL and Verilog in the same
expression?
2. Labels on directives
It is not clear to us how labels will be used in HDL.
Can anyone help us by writing an example that includes both PSL (label
definition)
and HDL (label usage)?
3. Verification unit binding
It seems to us that the proposal to let unbound vunits receive the binding
of an inheriting
vunit implies a certain type of instantiation. We present the following
scenario to check if
everyone agrees with our interpretation, and to clarify a point regarding
label pathnames:
Suppose we have an unbound vunit V, and suppose V is inherited both by
vunit A (bound to
instance a1.a2.a3) and by vunit B (bound to b1.b2.b3).
In this case we must create two copies of V -- one where all signals have
the prefix a1.a2.a3,
and the other with the prefix b1.b2.b3. In other words, we will have two
instances of V.
Note that A may also inherit C which inherits V, and C may have a third
binding.
In that case we need a third copy of V.
So the method for deciding how many copies are needed for V might look like
this:
start with V and travel to all inheritors of V, and continue recursively to
inheritors of inheritors.
When an unbound ancestor is encountered, do nothing.
For a bound ancestor, add a copy of V with prefixes from the ancestor's
binding.
(Later remove duplicate copies that have the same binding)
Implication for labels:
In our previous example, if V contains a label L, then L will have a copy
in each of V's copies,
so the copies of L will be:
a1.a2.a3.A.L
b1.b2.b3.B.L
(pathname of C's binding).C.L
5. Name resolution rules extension
Our feeling is that the new suggested levels (e) and (f) are not of the
same type as
the existing levels (a)-(d). We do think that (e) and (f) should be
specified in the LRM,
but not in the same list as the four existing levels.
Levels (a)-(d) relate to the inheritance mechanism. If a signal S has
several definitions
in different vunits, then the scope of each definition is determined by the
inheritance tree,
and also by the designated current vunit.
For example, suppose S is defined in vunits A and B, where A inherits B.
This situation
is legal if A is the current vunit, but it becomes illegal if a third vunit
C (which inherits A),
is the current vunit.
In this mechanism, there is only one signal S. Once the current vunit is
decided, only one
definition of S is the "winning" definition that actually defines S's
behavior.
This is the idea of the overriding mechanism.
Levels (e) and (f) relate to hierarchical scope: one block enclosed in
another block.
In this mechanism, redefining S inside the inner block actually defines a
new signal,
distinct from the S in the outer block. Each of these S's may have
different behavior,
and we know which S we mean depending on the lexical context.
We think this hierarchical scope for levels (e) and (f) should be explained
in the LRM.
Maybe it is not necessary to define the relative order of priority between
(e) and (f), because
this is actually a result of their relative containment -- in the current
definition, a forall property
can be contained inside a named property declaration, but the opposite
containment is
not allowed. This order may change if we decide to move the forall operator
outside
the directive.
________________________________________________________
Avigail Orni
Formal Methods Group
IBM Haifa Research Laboratory
Tel: 972-4-829-6396 ornia@il.ibm.com
"Erich Marschner"
<erichm@cadence.c To: <vfv@server.eda.org>
om> cc: "Erich Marschner" <erichm@cadence.com>, "Harry Foster" <harry@jasper-da.com>
Sent by: Subject: Extensions Subcommittee Meeting - Thursday 22 Jan 2004 - Minutes
owner-vfv@server.
eda.org
26/01/2004 23:46
Extensions Subcommittee Meeting - 22 Jan 2004 - Minutes
Date: Wednesday January 22, 2004
Time: 9:00am Pacific Time
Phone: US, toll-free: 877-634-9660
Phone: International: 203-566-6784
Passcode: 727384
Attendees:
Erich, Harry, Ben, Surrendra, Johan, Andrew, Avigail
Agenda:
1. Flavor macros
2. Labels on directives
3. Verification Unit binding
4. Messages and Severity
5. Name resolution rules extension
=====================================================================
1. Flavor Macros
- previously agreed to change 3 macros (DEF_SYM, RANGE_SYM, PATH_SYM) to
productions
- disagreement about which symbol to allow for the first two
- no agreement on which single symbol to allow for these two
- propose to revert to allowing all three symbols for each macro
- DEF_SYM shouldn't be an issue - limited occurrences
- RANGE_SYM is the issue - concern that [*a:b] becomes ambiguous (path? or
range?)
- not likely: most range boundaries will be integer constants or
simple identifiers
- could give preference to one interpretation - assume : in [*a:b]
is a RANGE_SYM, not PATH_SYM
2. Labels on Directives
Discussion came to the following conclusions:
- A directive may have a label
- All labels within a vunit must be unique
- A vunit may be explicitly bound to an instance or a module name
- a module name implies binding to each of the instances of that
module
- A directive label must be unique within the scope of the instance to
which its vunit is bound
- The full pathname of a label is determined as follows
- if in a vunit V that is explicitly bound to some instance I, then
I.V.label
- if in a vunit V that is not expllicitly bound, then as before, where
I comes from the vunit
into which this is inherited, or from the tool
- note that we are still flattening vunit inheritance, so vunit names
cannot be used to qualify
name references
- we should use labels as names for directives only - not for declarations
- to avoid confusion between label of, and name declared by,
declaration
- full pathname consists of bound pathname . vunitname . label
- label must be unique among all PSL labels of directives bound to the
same module
3. Unbound modules
- IBM tools do the binding; don't use pathname in vunit
- LRM says vunits are bound to top-level unit by default; this is a
problem
- binding should be determined as follows:
- if an instance pathname is specified, then vunit is bound to that
instance
- if a module name is specified, then vunit is bound to all instances
of that module name
- if neither is specified, and this vunit is inherited by another
one, use binding of the other one
- if still unbound, allow the tool to determine binding
- note that, if vunit a inherits vunit b, and a is explicitly bound, and
you need to bind b
to a different module, then b must be bound explicitly
- pathname is a full path - if multiple tops, then each item has a unique
top, and unique pathname
- signal references inside a vunit should not repeat binding pathname
4. Messages and Severity
- general support for VHDL-style severity and report clauses for
assertions
- report/severity keywords won't conflict with VHDL
- this is a tool-independent, portable solution
- portable if simple strings are used
- could also use language-dependent string construction
operators
- note that we may want to add action blocks later
- action to take on failure is tool-dependent
- assert would have both severity and report
- default severity is ERROR
- cover would have both severity and report
- default severity is what? NOTE? would it ever be anything "more
severe"?
- severity, report don't make sense for other directives
- there may be interest in future extensions for TB to detect assert/cover
activity
5. Name resolution rules extension
- need to address resolution of references to parameters and forall
variables
- brief discussion of Johan's proposal to do this
- general agreement that there is a need to address this
Next Meeting:
- we will meet again on the 29th to discuss this, and hierarchical naming
in PSL in general
-------------------------------------------
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
This archive was generated by hypermail 2b28 : Thu Jan 29 2004 - 08:27:26 PST