Re: [sv-ac] call to vote on Mantis 1932

Hi Manisha:

I was principal author of a set of documents submitted back in April
2002 to the Accellera FVTC that proposed the Extended CBV language.
The documents gave a comprehensive definition of a linear temporal
logic that includes strong and weak LTL operators, recursion, local
variables, negation, etc.

For the present discussion, the essential document from that set is 

(*) http://www.eda-twiki.org/vfv/hm/att-0772/01-ecbv_statement_semantics.ps.gz

The definition given there is automata-theoretic in its approach and
is very general.  In fact, in that document the strong and weak LTL
operators are derived forms, since they can be represented in terms of
recursion and specification of the acceptance condition for the
recursive form.  This is really just casting the well-known mu
calculus representations of the LTL operators in terms of recursion,
with the acceptance condition determining whether a least fixed
point or greatest fixed point quantifier applies.

The document imposes no language restrictions on the intermingling of
recursion, local variables, LTL operators, negation, etc.  However, in
order to ensure that the negation operator corresponds to language
complementation, some regularity is needed in the way the negation
operators appear in relation to the recursion graph and the acceptance
conditions.  The document gives simple graph-theoretic conditions and
proves that they are sufficient to ensure well-behavedness of the
semantics.

It has always been my vision that this full integration and
interoperation of all the features is where SVA should ultimately go.

For practical reasons I have not yet pushed for the full feature
integration and interoperation.  By imposing restrictions on the use
of negation with recursive forms, we were able to give a simpler
characterization of the semantics of recursion for SV 3.1a than the
one based on automata theory in (*).

I have no problem with the approach in 1932 of allowing only
restricted intermingling of LTL with recursion because I am confident
that the roadmap for generalizing the interaction of all of these
features presented in (*) remains achievable.

Best regards,

John H.

> X-MimeOLE: Produced By Microsoft Exchange V6.5
> Content-class: urn:content-classes:message
> Date: Mon, 28 Jan 2008 08:42:34 -0800
> X-MS-Has-Attach: 
> X-MS-TNEF-Correlator: 
> Thread-Topic: [sv-ac] call to vote on Mantis 1932
> Thread-Index: AchX47IoIQT6c/YKR9OkolDCn7Ox6gJtNz1wAAPxgmAACPHiwA==
> From: "Kulshrestha, Manisha" <Manisha_Kulshrestha@mentor.com>
> X-OriginalArrivalTime: 28 Jan 2008 16:42:36.0810 (UTC) FILETIME=[C9DEBEA0:01C861CC]
> 
> Hi,
> 
> I just wanted to understand the restriction for strong property in
> recursive properties and not weak ones. I do not think we should
> introduce it now. I even feel that combining these new operators (like
> until and always) in recursive properties is going to be very confusing.
> I was just wondering if we should restrict it for even weak properties.
> What do you think ? Do you think we loose anything important here by not
> allowing weak forms of these new operators ? Since PSL did not have a
> concept of recursive anyway, I think no one has written these
> combinations yet.
> 
> Thanks.
> Manisha
> 
> -----Original Message-----
> From: Bustan, Doron [mailto:doron.bustan@intel.com]=20
> Sent: Monday, January 28, 2008 6:16 PM
> To: Kulshrestha, Manisha; john.havlicek@freescale.com;
> sv-ac@server.eda.org
> Subject: RE: [sv-ac] call to vote on Mantis 1932
> 
> Hi Manisha,
> 
> >>1. In 16.12.1, it is mentioned that 'not' operator switches the
> strength
> >>of a property. I think it will be useful to have this information in
> >>16.12.2 also.
> 
> [[DB:]] Ed and Dmitry have the same comment so I have moved this
> paragraph to the negation part.
> 
> 
> >>2. Why are weak forms of these new operators  allowed in recursive=20
> >>properties (and not strong ones) ?
> 
> [[DB:]] We only allow weak constructs in recursive properties because
> alternating strong and weak in a "recursive cycle" makes it difficult to
> define the semantics. I guess that "strong" could be an exception
> because it cannot be applied on properties, and thus cannot be part of a
> "recursive cycle". I am a little afraid to get it in at this time in
> case I missing something. Do you think it is important to have it now?
> We can always put it latter (there are other restrictions that can be
> lifted as well.)
> 
> >>3. In the changes for multiclocked properties, it does have 'until' as
> 
> >>one of the operators which requires special care but not 'until_with'.
> >>Is that an oversight ?
> 
> 
> [[DB:]] I guess it is an oversight, I have add it now.
> 
> Thanks
> 
> Doron
> 
> ---------------------------------------------------------------------
> Intel Israel (74) Limited
> 
> This e-mail and any attachments may contain confidential material for
> the sole use of the intended recipient(s). Any review or distribution by
> others is strictly prohibited. If you are not the intended recipient,
> please contact the sender and delete all copies.

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