Subject: comments on pages 63-78: verification layer
From: Anthony McIsaac (anthony.mcisaac@st.com)
Date: Fri Oct 18 2002 - 08:33:41 PDT
Comments on the verification layer section pages 67-73.
page 67 line 43 +
assume:
Do we want a restriction that an assumed property has to be an
FL property (not an OBE property)?
Also for assume_guarantee (p68)?
page 70 line 46.
vmode and vprop types:
I'm not sure how useful these constructs are. This is of course a language
design issue, and the constructs were in the March 20 document; but they
were not discussed by the committee, and don't appear to be needed to meet
any of the committee's requirements. It seems to me that the options for
development of the language with regard to how verification tools use
Sugar specifications are still open, and the introduction of constructs
such as vprop and vmode limits the options, before we really know what
users will find they need. I suggest that we consider removing them from
the standard at this stage.
In the March 20 document, it was stated that verification units were the
only entities that can be directly accessed by verification tools; and
that tools might choose to ignore all verification units except vprops.
These statements are not in the draft LRM (sensibly, in my view; I
would think tools might want to access named objects within verification
units).
The only reason left in the draft LRM is the support of mix'n'match
verification, selecting certain groups of assertions to verify under
certain sets of constraints. But this can be done evn if all verifcation
units are called vunit. It appears that vprop and vmode are decorative
constructs, that don't make any difference to the way the verification
units are used.
I don't think we're yet at the stage of knowing what users will want to do.
One thing that some users might want could be a way of turning a vunit
that consists of just a list of property declarations into either a
list of assertions or a list of assumptions. A lot of this will be
done by the tools, rather than by the language. At some point, it may
become clear that certain features are generally required, and that
tool developers are creatinng constructs to support them. Of course, the
group looking after Sugar will then have to move quickly to specify standards
for the constructs.
This archive was generated by hypermail 2b28 : Fri Oct 18 2002 - 08:38:38 PDT