Subject: comments on pages 63-78: modelling layer
From: Anthony McIsaac (anthony.mcisaac@st.com)
Date: Fri Oct 18 2002 - 08:33:45 PDT
Comments on the modelling layer section, pages 75-78.
One specific comment:
page 75 line 30
We have a production for HDL_Declaration, but HDL_Declaration
doesn't appear at all in the formal syntax (we do have
module_or_generate_item_declaration). Do we need an extra
possibility HDL_Declaration in the Flavor Macro HDL_DECL,
or have I misunderstood the conventions?
Generally, I didn't get a good picture from this chapter
and chapter 7 of what the modelling code in a verification
unit looks like. In particular:
- is it true that you must be able to insert the
modelling code in a verification unit into the Verilog
module that the verification unit is bound to, and still
have a legal Verilog module?
(probably not, but how close is this to being true?)
- what has to be declared inside the verification unit
before it is used there?
- can the modelling code include modules?
(from the formal syntax, it looks as if it can't)
- can the built-in functions be used in the modelling code,
or only in expressions inside properties?
(from the formal syntax, it looks as if this is the case;
if so, this should be stated in the main chapter)
- can unions only be used in expressions inside properties?
(Again, it looks from the formal syntax as if this is the case,
but here I'm not sure why we need this. I can see that the
interpretation of the built-in functions depends on a
clock context, so their semantics may be tricky if they
appear outside properties. But I would have thought that
the union construct would be useful in the modelling
code for state machines, allowing non-deterministic
transitions. I can also see that it's useful to piggy-back
the semantics of the modelling layer on top of that of Verilog,
so that if the original HDL plus the modelling code is
in fact legal Verilog, then there's no work to be done; but
it looks as if structs and integer ranges extend Verilog in
any case.)
Back to more specific comments:
page 76 line 25.
For consideration in future versions:
Is "union" sufficient for conveniently expressing all the
non-determinism one might want? What about an 8-bit register
taking a non-deterministic value?
Generally again: I suspect that work will need to be done in future
versions of the LRM to specify precisely the semantics of everything
for multi-valued logic. Is it worth stating at some point in this
LRM that the semantics of properties etc. are only fully defined
for boolean logic?
-- Anthony McIsaacSTMicroelectronics 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 : Fri Oct 18 2002 - 08:38:59 PDT