Hardware Reference
In-Depth Information
For temporal logic operators we may also use the research notation: G for
always
,
F for
s_eventually
, and X for
nexttime
.
All variables and expressions are 2-state, even if their type is explicitly specified
as
logic
. The values
x
and
z
are interpreted as 0.
All properties are clocked by the global clock.
21.1
Auxiliary Notions
In this section, we briefly describe logical and mathematical notions that will be
used later in this chapter. The reader familiar with them may skip this section.
21.1.1
Relations
The
Cartesian product
of two sets, A and B,isthesetA
B consisting of all ordered
pairs .a; b/ such that a
2
A and b
2
B.
Example 21.1.
If A
Df
x; y
g
, and B
Df
0; 1; 2
g
, then A
B
Df
.x; 0/, .x; 1/,
.x; 2/, .y; 0/, .y; 1/, .y; 2/
g
.
t
A Cartesian product of an arbitrary number of sets A
1
A
2
:::
A
n
is defined
as the set of all tuples .a
1
;:::;a
n
/, where a
1
2
A
1
;:::;a
n
2
A
n
.
A
binary relation
R between two sets A and B is any set of ordered pairs .a; b/
such that a
2
A and b
2
B. In other words, R is a binary relation iff R
A
B.
Example 21.2.
.
For example, .3; 5/
2
,but.6; 4/
…
. Of course, we are accustomed to writing
3
5 instead of .3; 5/
2
and 6
—
4 instead of .6; 4/
…
.
The order
of integer numbers
Z
is a binary relation:
ZZ
t
It is possible to define relations of an arbitrary arity: an n-ary relation R between
the sets A
1
;:::;A
n
is any set of tuples .a
1
;:::;a
n
/ such that a
1
2
A
1
;:::;a
n
2
A
n
.
In other words, R is an n-ary relation between A
1
;:::;A
n
iff R
A
1
A
n
.
21.1.2
Logic Notation and Quantifiers
Boolean Logic:
In logical formulas, we are using the following notation for
Boolean operators:
:
for negation (Boolean NOT),
^
for conjunction (Boolean
AND),
_
for disjunction (Boolean OR),
!
for implication, and
˚
for XOR.
Search WWH ::
Custom Search