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

Hi Lisa, Manisha,

 

I think that a convincing argument for the consistency of weak LTL
operators in recursive properties is

that weak until can be implemented using recursive properties:

 

property r_until(p1,p2);

   p2 or (p1 and 1 |=> r_until(p1,p2));

endproperty

 

So everything that is expressed with recursive properties with until,
always, (weak ) eventually etc. 

can be easily translated to recursive properties without them

 

best regards

 

Doron

 

________________________________

From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On
Behalf Of Bustan, Doron
Sent: Tuesday, January 29, 2008 8:43 AM
To: Lisa Piper; john.havlicek@freescale.com; sv-ac@server.eda.org
Subject: RE: [sv-ac] call to vote on Mantis 1932

 

Hi Lisa,

 

Thanks for the review.

 

My comments are below. I will try to write something about the recursive
properties.

 

Doron

 

4. this is more of a question.  I have become confused on the meaning of
followed-by. Should I be thinking along the lines of attempts, or is
this a one time thing as though it is in an initial block?

[[DB:]] It should be attempt based, (unless the assertion is in initial
block)

 

 I understood the description and examples, but not the equivalency
expressions to |-> and |=>. I am having trouble following what happens
at a specific clock tick when the sequence on the LHS is false - does
that attempt pass or fail? There is something missing here. 

[[DB:]]  For a specific attempt, if there is no match of the sequence on
the LHS, then the property evaluates to false. Comparing to |->,|=> the
universal quantifier (for every match) is replaced with an existential
quantifier (exists a match).

 

5. shouldn't examples p2 to p5 in the description of always have the
##[range] instead of range?.

property p3;

s_always [2:5] a;

endproperty

 

should be 

 

property p3;

s_always ##[2:5] a;

endproperty

 

I think this:

 

s_always [constant_range] property_expr (ranged strong form of s_always)

 

should be:

 

s_always ##[constant_range] property_expr (ranged strong form of
s_always)

 

I think it will be very strange if always uses the ## and s_always does
not which is what the current syntax shows.  In any case the examples
here are inconsistent with the syntax. The same issue exists with
eventually.

 

[[DB:]] Non of them have the ##, the only difference is that s_always
shall not use unbounded range

 

 

7. didn't Dmitry's 1683 change this: the

"clock for the end of the antecedent must be the same as the clock for
the beginning of the consequent."            

 

[[DB:]] There is a note: "Note to the editor: if 1683 does not pass
then"

8. I would like to discuss whether recursive support is necessary at
this time.

 

9. I would to understand whether this is dependent on the proposal for
the VPI changes, or whether this could get accepted without the VPI
getting accepted.

[[DB:]] I do not want it to depend on the vpi proposal. Giving the time
constraints, I think we should priorities this, have the main proposal
in the 2008, and fix the vpi latter.

 

 

 

 

 

 

 

 

 

 

 

-----Original Message-----
From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of John
Havlicek
Sent: Tuesday, January 15, 2008 9:00 PM
To: sv-ac@eda.org
Subject: [sv-ac] call to vote on Mantis 1932

 

Hi Folks:

 

This is the call to vote on the proposal for Mantis 1932.  Note that

this ballot runs until 2008-01-28, but do not delay since we are

running out of time!

 

The documents on Mantis are

 

   LTL.1932.080115.pdf

   LTL_Formal.080115.pdf

 

Please vote if you are eligible.  See details below.

 

J.H.

 

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

Ballot on Mantis 1932

 

- Called on 2008-01-15, final ballots due by 2008-01-28 T 23:59-08:00.

 

 v[xxxxxxxxxxxxxxxxxxxxx-xxxxxxxxxxxxxxxxxxxxxxxx-xx] Doron Bustan
(Intel)

 v[xxxxx--xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx-x] Eduard Cerny
(Synopsys)     

 n[----------------------x-xxx---------x-x-xxx-x---x] Surrendra Dudani
(Synopsys)

 v[xxxxxxxx-xxxxxx-xxxxxxxxx-xx-xxxxx-xxx-xxx-------] Yaniv Fais
(Freescale)

 t[xxxx--xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx] John Havlicek
(Freescale - Chair)

 v[xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxrxxxxxxxxxxxxx-xxx] Dmitry Korchemny
(Intel - Co-Chair)

 v[xxxxx-xxxxxxxxx-xxx-x--xx--xxxxx----------xx-xxxx] Manisha
Kulshrestha (Mentor Graphics)

 n[------------------------------xxxxx-------x-xx-x-] Jiang Long (Mentor
Graphics)

 n[---------x------------x--xxx.....................] Joseph Lu (Altera)

 v[xxxxxxxxxxxxxxxxxxx..............................] Johan Martensson
(Jasper)

 n[---------------------------x--x-xx--xx-xxxxxxx-x-] Hillel Miller
(Freescale)

 v[xxxxx-xxxx-xxxxxxxxxxxxxxxxxxx-xxxxxxxx-xxxxxxxxx] Lisa Piper
(Cadence)

 v[xxxxxx-x-x-xx-xxxxxxx-x-xxxxx-x..................] Erik Seligman
(Intel)

 n[-------x-x----x--------xxxx-----xxxx-xx----------] Tej Singh (Mentor
Graphics)

 v[xxxxxx-x-xxxxxx--xxxxxxxx-xxxxxxxxxxxxxxxxxxxxxxx] Bassam Tabbara
(Synopsys)

 v[xxxxxxxxx-xxxxxxxxxxxxx-xxxxxxxxxx...............] Tom Thatcher (Sun
Microsystems)

   |------------------------------------------------- attendance on
2008-01-15

 |--------------------------------------------------- voting eligibility
for this ballot

|---------------------------------------------------- email ballots
received

 

        Legend:

                x = attended

                - = missed

                r = represented

                . = not yet a member

                v = valid voter (2 out of last 3 or 3/4 overall)

                n = not a valid voter

                t = chair eligible to vote only to make or break a tie

 

 

   

 

-- 

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 <http://www.mailscanner.info/> , and is

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

believed to be clean. 
---------------------------------------------------------------------
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.