RE: [sv-ac] Comment regarding LTL - Mantis 1932

Hi John,

I agree with requiring the same clock in until, inherited. It was more a
question, no contest.

Regarding the vacuity definition, yes, negation poses problems once you
add the success condition, I tried that too and gave up. 

Regards,
ed

> -----Original Message-----
> From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On 
> Behalf Of John Havlicek
> Sent: Monday, January 28, 2008 9:35 PM
> To: doron.bustan@intel.com
> Cc: Eduard.Cerny@synopsys.COM; john.havlicek@freescale.com; 
> sv-ac@eda.org
> Subject: Re: [sv-ac] Comment regarding LTL - Mantis 1932
> 
> Hi Doron, Ed:
> 
> > >>Regarding the leading clock in until. My point is that 
> the rule deals
> > with
> > >>the case when some clock v flows in P1 until P2. But what 
> if there is
> > no
> > >>clock flowing in? E.g. Assert property (P1 until P2);
> > >>Does the leading clock of P1 have to be the same as in P2? (I hope
> > so.)
> > >>
> > 
> > [[DB:]] Since the leading clock of until is inherited, 
> there must be a
> > clock flowing from the left into the until property; so 
> unless there is
> > an inferred clock, the assertion "assert property (P1 until P2);" is
> > illegal.
> 
> I agree with Doron that if no clock flows in, then this think that
> 
>    assert property (P1 until P2); 
> 
> is illegal.  Whether or not the semantic leading clock of P1 and P1
> must be identical and identicla to the inherited clock depend on 1683.
> If 1683 is rejected, then any non-inherited clocks of P1 and P2 must
> be identical and also identical to the inherited clock.
> 
> > 
> > The rule in item c) says "- Every explicit semantic leading 
> clock of P1
> > or P2 is identical to c."  I think this match your intuition
> > 
> > 
> > >>In the formal part, vacuity, in the case of P1 or P2, it 
> seems to me
> > that
> > >>if P1 has vacuous success and P2 is non-vacuous failure, 
> it would be
> > >>declared as non-vacuous success. That looks strange. Or did I miss
> > >>something?
> > >>
> > [[DB:]] I think you are right, and this is bothering. 
> However, it is not
> > part of 1932. We tried to give a conservative definition (no false
> > negatives) and keep the definition indifferent to negation. 
> I think that
> > sometime in the future we will have to find a better definition.
> 
> This seems to be an inevitable consequence of decoupling "success"
> from "vacuity".  Our basic intuition has been that non-vacuity is
> oblivious to negation because of the rule
> 
>    w |=^{non} not p
> 
> iff 
> 
>    w |=^{non} p
> 
> I think that if we want
> 
>    (w |= p or q)  and  (w |=^{non} p or q)
> 
> to imply that 
> 
>    either
>       w |= p and w^{non} |= p 
>    or 
>       w |= q and w^{non} |= q
> 
> then we will need to recouple the concepts.  This seems to provide
> some chanllenges for negated formulas.
> 
> J.H.
>  
>    
> 
> -- 
> This message has been scanned for viruses and
> dangerous content by MailScanner, and is
> believed to be clean.
> 
> 

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