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

 

I vote yes with the following contingencies:

 

1. Editorials in blue:  For example, consider the following assertion:

a1: assert property (@clk not a ##1 b);

Since the sequential property a ##1 b is used in an assertion, it is
weak. This means that if clk stops ticking ...

 

2. Two forms of followed-by are provided: Overlapped using operator #-#
and nonoverlapped using operator

#=#.  (The line spacing is weird here. It looks like there is an extra
return after operator)

 

3. initial explicit_always: assert property(always p);   The bold is
bsckwards (keywords area not bold and should be).  The previous examples
need to be fixed also.  Similarly, in subsequent examples, should
s_always and s_next should be bold too.

 

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? 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. 

 

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.

 

6. s_until and until_with, etc should be bold

 

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."            

 

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.

 

 

 

 

 

 

 

 

 

 

 

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