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

Hi John,

I agree, definitions in terms of a presupposed set of runs seems
sufficient. 

My greatest concern is actually not with the lack of formal semantics in
this area but rather that there doesn't even seem to be an informal (:-))
formal verification semantics for cover_property_statement. Especially
for non sequence properties.

Best Regards,

Johan


On Tue, Sep 04, 2007 at 08:20:09AM -0500, John Havlicek wrote:
> 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

-- 
------------------------------------------------------------
Johan Mårtensson                 Office: +46 31 7451913
Jasper Design Automation         Mobile: +46 703749681 
Arvid Hedvalls backe 4           Fax: +46 31 7451939
411 33 Gothenburg, Sweden        Skype ID: johanmartensson
------------------------------------------------------------

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