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