[sv-ac] [Fwd: "Null repition" semantics]

Dear all,

I am forwarding this message from my colleague Michael Pellauer,
who has encountered some issues with the assertions spec in the
SV 3.1a LRM.

Nikhil

-------- Original Message --------
Subject: "Null repition" semantics
Date: Tue, 10 Aug 2004 17:08:39 -0400
From: Michael Pellauer <mpellauer@bluespec.com>
To: Rishiyur S. Nikhil <nikhil@bluespec.com>

Hello all,

I've been working with the semantics of System Verilog Assertions for
Bluespec's implementations, and I have some questions. Perhaps these
issues have already been raised on your errata list - if so I'm sorry to
take your time.

My questions generally pertain to the "null repitition" form of the
abstract grammar of unclocked sequences (as defined in Appendix H.2.1), IE:

R [*0]
(where R is an unclocked sequence)

While I believe that the semantics of null reptition are clear enough in
isolation (as defined in H.3.2) I'm not quite clear on how it is
supposed to interact with the other core operators.

There's a good description of some of the intended behavior in Section
17.2.2 (page 210), however this natural language description does not
seem to have made it into the formal semantics, or the derived operators
of Section H.2.3. Perhaps there is some reason that they are superfluous
that I am missing.

Specifically, what are the intended behaviors of the following sequences:

A) (R1 [*0]) or R2 //Or vice versa
B) (R1 [*0]) intersect R2 //I really don't understand this case
C) R1 intersect (R2 [*0])
D) (R1 [*0]) [*1:$]
E) (R1 [*0] ##0 R2) ##1 R3
F) first_match(R1 [*0])

Additionally, I suggest that something based on the natural language in
17.7.2 be added to the derived operators section H.2.3. It will
probably be something like the following, but please check that I
haven't made any slip-ups:

(R1 [*0]) ##n R2 === ##(n-1) R2 for n > 1
(R1 [*0]) ##1 R2 === R2
R1 ##n (R2 [*0]) === R2 ##(n-1) 1 for n > 1
R1 ##1 (R2 [*0]) === R1
R1 ##0 (R2 [*0]) === ???
(R1 [*0]) ##0 R2 === ???

Also the following derivations intuitively seem to be correct:

((R1 [*0]) or R2) ##1 R3 === R3 or R2
first_match(R1 [*0]) === R1 [*0]
(R1 [*0]) [*1:$] === R1 [*0]

I have gone ahead with my implementation by estimating the behavior I
think is correct for all of the above cases. However, I would really
appreciate some insight in how the language designers intended null
repitition to interact with the other "elemental" operators.
Particularly troubling to me is case (B) above.

I appreciate any contributions you can offer,

Michael
Received on Tue Aug 10 14:42:45 2004