Hardware Reference
In-Depth Information
D
(
(!
c
[
*
] ##1
c
&& 1)[
*
]
##1
s
.r
1
;c/
##1 (!
c
[
*
] ##1
c
&& 1)[
*
]
T
)
T
s
.r
2
;c/
[
SCR1
]
intersect
((
c
[->1])[
*
] ##1
T
s
.r
1
;c/
##1 (
c
[->1])[
*
])
T
s
.r
2
;c/
intersect
t
Example 22.16.
Calculate a clock rewrite rule for
always
p.
Solution:
always
p is defined to be equivalent to p
until
1'b0
. Boolean
operands of a weak operator like
until
are automatically weakened, as though
they were within implicit instances of
weak
. Therefore
T
p
.
always
p; c/
D
T
p
.p
until
1'b0
;c/
D
(
c
implies
T
p
.p; c/
)
until
(
c
and
T
s
.
1'b0
;c/
)
[
PCR8
]
p
.p; c/
)
until
(
c
and
(!
c
[
*
] ##1
c
&& 1'b0))
D
(
c
implies
T
[
SCR1
]
p
.p; c/
)
until
(
c
&& 1'b0)
(
c
implies
T
p
.p; c/
)
until
1'b0
(
c
implies
T
t
p
.
;c/:
Example 22.17.
Show that the following equivalence is preserved under
T
r
#-#
p
not
(
r
|->
not
p
)
(*)
Solution:
Compute:
p
.
not
(
r
|->
not
p
)
;c/
D
not
(
T
T
p
.r
|->
not
p; c/
)
[
PCR3
]
s
.r; c/
|->
T
p
.
not
p; c/
)
D
not
(
T
[
PCR6
]
s
.r; c/
|->
not
T
p
.p; c/
)
D
not
(
T
[
PCR3
]
s
.r; c/
#-#
T
p
.p; c/
T
[.
/]
p
.r
#-#
p; c/
D
T
[
PCR6
]
t
It is important to understand that the clock rewrite rules do not account for
scoping of clocks as defined by the clock flow rules. The addition of clocking event
controls consistent with the clock flow rules may be necessary before the clock
rewrite rules may be applied.
Example 22.18.
Assume that c is the incoming clock to x
##1 @(
d
)
y
|=>
z
.
Show that application of
p
.
;c/to this property does not correctly account for
clock flow. Add clocking event controls to the property so that application of
T
T
p
.
;c/yields the correct rewrite.
Search WWH ::
Custom Search