Michael:
In the absence of local variables, the unclocked semantics of SVA sequence
operators is similar to standard definitions for regular expression. The
semantics of a sequence can be defined by specifying the language of finite
words that tightly satisfy the sequence.
Denote the language of sequence R by L(R). For any sequence R,
L(R[*0]) = {\emptyword}. The languages denoted by other basic operators
are
L((R ##1 S)) = {xy : x \in L(R) and y \in L(S)}
L((R ##0 S)) = {xyz : |y| = 1 and xy \in L(R) and yz \in L(S)}
L((R or S)) = L(R) \union L(S)
L((R intersect S)) = L(R) \intersect L(S)
L(R[*1:$]) = {x_1...x_j : j >= 1 and x_i \in L(R) for all 1 <= i <= j}
> A) (R1 [*0]) or R2 //Or vice versa
L((R1[*0]) or R2) = {\emptyword} \union L(R2)
> B) (R1 [*0]) intersect R2 //I really don't understand this case
L((R1[*0]) intersect R2) = {\emptyword} \intersect L(R2)
> C) R1 intersect (R2 [*0])
L(R1 intersect (R2 [*0])) = L(R1) \intersect {\emptyword}
> D) (R1 [*0]) [*1:$]
L((R1[*0]) [*1:$]) = {\emptyword}
> E) (R1 [*0] ##0 R2) ##1 R3
L((R1 [*0] ##0 R2) ##1 R3) = {}
This is because ##0 concatenation requires a non-empty match
of both operands, while R1[*0] is tightly satisfied only by
\emptyword.
> F) first_match(R1 [*0])
L(first_match(R1 [*0])) = {\emptyword}
Note that
L((R[*0] ##1 S)) = L(S) = L((S ##1 R[*0]))
From this, you can derive the identities
> (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
where "R === S" is understood to mean "L(R) = L(S)".
> R1 ##0 (R2 [*0]) === ???
L((R1 ##0 (R2 [*0]))) = {}
> (R1 [*0]) ##0 R2 === ???
L(((R1 [*0]) ##0 R2)) = {}
> ((R1 [*0]) or R2) ##1 R3 === R3 or R2
(R1 [*0]) or R2) ##1 R3 === R3 or (R2 ##1 R3)
The following look correct to me:
> first_match(R1 [*0]) === R1 [*0]
> (R1 [*0]) [*1:$] === R1 [*0]
A number of algebraic identities are given in the Accellera Technical Report
2004.01 (http://www.accellera.org/techrep.pdf), although the focus of that report
is the semantics of local variables. The case of no local variables is subsumed
by the case with local variables.
Best regards,
John H.
> 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 Mon, 16 Aug 2004 16:44:34 -0500 (CDT)
This archive was generated by hypermail 2.1.8 : Mon Aug 16 2004 - 14:44:55 PDT