Hardware Reference
In-Depth Information
C4
.
posedge
b/
D
$rising_gclk(
b
)
.
C5
.
negedge
b/
D
$falling_gclk(
b
)
.
C6
.
edge
b/
D
.
posedge
b/
||
.
negedge
b/.
C7
.e
iff
b/
D
.e/
&&
b.
C8
.e
1
or
e
2
/
D
.e
1
/
||
.e
2
/.
C9
.e
1
,
e
2
/
D
.e
1
/
||
.e
2
/.
For example,
.
posedge
clk
iff
enable
/
D
$rising_gclk(clk) && enable
After transforming clocking events into Boolean expressions, the formal seman-
tics eliminates the clocking event controls by folding the associated Boolean
expressions into the underlying sequences and properties. The resulting
unclocked
sequences and properties are then interpreted over traces (i.e., finite and infinite
words). The elimination of the clocking event controls is accomplished by a system
of
clock rewrite rules
. The rewrite rules define a function
s
that transforms a
sequence and the Boolean expression for a clock into an unclocked sequence. They
also define a function
T
p
for transforming properties similarly. The clock rewrite
rules are as follows, where c denotes a clocking event:
T
s
.
(
r
)
;c/
D
(
T
s
.r; c/
)
.
SCR0
T
s
.b; c/
D
!
c
[
*
] ##1
c
&&
b.
SCR1
T
s
.
(1,
v
=
h
)
;c/
D
T
s
.
1
;c/
##0 (1,
v
=
h
)
.
SCR2
T
s
.
@(
c
2
)
r; c
1
/
D
T
s
.r; c
2
/.
4
SCR3
T
s
.r
2
;c/, where
op
can be any of the
operators
##0
,
##1
,
or
, and
intersect
.
s
.r
1
s
.r
1
;c/
op
SCR4
T
op
r
2
;c/
D
T
T
s
.
first_match
(
r
)
;c/
D
first_match
(
T
s
.r; c/
)
.
SCR5
T
s
.r
[
*
n
]
;c/
D
T
s
.r; c/
[
*
n
]
. The same rule applies to ranged repetition
SCR6
T
operators.
p
.
(
p
)
;c/
D
(
T
p
.p; c/
)
.
PCR0
T
p
.
op
(
r
)
;c/
D
op
(
T
s
.r; c/
)
, where
op
is either
strong
or
weak
.
PCR1
T
p
.
@(
c
2
)
p; c
1
/
D
T
p
.p; c
2
/.
5
PCR2
T
p
.p; c/, where
op
is any of
not
,
disable iff
(
b
)
,
accept_on
(
b
)
, and
reject_on
(
b
)
.
p
.
op
p; c/
D
op
PCR3
T
T
p
.p
1
op
p
2
;c/
D
T
p
.p
1
;c/
op
p
.p
2
;c/, where
op
can be any of the
PCR4
T
T
operators
and
,
or
,
implies
, and
iff
.
p
.p; c/.An
analogous rule applies to rewrite the synchronous reject in terms of the
asynchronous reject.
p
.
sync_accept_on
(
b
)
p; c/
D
accept_on
(
b
&&
c
)
T
PCR5
T
4
This rule can be applied only after applying the clock flow rules in Sect.
12.2.4.1
.
5
See footnote
4
.
Search WWH ::
Custom Search