[sv-ac] Re: 16.14.3 and simulation centric semantics.

Hi Johan:

I don't think I disagree with any of your points.  Some of
your questions have come up, and people have had differing
opinions about them.

I do not think it will be feasible for us to give a formal
definition of the set of runs of a system.

It seems more likely that we will be able to make definitions
that presume that a set of runs is given, with the intuition
that the set consists of the runs of a system of interest.

J.H.

> Date: Tue, 4 Sep 2007 14:51:01 +0200
> From: Johan =?iso-8859-1?Q?M=E5rtensson?= <johan.martensson@jasper-da.com>
> Cc: sv-ac@eda-stds.org, john.havlicek@freescale.com,
>         "Bresticker, Shalom" <shalom.bresticker@intel.com>
> Content-Disposition: inline
> X-OriginalArrivalTime: 04 Sep 2007 12:51:04.0987 (UTC) FILETIME=[416346B0:01C7EEF2]
> 
> Hi Dimitry,
> 
> I regard annex F as agnostic between simulation and formal verification.
> It gives a relation (of satisfaction) between a run and a formula.  A
> relation of this sort is a prerequisite for defining both when a
> simulation tool should report an error for a formula on a run and when a
> formal tool should report validity or counterexample for example.
> 
> What seems missing from the formal semantics in annex F is a definition
> of the semantics for the different concurrent assertion statements.
> 
> It seems a semantics for the concurrent assertion statements would have
> to be given differenty for the case of simulation and formal verification
> respectively.
> 
> For example for assert_property_statement in simulation the problem is
> to relate a concrete run and a property so the relation from Annex F
> seems to be more or less directly applicable, whereas in formal we need
> to say something about how the formula should relate to the members in
> the set of possible runs of the system.
> 
> It seems an exact formal verification semantics can and should be given
> to assume_property_statement in relation to assert_property_statement in
> terms of the set of runs of a system, whereas for simulation maybe an
> exact semantics is not really feasible and/or desirable.
> 
> Currently I don't think there is a great risk of confusion as to the
> formal verification semantics for asserts and assumes since I guess it
> is more or less straightforward how it should be formulated.
> 
> In the case of cover_property_statement the case is not so clear I think.
> 
> One intuition is to have the tool search for a trace where the property
> is exemplified. This may be pretty straigtforward in case the property is a
> simple sequence: simply find a (finite) trace where the sequence matches
> at least once.
> 
> But what is desirable for properties in general?
> 1) Implication/Vacuity
>  For example 'cover property r|=> s' for some sequences r and s. In this
>  case any trace where the sequence r doesn't match is a witness for the
>  property. Is it enough to present such a trace or should the tool look
>  for a more interesting trace, a trace where r ##1 s matches, for example?
> 2) Infinite match
>  In case the sequence is weakly embedded (mantis 1932) for example
>  'cover property a[*0:$] ##1 b' for a design where b can never happen
>  but where there are infinite runs where a is true from some point
>  onward. Should the tool present an looping trace in this case.
> 3) Liveness
>  Are there some special considerations w.r.t. cover of liveness properties?
>  
> For a formal tools company supporting SVA you are under pressure from
> customers to support as many constructs as possible from the LRM (and/or
> which they have been using for simulation).
> 
> Now when an official semantics is lacking the temptation is to provide
> some idiosyncratic semantics that will then maybe not be forwards
> compatible and/or compatible with what happens in other tools.
> 
> With mantis 1768 we get a cover_sequence_statement. I would be happy if
> we could give a well defined formal verification semantics for it and
> then maybe state that for cover_property_statement the formal
> verification semantics is not defined.
> 
> Best Regards,
> 
> Johan M
> 
> On Tue, Sep 04, 2007 at 12:03:44PM +0300, Korchemny, Dmitry wrote:
> > Hi Johan,
> >  
> > Though Clause 16 is in some sense simulation centric, Annex F is not.
> > I agree with you about cover statement, and we had several discussions
> > about it in the past, but haven't made any decision yet. The idea was
> > to define the cover statement as E<formula>, instead of A<formula> as
> > in case of assertions (E = existential quantification, and A =
> > universal quantification) for formal verification and to use it to
> > find a property witness.
> > 
> > Note, however, that coverage is widely used in simulation, and
> > therefore it should be well elaborated for simulation as well.
> > 
> > Thanks, Dmitry
> > 
> > -----Original Message----- From: johan.martensson@jasper-da.com
> > [mailto:johan.martensson@jasper-da.com] Sent: Thursday, August 30,
> > 2007 6:55 PM To: sv-ac@eda-stds.org Cc: Korchemny, Dmitry;
> > john.havlicek@freescale.com; Bresticker, Shalom Subject: 16.14.3 and
> > simulation centric semantics.
> > 
> > Hi,
> > 
> > I think the informal semantics of chapter 16 of the LRM is very
> > simulation centric in certain places and a semantics for the context
> > of formal verification is more or less unspecified there.
> > 
> > A case in point is 16.14.3. I don't think the text there makes much
> > sense in the context of formal verification.  A semantics for cover of
> > sequences could well be given for formal, I think. I'm not so sure
> > about cover of properties in general though.
> > 
> > Best Regards,
> > 
> > Johan M

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.