Hardware Reference
In-Depth Information
Solution:
By
CF3
,
CF7
, and
CF8
, d governs y and
z
, while the incoming clock c
governs x. Compute
p
.x
##1 @(
d
)
y
|=>
z
;c/
D
T
T
s
.x
##1 @(
d
)
y; c/
|=>
T
p
.
z
;c/
[
PCR6
]
s
.x; c/
##1
T
s
.
@(
d
)
y; c/
|=>
T
p
.
z
;c/
D
T
[
SCR4
]
s
.x; c/
##1
T
s
.y; d /
|=>
T
p
.
z
;c/
D
T
[
SCR3
]
Thus, according to the rewrite, d governs only y, while c governs x and
z
.Tofix
the problem, add the clocking event control
@(
d
)
after
|=>
:
T
p
.x
##1 @(
d
)
y
|=> @(
d
)
z
;c/
D
T
s
.x
##1 @(
d
)
y; c/
|=>
T
p
.
@(
d
)
z
;c/
[
PCR6
]
s
.x; c/
##1
T
s
.
@(
d
)
y; c/
|=>
T
p
.
@(
d
)
z
;c/
D
T
[
SCR4
]
s
.x; c/
##1
T
s
.y; d /
|=>
T
p
.
z
;d/
D
T
[
SCR3
,
PCR2
]
t
22.5
Formal Semantics of Resets
The special letters
>
and
?
play an important role in the formal semantics of
resets. If a reset condition occurs at some point in a trace
w
, then the disposition
of the evaluation depends on replacement of the suffix of
w
beginning at that point
by
>
!
, or both, depending on the particular reset. The intuition is that all
properties hold on
>
!
,
?
!
, while no properties hold on
?
!
.
7
Therefore, replacing a
!
suffix of
w
by
>
precludes failure after the point of replacement, while replacing
!
forces success to be complete prior to the point of replacement.
Abort operators of the “accept” kind replace the suffix beginning at the occurrence
of the abort condition by
>
the suffix by
?
!
, whereas abort operators of the “reject” kind replace
!
.For
disable iff
, the disposition on occurrence of the disable
condition is neither “pass” nor “fail”, but “disabled”, so the formal semantics uses
both replacements: the replacement of the suffix by
>
the suffix by
?
!
confirms that failure did
not occur before the disable condition, whereas the replacement of the suffix by
?
!
confirms that success also did not occur before the disable condition.
7
There are some theoretical subtleties involved. It is possible to write a sequence that does not
match any word, even when interpreted over the alphabet extended with
>
and
?
. An example is a
sequence involving a length mismatch, such as r
D
1'b1
intersect
(1'b1 ##1 1'b1)
.
From r , one can create a property, such as
weak
(
r
)
, that is not satisfiable, even by the word
>
!
.
However, by restricting each maximal sequence appearing in a concurrent assertion to be
non-
degenerate
, i.e., to match at least one nonempty finite word when interpreted over the extended
alphabet, this problem is avoided. The SystemVerilog LRM requires maximal sequences to be
nondegenerate in the appropriate circumstances to avoid such problematic cases.
Search WWH ::
Custom Search