Hardware Reference
In-Depth Information
p
.r
op
p; c/
D
T
s
.r; c/
op
p
.p; c/, where
op
is any of
|->
,
|=>
,
#-#
,
PCR6
T
T
and
#=#
.
6
p
.
nexttime
p; c/
D
!
c
until
(
c
and nexttime
(!
c
until
(
c
and
T
PCR7
T
p
.p; c/
)))
.
p
.p
1
until
p
2
;c/
D
(
c
implies
T
PCR8
T
p
.p
1
;c/
)
until
(
c
and
T
p
.p
2
;c/
)
.
Rule
PCR7
is the most complicated. It contains two alignments to c, performed
by the idiomatic subproperty
!
c
until
c. The first brings evaluation to alignment
with a tick of c, and the second performs the advance to the next tick of c,as
specified by
nexttime
(see Sect.
12.2.5.1
). The first alignment is needed to get the
proper semantics when the clock is changing. If evaluation of
nexttime
p begins
in a tick of c, then the first alignment does not advance time.
The clock rewrite rules above cover all the primitive operators and a number
of derived operators. For other derived operators, rewrite rules are obtained by
applying the rules above to the definition of the derived operator in terms of more
primitive operators.
Example 22.14.
Calculate a clock rewrite rule for b
[->1]
.
Solution:
b
[->1]
is defined to be equivalent to
!
b
[
*
] ##1
b. Therefore,
T
s
.b
[->1]
;c/
D
T
s
.
!
b
[
*
] ##1
b; c/
s
.
!
b
[
*
]
;c/
##1
T
s
.b; c/
D
T
[
SCR4
]
s
.
!
b; c/
[
*
] ##1
T
s
.b; c/
D
T
[
SCR6
]
D
(!
c
[
*
] ##1
c
&& !
b
)[
*
] ##1 !
c
[
*
] ##1
c
&&
b
[
SCR1
]
t
Example 22.15.
Calculate a clock rewrite rule for r
1
within
r
2
.
Solution:
r
1
within
r
2
is defined to be equivalent to
(1[
*
] ##1
r
1
##1 1[
*
])
intersect
r
2
Therefore,
s
.r
1
within
r
2
;c/
D
T
T
s
.
(1[
*
] ##1
r
1
##1 1[
*
])
intersect
r
2
;c/
s
.
(1[
*
] ##1
r
1
##1 1[
*
])
;c/
intersect
T
s
.r
2
;c/
D
T
[
SCR4
]
s
.
1[
*
] ##1
r
1
##1 1[
*
]
;c/
)
intersect
T
s
.r
2
;c/
D
(
T
[
SCR0
]
s
.
1[
*
]
;c/
##1
T
s
.r
1
;c/
##1
T
s
.
1[
*
]
;c/
)
D
(
T
s
.r
2
;c/
intersect
T
[
SCR4
]
s
.
1
;c/
[
*
] ##1
T
s
.r
1
;c/
##1
T
s
.
1
;c/
[
*
])
D
(
T
s
.r
2
;c/
intersect
T
[
SCR6
]
6
See footnote
4
.
Search WWH ::
Custom Search