[sv-ac] FW: BOUNCE vfv@eda.org: Non-member submission from [Gal Vardi <vardi@il.marvell.com>]

Subject: [sv-ac] FW: BOUNCE vfv@eda.org: Non-member submission from [Gal Vardi ]
From: Erich Marschner (erichm@cadence.com)
Date: Thu Feb 20 2003 - 07:35:13 PST

Next message: Stephen Meier: "[sv-ac] cover requirements"
Previous message: Faisal Haque: "[sv-ac] Agenda for today's meeting"
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]

The following comments on the SVA LRM were received from Gal Vardi of Galileo. Reposting to sv-ac and vfv because they bounced the first time.

| From owner-vfv Mon Feb 17 00:42:01 2003
| Received: from galileo5.galileo.co.il (pop3.galileo.co.il
| [199.203.130.130])
| by server.eda.org (8.12.0.Beta7/8.12.0.Beta7) with
| ESMTP id h1H8fven002386
| for <vfv@eda.org>; Mon, 17 Feb 2003 00:42:00 -0800 (PST)
| Received: from il.marvell.com (galileo170.galileo.co.il
| [10.2.10.170])
| by galileo5.galileo.co.il (8.12.6/8.12.6) with ESMTP id
| h1H8f7J5021696;
| Mon, 17 Feb 2003 10:41:08 +0200 (GMT-2)
| Message-ID: <3E50A022.3000308@il.marvell.com>
| Date: Mon, 17 Feb 2003 10:41:06 +0200
| From: Gal Vardi <vardi@il.marvell.com>
| User-Agent: Mozilla/5.0 (X11; U; SunOS sun4u; en-US; rv:1.0.1)
| Gecko/20020920 Netscape/7.0
| X-Accept-Language: en-us, en
| MIME-Version: 1.0
| To: Accellera VFV <vfv@server.eda.org>,
| "Faisal Haque (Accellera SV-AC)"
| <fhaque@cisco.com>
| CC: vardi@il.marvell.com
| Subject: Accelera SVA - comments for review LRM 0.8
| Content-Type: multipart/alternative;
| boundary="------------090606010304030706040009"
|
|
| --------------090606010304030706040009
| Content-Type: text/plain; charset=us-ascii; format=flowed
| Content-Transfer-Encoding: 7bit
|
|
|
| Hi -
| These are my comments regarding SVA proposal Rev0.8
|
| Some inaccuracies, some explanations or clarifications needed, and some
| wishful thoughts that the asserions will fit what I know and what I am
| used to.
| Iam aware it is just my guts feeling of what is clearer and easier to
| understand/use, but you read and judge.
|
| p.42 11.2 - check(cond)block; else block; - can you explain why not
| using good old if-then-else construct , or some switch/case ?
| p.42 11.2 - should specify the truth values of the
| expressions : (x==0), (z==0) , (x==z) etc.
| (I think it is evaluated to true in verilog HDL, but I feel that in
| a verification language they are logically different values and should
| be false. verilog standard uses "===" comparison to force
| the false value.)
|
| p.45 11.4 , 10th line in paragraph : "The concatenation specifies a
| delay between ....."
| This is inaccurate, since a concatenation before a zero length
| sequence does force a delay.
| ( a ; b ; c ; [0 .. 3] d ) - here c & d may occur on the same cycle.
| p.45 11.4 , last paragraph in this page : "The first element in a
| sequence is checked at the first occurrence of the clock or at or after
| the event that triggered evaluation of the sequence"
| Besides the redundant "at" word , this is not true - it is checked at
| the event (within the same clock tick) and not after it.
| p.26 11.4 "Note that the following two are not equivalent.." - This
| syntax is quite confusing for me, just give a second thought about the
| semantics. If you are familiar with this - go with it.
| p.48, 11.6.1 - some mixture (possibly typo or tricky MS word
| processors
| ;) of "=*" and "*=".
| please fix all to the correct syntax.
| p.49 11.6.2 - you can add to fell/rose/stable the functions $prev and
| $changed. We find it very useful.
|
| p.50 1.6.3 - AND operation on a multiple-occurance sequence
| is not welldefined.
| A multiple-occurance-sequence , e.g. (*) ((stop=0)*[1:inf]) is a
| sequence of any positive length where the signal stop is not
| active all along.
| the AND sequence :
| (**) (first_data ; busy*[1..inf] ; end_data) and
| ((stop=0)*[1:inf])
| may be interpreted as "a whole transmission of first_data to
| last_data without any occurrence of "stop" in between.
| So on this 12-cycles long trace : first_data & stop ; busy [10] ;
| end_data the above sequence will not "succeed".
| but from the informal definition "waiting for the other sequence to
| succeed ..." I want to conclude the opposite :
| ((stop=0)*[1:inf]) is a sequence which succeeds after 1
| clock-tick of inactive "stop".
| So this sequence is "waiting" for the other to succeed,
| and the result is that the above mentioned sequence (**)
| succeeds !!!
| What is the exact interpretation of the semantics in this case ?
|
| p.55 , 11.6.6 - first match is not well-defined :
| a. where is the ending point of the operator first_match : do you
| take the first cycle of the matching sequence or the last ?
| b. using first_match on OR'ed sequences : (seqA || seqB) - do you
| take the first sequence to start, or the first one to end/succeed ?
| example : ( a ; b ; first_match ( (c;d;e;f) || (d;e)) ) ; [0]z
| Where should z occur ? with 'c' , with 'f' , with 'd' or with 'e' ?
|
| p.56, 11.6.7 - Here is a major point for SVA+PSL
| coordination : syntax of => and -> should be unified and similar !
| p.58 , 11.6.7 - the paragraph explaining below Figure 11-12.
| The last sentence of the paragraph (claiming "That also means that
| there is no match at 5.6 and 7) seems to conflict with previous
| statements. As I understand, the mentions sequence (in page 57, last
| line) does succeed on cycle 5 and 6.
| p.58 11.6.8 - last line in page, "If no sequence succeeds ... true
| sequence of length one".
| My "feeling" is that the returned sequence should be of length zero
| (= equal to a plain single concatenation - ;).
| I must admit I don't have any realization of where it is used and
| when it is useful.
| p.59 , 11.6.9 - throughout ... within -
| I don't see why do you need two operators to reflect a single
| relation between two operands.
| my (small) experience with parsing and split/combined keywords
| carries some frustration from our well known CTL-until
| operator :
| A(x U y).
| p.60 , 11.6.10 - last line, "The start point ... must be between ..."
| add an explicit explanation that "between" is inclusive ,
| containing the endpoints.
|
| p. 63 , 11.9 - $past ? what about $prev ?
| - $countones - good ! should add $countzeroes too !
| (remember they are not necessarily complementing, the bus might contain X's too !)
|
|
| I wish you success and good luck with the rest of (fight over :) our work,
|
|
| regards,
| Gal.
|
|
|
|
|
|
|
|
|
|
|
|
| --
| \\\|/// ))))|((((
| \\ ~ ~ // / ^ _ \
| ( @ @ ) ( (o) (o) )
| *=oOOo=(_)=oOOo===oOOO====(_)====OOOOo==*
| | Gal Vardi |
| | Formal Verification |
| | Marvell Semiconductor Israel Ltd |
| | tel: (+972) 04-9999555 ext. 1274 |
| | gal.vardi@il.marvell.com |
| *====================Oooo.==============*
| .oooO ( )
| ( ) ) /
| \ ( (_/
| \_)
|
| This message may contain confidential, proprietary or
| legally privileged
| information. The information is intended only for the use of
| the individual
| or entity named above. If the reader of this message is not the
| intended recipient, you are hereby notified that any dissemination,
| distribution or copying of this communication is strictly
| prohibited. If you
| have received this communication in error, please notify us
| immediately by
| telephone, or by e-mail and delete the message from your computer.
|
|
| --------------090606010304030706040009
| Content-Type: text/html; charset=us-ascii
| Content-Transfer-Encoding: 7bit
|
| <!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
| <html>
| <head>
| <title></title>
| </head>
| <body>
| 
| 
| Hi - 
| These are my comments regarding SVA proposal Rev0.8 
| 
| Some inaccuracies, some explanations or clarifications
| needed, and some
| wishful
| thoughts that the asserions will fit what I know and what I
| am used to. 
| Iam aware it is just my guts feeling of what is clearer and easier to
| understand/use,
| but you read and judge. 
| 
| p.42 11.2 - check(cond)block; else block; -  can
| you explain why
| not
| using good old if-then-else construct , or some switch/case ? 
| p.42 11.2 - should specify the truth values of the
| expressions : (x==0) ,
| (z==0) , (x==z) etc. 
|     (I think it is evaluated to
| true in verilog
| HDL, but I
| feel that in a verification language they are logically
| different values
| and should be false. verilog standard uses
| "===" comparison
| to force the false value.) 
| 
| p.45 11.4 , 10th line in paragraph : "The concatenation
| specifies a delay
| between ....." 
|     This is inaccurate, since a concatenation
| before a zero
| length sequence
| does force a delay. 
|     ( a ; b ;  c ; [0 .. 3] d ) - here c
| & d may
| occur on the same cycle. 
| p.45 11.4 , last paragraph in this page : "The first element in a
| sequence
| is checked at the first occurrence of the
| clock or at or after
|  the event that
| triggered
| evaluation of the sequence" 
| Besides the redundant "at" word , this is not true - it is
| checked at
| the event (within the same clock tick) and not
| after it. 
| p.26 11.4 "Note that the following two are not
| equivalent.." - This
| syntax is quite confusing for me, just give a second thought
| about the
| semantics.
| If you are familiar with this - go with it. 
| p.48, 11.6.1 - some mixture (possibly typo or tricky MS word
| processors ;)
| of "=*" and "*=". 
|     please fix all to the correct syntax. 
| p.49 11.6.2 - you can add to fell/rose/stable the functions
| $prev
| and  $changed. We find it very useful. 
| 
| p.50 1.6.3 - AND operation on a multiple-occurance sequence
| is not well
| defined. 
|     A multiple-occurance-sequence , e.g. (*)
| ((stop=0)*[1:inf]) is
| a sequence of any positive length where the signal
| stop is not active
| all along. 
|     the AND sequence  : 
| (**)            
|  (first_data ; busy*[1..inf] ; end_data) and
| ((stop=0)*[1:inf]) 
|     may be interpreted as "a whole transmission of
| first_data to last_data
| without any occurrence of "stop" in between. 
|     So on this 12-cycles long trace :
| first_data &
| stop ; busy [10]
| ; end_data the above sequence will not "succeed". 
| but from the informal definition "waiting for the other
| sequence to succeed
| ..." I want to conclude the opposite : 
|         
| ((stop=0)*[1:inf]) is a
| sequence which succeeds after
| 1 clock-tick of inactive "stop". 
|     So this sequence is "waiting" for the other to
| succeed, 
|     and the result is that the above
| mentioned sequence
| (**)  succeeds !!! 
| What is the exact interpretation of the semantics  in
| this case ? 
| 
| p.55 , 11.6.6 - first match is not well-defined : 
|     a. where is the ending point of the operator
| first_match : do
| you take the first cycle of the matching sequence or the last ? 
|     b. using first_match on OR'ed sequences : (seqA ||
| seqB) - do you take
| the first sequence to start, or the first one to end/succeed ? 
|         example : ( a ; b ;
| first_match (
| (c;d;e;f) || (d;e)) ) ;
| [0]z 
|     Where should z occur ? with 'c' , with
| 'f' , with 'd' or
| with 'e' ? 
| 
| p.56, 11.6.7 - Here is a major point for SVA+PSL
| coordination : syntax of
| => and -> should be unified and similar ! 
| p.58 , 11.6.7 - the paragraph explaining below Figure 11-12. 
|     The last sentence of the paragraph
| (claiming "That also
| means that there
| is no match at 5.6 and 7) seems to conflict with previous
| statements. As
| I understand, the mentions sequence (in page 57, last line) does
| succeed
| on cycle 5 and 6. 
| p.58 11.6.8 - last line in page, "If no sequence succeeds ... true
| sequence
| of length one". 
|     My "feeling" is that the returned
| sequence should be of
| length zero
| (= equal  to a plain single concatenation - ;). 
|     I must admit I don't have any realization
| of where it is
| used and when
| it is useful. 
| p.59 , 11.6.9 - throughout ... within  - 
|     I don't see why do you need two
| operators to
| reflect a single
| relation between two operands. 
|         my (small) experience
| with parsing and
| split/combined  keywords carries
| some frustration     from our well known CTL-until
|  operator : A(x U y). 
| p.60 , 11.6.10 - last line, "The start point ... must be
| between ..." 
|         add an explicit
| explanation that
| "between" is inclusive ,
| containing the endpoints. 
| 
| p. 63 , 11.9 - $past ? what about $prev ? 
|            
|    
|     - $countones - good ! should add
| $countzeroes
| too ! 
|            
|    
|     (remember they are not necessarily
| complementing, the
| bus might contain X's too !) 
| 
|   
| I wish you success and good luck with the rest
| of (fight over :) our
| work,
| 
| 
| 
| regards, 
| Gal. 
| 
|     
| 
| 
|     
| 
| 
| 
| 
| 
| 
| 
| <pre class="moz-signature" cols="$mailwrapcol">--
| \\\|/// ))))|((((
| \\ ~ ~ // / ^ _ \
| ( @ @ ) ( (o) (o) )
| *=oOOo=(_)=oOOo===oOOO====(_)====OOOOo==*
| | Gal Vardi |
| | Formal Verification |
| | Marvell Semiconductor Israel Ltd |
| | tel: (+972) 04-9999555 ext. 1274 |
| | <a class="moz-txt-link-abbreviated"
| href="mailto:gal.vardi@il.marvell.com">gal.vardi@il.marvell.com</a>
| |
| *====================Oooo.==============*
| .oooO ( )
| ( ) ) /
| \ ( (_/
| \_)
|
| This message may contain confidential, proprietary or
| legally privileged
| information. The information is intended only for the use of
| the individual
| or entity named above. If the reader of this message is not the
| intended recipient, you are hereby notified that any dissemination,
| distribution or copying of this communication is strictly
| prohibited. If you
| have received this communication in error, please notify us
| immediately by
| telephone, or by e-mail and delete the message from your computer.
| </pre>
| </body>
| </html>
|
| --------------090606010304030706040009--
|
|

Next message: Stephen Meier: "[sv-ac] cover requirements"
Previous message: Faisal Haque: "[sv-ac] Agenda for today's meeting"
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]

This archive was generated by hypermail 2b28 : Thu Feb 20 2003 - 07:37:57 PST