Subject: Re: vunits...
From: David Van Campenhout (dvc@verisity.com)
Date: Thu Jun 12 2003 - 10:32:26 PDT
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
> >
> >
> >
> >
>
>
>
This archive was generated by hypermail 2b28 : Thu Jun 12 2003 - 10:33:16 PDT