Subject: Re: vunits...
From: Anthony McIsaac (anthony.mcisaac@st.com)
Date: Tue Jun 24 2003 - 02:14:38 PDT
David,
I agree with you that inheritance of vunits does not
provide all that one might want for building
hierarchical property specifications.
The discussion in the committee has concentrated largely
on the language for specifying individual properties
(the temporal and boolean layers). Now that people are
starting to use the language in a variety of verification
tools, it may be useful to consider carefully what
capabilities are required for the management and
maintenance of properties and specifications.
Am I right in thinking that you want to be able specify
something like the following (I'm using a non-committal
term "property_group" rather than "vunit")?
property_group bus_protocol(r,g) {
property request_not_retracted(r,g): always (r && !g -> next(r));
property grant_eventually_asserted(r,g): always(r -> eventually! g);
property no_unsolicited_grants(r,g): always( g -> r);
assume request_not_retracted(r,g);
assert grant_eventually_asserted(r,g);
assert no_unsolicited_grants(r,g);
}
vunit my_interface_is_bus_compliant(my_design) {
instantiate bus_protocol(my_request,my_grant);
}
and to be able to move in two directions:
(i) instantiating bus_protocol for different blocks
with different signal names
(ii) using bus_protocol to build larger property groups,
for example
property_group core_bus_bridge(r_in, g_out, r_out, g_in) {
bus_protocol(r_out, g_in);
core_protocol(r_in, g_out);
}
It does look to me as if these capabilities are
significantly more than is provided by the vunit
construct. I think that this construct is useful
for the time being, as a straightforward way
of managing properties; and it does not rule
out the development of other language features
to improve the way properties can be managed.
But I do agree that it is time to think about
the development of such other features.
Anthony
dvc@verisity.com wrote:
>
> Hi,
>
> I would like to raise two issues regarding vunit/vprop/vmodes. The
> first one is a request for clarification; the second one is a request
> for enhancement.
>
> 1. Section 7.2. in the LRM should clarify that the vunit/vprop/vmode
> constructs are declarations (definitions).
> So, you can read a bunch of vunits into a verification tool, but
> the tool shouldn't do anything (beyond compilation) until you tell
> it which vunit you want to verify.
> As such there is no concept of instantiation of vunits in PSL.
>
> 2. The lack of explicit instantiation construct for vunits limits
> the kinds of hierarchical sets of properties that can be constructed.
>
> I am arguing for an instantiation construct for vunits that
> (1) is separate from the definition of a vunit, and
> (2) would allow for the specification of what hdl instance
> the vunit instance is to be bound to.
>
> Such a construct would allow for hierarchical sets of properties to
> be constructed. These hierarchies can be totally different from the
> hdl hierarchy. It is still up to the user to tell the verification
> tool which hierarchical vunit to use. One can think of a number of
> variations to specify a subset of the hierarchy.
>
> In the current language def, a vunit can be bound to an hdl module,
> which has the effect of duplicating the definition and binding for
> each instance of that module. This is the only feature that allows
> for duplicating a vunit, where the different copies are bound to
> different hdl entities (though in a very limited way.)
>
> In the current language def, the inherit construct bears some
> similarity to instantiation, but the inherited vunit keeps its own
> hdl binding (which defaults to the top-level hdl module).
>
> What do you think?
> Below is a series of messages Cindy and I exchanged on this topic.
>
> David
> ------------------------------------------------------------------------
> David Van Campenhout <dvc@verisity.com> Verisity Design
> Tel.: +1 650 934-6878 Fax: +1 650 934-6801
>
> Cindy Eisner writes:
> > david,
> >
> > i agree that the inherit construct is different than an instantiation, but
> > not that it doesn't allow you to build hierarchical structures. if your
> > vunit doesn't contain any modeling code (that is, if it is a vprop), then
> > there is no difference between an instantiation and an inherit. the
> > difference is only in the case there is modeling code such that the same
> > signal is declared in the inheriting and inherited unit. so i don't follow
> > your point. and we do use sugar with simulation, in focs, as well as in
> > formal, and haven't seen the need to instantiate a vunit.
> >
> > but perhaps i am missing your point. please feel free to bring this up
> > over the reflector. we both would get more inputs that way from people who
> > agree/disagree, which could only make the discussion more productive.
> >
> > regards,
> >
> > cindy.
> >
> > Cindy Eisner
> > Formal Methods Group Tel: +972-4-8296-266
> > IBM Haifa Research Laboratory Fax: +972-4-8296-114
> > Haifa 31905, Israel e-mail:
> > eisner@il.ibm.com
> >
> >
> > David Van Campenhout <dvc@verisity.com> on 11/06/2003 18:34:53
> >
> > Please respond to dvc@verisity.com
> >
> > To: Cindy Eisner/Haifa/IBM@IBMIL
> > cc:
> > Subject: Re: vunits...
> >
> >
> > Cindy,
> >
> >
> > Thanks for your response.
> >
> > I think that the analogy with verilog modules is broken in that vunits
> > don't allow one to build hierarchical structures; the inherit
> > construct is quite different from an instantiation. So, vunits are
> > essentially flat containers.
> >
> > The lack of the ability to build up hierarchical congregations of
> > properties, may be problematic if I want to tell a verification tool
> > to check a large number of properties. (This is unlikely for an FV
> > tool, but checking all properties is the normal use model with a
> > simulator.)
> >
> > I see a need for a construct for instantiation vunits. The
> > instantiation construct should allow for the specification of the
> > hierarchical hdl path the instance is to be bound to. This would allow
> > one to build up a hierarchical set of properties. You can then still
> > tell the verification tool which top-level container (vunit) you want
> > to check.
> >
> > Best regards,
> >
> >
> > David
> >
> >
> >
> > Cindy Eisner writes:
> > > david,
> > >
> > > >It seems to me that PSL lacks a clear separation between instantiation
> > > >and declaration for the vunit/vmode/vprop constructs.
> > > >
> > > >It seems to me that any definition of a vunit/vmode/vprop
> > > >automatically instantiates the definition's content. This may not be
> > > >desired if the vunit/vmode/vprop definition contains directives.
> > >
> > > a vunit is not automatically instantiated - there is nothing to do the
> > > instantiating. it is more like a module in verilog. you can read a
> > bunch
> > > of modules into a synthesis tool, but unless you tell your synthesis
> > tool
> > > which one to synthesize, it will just sit there. likewise, you can read
> > a
> > > bunch of modules into a simulator, but you must tell the simulator which
> > is
> > > the top level module to simulate. so, you can read a bunch of vunits
> > into
> > > a verification tool, but the tool shouldn't do anything (beyond
> > > compilation) until you tell it which vunit you want to verify.
> > >
> > > does this make sense? if so, i agree that this should be clarified in
> > the
> > > lrm.
> > >
> > > regards,
> > >
> > > cindy.
> > >
> > > Cindy Eisner
> > > Formal Methods Group Tel:
> > +972-4-8296-266
> > > IBM Haifa Research Laboratory Fax: +972-4-8296-114
> > > Haifa 31905, Israel e-mail:
> > > eisner@il.ibm.com
> > >
> > >
> > > David Van Campenhout <dvc@verisity.com> on 10/06/2003 19:00:33
> > >
> > > Please respond to dvc@verisity.com
> > >
> > > To: Cindy Eisner/Haifa/IBM@IBMIL
> > > cc:
> > > Subject: vunits...
> > >
> > >
> > > Hi Cindy,
> > >
> > >
> > > Before posting the following to Eric's list of things to be clarified
> > > I wanted to check it with you...
> > >
> > > It seems to me that PSL lacks a clear separation between instantiation
> > > and declaration for the vunit/vmode/vprop constructs.
> > >
> > > It seems to me that any definition of a vunit/vmode/vprop
> > > automatically instantiates the definition's content. This may not be
> > > desired if the vunit/vmode/vprop definition contains directives.
> > >
> > > Along the same line, I read that the inherit construct causes an
> > > instantiation of the content of the inherited unit in the inheriting
> > > unit.
> > >
> > > To facilitate libraries and re-use, I would expect to be able to
> > > define a set of properties, assert them, and group these definitions
> > > and assertions into a vunit, and then instantiate the whole vunit.
> > > (For example, the vunit may describe a PCI bus, and the DUT may have
> > > several PCI interfaces.) The instantiation should specify the HDL
> > > binding.
> > >
> > > Am I missing something?
> > >
> > >
> > > David
> > >
> > >
> > >
> > >
> >
> >
> >
-- 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 : Tue Jun 24 2003 - 02:15:24 PDT