Re: [$ieee-1850] Third draft (Mar-8) of IEEE-1850 PSL LRM

ben,

>— (empty ; [*n]; seq), where n is greater than 0, is equivalent to
([*n-1]; seq)

no!  whatever the value of n, {empty ; [*n] ; seq} is equivalent to { [*n]
; seq ]

>— (seq; [*n]; empty), where n is greater than 0, is equivalent to (seq ;
[*n-1])

as above.  { seq ; [*n] ; empty } is equivalent to { seq ; [*n] } whatever
the value of n

in addition, i have no opinion about whether or not such clarifying
statements should be made.  however, if they are made, i have an opinion
about the wording:

>An empty sequence is one that does not match over any positive number of
clocks.

the term "match" is not defined for psl.  i would say "An empty sequence is
one that holds tightly only on an empty path."

>The
>following rules apply for concatenating sequences with empty sequences.

"for concatenating non-empty sequences with empty sequences"

>An empty
>sequence is denoted as empty and a sequence is denoted as seq.

"and a non-empty sequence is denoted as seq"

>— (empty : seq) does not result in a match

"does not hold tightly on any path"

>— (seq : empty) does not result in a match

"does not hold tightly on any path"

>— (empty ; [*n]; seq), where n is greater than 0, is equivalent to
([*n-1]; seq)

use correct info, as per my comment above.

>— (seq; [*n]; empty), where n is greater than 0, is equivalent to (seq ;
[*n-1])

use correct info, as per my comment above.

>For example,
>{b ; {a[*0] : c}}
>produces no match of the sequence.

"does not hold tightly on any path"

cindy.

--------------------------------------------------------------------
Cindy Eisner
Formal Methods Group
IBM Haifa Research Laboratory
Haifa 31905, Israel
Tel: +972-4-8296-266
Fax: +972-4-8296-114
e-mail:  eisner@il.ibm.com

ben cohen <hdlcohen@gmail.com>@eda.org on 03/08/2005 08:04:00 AM

Please respond to ben cohen <hdlcohen@gmail.com>

Sent by:    owner-ieee-1850@eda.org


To:    "Harry D.Foster" <harry@jasper-da.com>
cc:    ieee-1850@eda.org
Subject:    Re: [$ieee-1850] Third draft (Mar-8) of IEEE-1850 PSL LRM



Harry,
I am still going through the document.  However, attached is a one
page pdf file that has some initial feedback.
Ben

--------------------------------------------------------------------------
Ben Cohen Trainer, Consultant, Publisher (310) 721-4830
http://www.vhdlcohen.com/  ben_ f rom _abv-sva.org
* Co-Author: SystemVerilog Assertions Handbook, 2005 ISBN 0-9705394-7-9
* Co-Author: Using PSL/SUGAR for Formal and Dynamic Verification 2nd
Edition, 2004, ISBN 0-9705394-6-0
* Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn
0-9705394-2-8
* Component Design by Example ", 2001 isbn 0-9705394-0-1
* VHDL Coding Styles and Methodologies, 2nd Edition, 1999 isbn
0-7923-8474-1
* VHDL Answers to Frequently Asked Questions, 2nd Edition, isbn 0-7923-8115
---------------------------------------------------------------------------