Subject: issues from original LRM review
From: Anthony McIsaac (anthony.mcisaac@st.com)
Date: Tue Oct 21 2003 - 09:54:13 PDT
Ther are some issues that I believe were unresolved in the
original LRM review last year, before the release of v1.0,
and don't appear to be in the list of those being tracked.
I don't know exactly what has been discussed in the LRM
subcommittee: forgive me if these points have been covered.
1. Can Boolean HDL expressions and PSL expressions be combined?
If so, with what operators?
- the HDL logical operators don't apply to PSL expressions, so
it must be PSL logical operators?
e.g. is A && prev(B) a valid Boolean? Or is this technically
an FL property that is not a Boolean?
[the answer being that, as things stand, it is an FL property
but not a Boolean]
- if the latter, does this raise an issue for the definition
of rose(s) as !s & prev(s)? - or any other issues?
And is r == prev(r) even a legal expression?
Should we be defining prev as an extension to Verilog?
2. section 4.4.1, definition of unclocked properties. There
was a question about properties that are unclocked at the
top level, but have clocked subproperties. And a suggestion
to remove definition of unclocked properties as nothing
depends on it. The whole point was considered minor, and it
was seen as harmless to leave the text as it was for the
time being, but with a note to tidy the point up later.
3. More substantial issue of flavors.
The LRM seems to imply that the flavor has to be uniform
throughout a PSL specification. In particular, the flavor
of a verification unit should correspond to the flavour
of the HDL unit it is bound to. (4.3.2.1 and 4.3.2.2).
I'm not sure that this is really the case, but:
First request - can the LRM be explicit about exactly
what the rules are?
Second request - can they be as relaxed as possible.
e.g. so that its's possible:
- to write a spec as a PSL verification unit, without
knowing the language of the design
- to inherit a Verilog flavor verification unit in a
VHDL flavour verification unit
- to use a VHDL path name for a design variable in
a Verilog flavor verification unit
4. (noticed in the course of writing the last comment).
The title of Box 1 on page 21 appears to be wrong.
5. vprop and vmode.
I am still unhappy with these constructs, and renew
my request to remove them from the standard language.
I made some comments on this point in a mail to the
reflector dated 25 October 2002. I also explained my
reasons to the LRM subcommittee, which I repeat here.
After the discussion on Monday, I feel more strongly that they are
not the right constructs, and that they should be removed at some
stage.
The suggestion was that some users and tools might want to take
advantage of these constructs, for building the main vunits out
of vprops and vmodes.
There are two ways one might make use of vprop and vmode:
(i) The tool could make use of the fact that it knows a vunit contains
only assertions, or does not contain assertions, to carry out the
verification task, as prescribed by the language, in some more efficient
or convenient way.
(ii) The tool could treat the verification directives in vprops and
vmodes differently from those in vunits.
I don't think (i) is in question here. It is very easy in any case for
tools to detect that a verification unit contains only assertions, or
doesn't contain assertions.
So we must have (ii) in mind. For example, vprops might never appear on
the menu of vunits that the user can activate. The trouble is that
other tools might choose to distinguish completely differently between
how they treated vprops and vunits, and therefore specifications
wouldn't be portable between tools. The point of having a standard language
is that significant differences in the way tools treat specifications
are defined by the language. If we want tools to treat vprops and vunits
differently, we should specify how they are to do so.
In any case, it seems to be overkill to have a verification directive,
assert, to tell tools to verifiy the property, and then another feature
of the language to tell them actually to pay attention to the directive.
If we really need to do this, it indicates we've got something wrong with
the language.
I was expecting to build up vunits something like
vunit prop1 {
property P1 = .....
}
vunit prop2 {
property P2 = ....
}
vunit mode1 {
property M1 = .....
}
vunit rule {
inherit prop1;
inherit prop2;
inherit mode1;
assert prop1.P1;
assert prop2.P2;
assume mode1.M1;
}
-- Anthony McIsaacSTMicroelectronics Limited 1000 Aztec West Almo
-- Anthony McIsaac
STMicroelectronics (R&D) Limited 1000 Aztec West Almondsbury Bristol BS32 4SQ
Tel: ++44 (0)1454 462466 Fax: ++44 (0)1454 617910
Email: Anthony.McIsaac@st.com
This archive was generated by hypermail 2b28 : Tue Oct 21 2003 - 09:54:58 PDT