Hardware Reference
In-Depth Information
We say that sequence s is tightly satisfied on word w , and write w j s,iff w
matches s. In Chaps. 6 and 11 , we have informally defined a match for each type of
sequence. Here, we provide the formal semantics of sequence match. As in the case
of properties, the formal semantics of sequences is defined recursively from the base
case of a Boolean sequence. We describe here only the formal semantics of the
basic sequence forms. The derived sequence forms have been defined as shortcuts
in Chaps. 6 and 11 .
In the context of sequence tight satisfaction, we assume that w is a finite word.
By ˙ , we understand the language consisting from all finite words over the
alphabet ˙ .
Boolean Sequence: The Boolean sequence e is tightly satisfied on w iff j w jD 1
and e is true on w :
w j e iff . j w jD 1/ and . w 0
ˆ e/:
Concatenation: The concatenation r ##1 s of the sequences r and s is tightly
satisfied on the word w iff it is possible to break w into two words x and y such
that r is tightly satisfied on x and s is tightly satisfied on y:
w j r ##1 s iff there exist x, y so that w D xy, and x j r and y j s:
Fusion: The fusion r ##0 s of the sequences r and s is tightly satisfied on the word
w iff it is possible to break w into three words x, y, and z , where the size of y is 1,
such that r is tightly satisfied on xy and s is tightly satisfied on y z :
w j r ##0 s iff there exist x, y, z so that w D xy z and j y jD 1, and xy j r and
y z j s.
Disjunction: The disjunction r or s of the sequences r and s is tightly satisfied on
the word w iff either sequence is tightly satisfied on w :
w j r or s iff . w j r/ or . w j s/.
Intersection:
The intersection r intersect s of the sequences r and s is tightly satisfied on
the word w iff both sequences are tightly satisfied on w :
w j r intersect s iff . w j r/ and . w j s/.
Empty Sequence: The empty sequence s [ * 0] is tightly satisfied on the word w iff
w is empty:
w j s [ * 0] iff j w jD 0.
Search WWH ::




Custom Search