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

Hi Doron,
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.)

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?

Thanks,

Ed

Sent from BlackBerry.


----- Original Message -----
From: Bustan, Doron <doron.bustan@intel.com>
To: Eduard Cerny <Eduard.Cerny@synopsys.COM>; john.havlicek@freescale.com <john.havlicek@freescale.com>; sv-ac@eda.org <sv-ac@eda.org>
Sent: Mon Jan 28 00:36:25 2008
Subject: RE: [sv-ac] Comment regarding LTL - Mantis 1932

Hi Ed,

 

Thanks for the review

 

I implemented most of your comments. I do have some notes below

 

Doron

 


pp7, 16.122.1: "Since only one match of a sequence_expr is needed ..." Also I am not sure why this and the next paragraph is needed.

 

[[DB:]] I fixed the typo, I think these paragraphs add intuition, so I left them in.

 

 

pp10, 16.122.10: the text explaining the Examples is correct only if the properties are in a verif. statement that is in an initial procedure. That should be mentioned.

 

[[DB:]] I think that the correction for the next item should be enough

pp11, Examples: The comments should start with "property succeeds if ...", otherwise it is not clear what is being described. 

 

[[DB:]] I add “The comments in the following examples describe the conditions for the properties to be evaluated to true.“ before the examples

 

 

pp13, Examples: the description is only correct if these properties are in verif. statements in initial procedures. Bottom of description paragraph, always should not be bold, because it is a generic term there.

 

[[DB:]] I add some text that say that the conditions described are for the property to be evaluated to true

 

 

pp23, b): 

 Every explicit semantic leading clock of q1 [ else q2 ] is identical to c.

 

is legal, but

@(c) if (b) @(c) (p1 else @(c2) p2)

 

[[DB:]] I think that the current text is fine. The first sentence sait that both operands should be clocked with the leading clock

The seconf is illegal because the second operand of the “and” is clocked on a different clock.

 

pp23: If p1 until p2 is the max. property of an assertion, it is not clear whether the leading clock of p1 can be different of the clock of p2. I'd say that the clocks shall be the same, but I could not see it from the text.

 

[[DB:]] I am not sure what you mean. Why is it important whether this is a top level property?

------------------------

 

 

 


-- 
This message has been scanned for viruses and 
dangerous content by MailScanner <http://www.mailscanner.info/> , and is 
believed to be clean. 

-- This message has been scanned for viruses anddangerous content by MailScanner, and isbelieved to be clean.