Hardware Reference
In-Depth Information
1
bit
active[tagType];
2
always
@(
posedge
clk)
3
if
($sampled(start))
begin
a_no_tag_reuse:
assert final
(
4
!active.exists($sampled(tagIn))
5
);
6
active[$sampled(tagIn)] <= 1'b1;
7
end
8
else if
($sampled(complete))
begin
9
a_comp_tag_ok:
assert final
(
10
active.exists($sampled(tagOut))
11
);
12
active.delete($sampled(tagOut));
13
end
14
Fig. 15.10
Encoding of tag protocol control check
A tag value becomes active the cycle after an occurrence of
start
at which
tagIn
held that value.
A tag value becomes inactive the cycle after an occurrence of
complete
at
which
tagOut
held that value.
4.
start
may be high if and only if
complete
is not high and the value of
tagIn
is
inactive in that cycle.
5.
complete
maybehighifandonlyif
start
is not high and the value of
tagOut
is active in that cycle.
6. An occurrence of
start
corresponds to an occurrence of
complete
if and only
if the following conditions are all satisfied:
The occurrence of
start
is strictly before the occurrence of
complete
.
Thevalueof
tagIn
at the occurrence of
start
equals the value of
tagOut
at
the occurrence of
complete
.
There is no earlier occurrence of
complete
satisfying both of the two
preceding conditions.
7. If an occurrence of
start
corresponds to an occurrence of
complete
, then the
value of
dataIn
at that occurrence of
start
equals the value of
dataOut
at that
occurrence of
complete
.
The control part of the tag protocol specification is more complicated than in
our previous examples. As for the FIFO protocol, auxiliary variables can help in
encoding the control part of the specification. In the tag protocol, we need to keep
track of which tags are active. An associative array of bits can be used to do this
as shown in Fig.
15.10
. This encoding uses final assertions to perform the control
checks specified in Rules
4
and
5
. Note that the value associated to a tag in the
associative array
active
is not important, only whether or not the tag exists in the
array.
Search WWH ::
Custom Search