Hardware Reference
In-Depth Information
Let-declaration
legal_txa
on Line
9
is aimed to check the validity of the packet
type, as specified by Rule
TX1
.
Lines
11
-
15
contain free variable declarations. Free bit
valid
(Line
11
) indicates
when the transmitted data bit is valid. Free bit
data
is a data bit—the result of the
serialization. Both these free variables are directly copied to the checker outputs
(Lines
17
-
18
). The necessity of this copy is explained in Example
23.31
.
Free bit
packet_start
(Line
13
) indicates the beginning of a packet trans-
mission: either a transmission of a new packet or a retransmission of a recently
transmitted one. Free bit
new_packet
(Line
14
) indicates the beginning of a new
packet transmission. Finally, free variable
packet
corresponds to packet contents
(Rule
TX2
). The described free variables are constrained by the assumptions shown
in Fig.
23.5
. Let us now move to that figure.
Assumptions
m_rst_vs_packet_start
and
m_rst_vs_valid
restrict the gene-
rator behavior during the reset (Rule
TX5
). Assumption
m_rst_vs_packet_start
(Line
3
) forbids a new transmission when the reset is active. Assumption
m_rst_vs_valid
(Line
5
) enforces
valid
bit deassertion during the reset.
Both assumptions have an explicitly specified disable condition to override the
default. Note the problem with the inconsistent sampling of a reset condition. In
disable iff
clauses
rst
is not sampled, whereas in these two assumptions it is,
because it is part of their body. The same problem exists for the assignment on
Line
18
which implicitly uses the sampled value of
rst
(Line
12
). It remains to
hope that the value of
rst
does not change at the same time steps when the clock
does.
17
Assumption
m_non_overlap_start
(Line
7
) follows Rule
TX4
: No new trans-
action is allowed until the completion of the current one. The transaction length
LENGTH
is defined on Line
1
.
Line
10
declares
ptr
, a pointer to a currently transmitted packet bit. This variable
occupies the number of bits necessary for referencing any bit in a packet, the bit
numeration starting from 0 (Line
2
). The pointer is updated at each clock tick
(Line
18
); the next value of the pointer is calculated by function
next_tx_ptr
(Lines
11
-
17
). Each time the reset is active the processing starts anew, and the
pointer is set to 0 (Line
12
;Rule
TX5
). When
packet_start
is active, i.e., when
the transmission of a new packet or the retransmission of a transmitted one begins,
the pointer value is set to 1 (Line
13
; see also Exercise
23.9
). Whenever a packet
transmission continues, the pointer is incremented (Lines
14
-
15
;Rule
TX4
). Finally,
when the packet transmission has been completed, the pointer is reset to 0 (Line
16
).
See Exercise
23.10
regarding an alternative implementation of packet transmission.
Assumption
m_def_valid
(Line
20
) defines the conditions of data validity: at
the beginning of the packet transmission (
packet_start
asserted) or in its middle
(
ptr != 0
). We could eliminate free variable
valid
and use output argument
tx_valid
directly, because this assumption may be replaced with assignment
assign
tx_valid = packet_start || ptr != 0;
17
Remember that this problem exists only in simulation. In FV the reset value is sampled even in
disable iff
clauses.
Search WWH ::
Custom Search