Hardware Reference
In-Depth Information
However, we prefer to keep free variable
valid
because it improves the checker
readability and makes its code more robust for potential modifications of the
protocol.
Assumption
m_def_data
(Line
22
) requires
data
to contain the currently trans-
mitted bit when the result is valid. Assumption
m_new_only_if_start
(Line
24
)
takes care that
packet_start
is set for a new packet.
Lines
27
-
29
define an indication (
packet_seen
) that at least one packet has
arrived.
packet_seen
is zeroed at a reset. Assumption
m_new_if_start_not_seen
(Line
31
) takes care to set
new_packet
when the first packet has arrived.
Assumption
m_tx_packet_new
(Line
33
) limits packet generation to packets of
a legal type (Fig.
23.4
,Line
9
). It is sufficient to require this for new packets
only. Assumption
m_tx_packet_stable
(Line
35
) guarantees that the contents of
packet
may change only when a new packet arrives.
Lines
37
-
38
handle the quiet mode. Assumption
m_quiet_data
(Line
38
)
requires the data to be zero when the result is invalid (Rule
TX3
). Note that the
if
statement on Line
37
is a generate
if
as it belongs directly to the checker scope.
The checker also contains two sanity assertions that check its implementation.
Assertion
a_sanity_valid_0
(Line
39
) makes sure that the result is invalid until
the first packet starts transmitting. Assertion
a_sanity_valid_1
verifies that the
packet is transmitted continuously from the beginning to the end (Rule
TX4
).
As explained in Sect.
23.3.3
checker free variables are randomized in
simulation subject to the constraints imposed by the assumptions. Contemporary
simulators have strong abilities of solving combinatorial constraints. But our
checker contains two temporal assumptions:
m_non_overlap_start
(Line
7
) and
m_tx_packet_stable
(Line
35
). This may become an obstacle to generate a viable
test. Note, however, that the implementation of assumption
m_non_overlap_start
in simulation should be straightforward as the actual constraint on
packet_start
at
each clock is unambiguously defined by the values of this variable in the preceding
LENGTH - 1
clock cycles. As for assumption
m_tx_packet_stable
,itmaybe
rewritten as
##1 $changed(packet) |-> !new_packet
which makes it, essentially, combinational.
Exercises
23.1.
Define the formal semantics of unconditional free variable nonblocking
assignment controlled by a clocking event of each of the following forms:
(a)
@(
posedge
clk)
,
(b)
@(
negedge
clk)
,
(c)
@(
edge
clk
iff
en)
,
(d)
@(
posedge
clk
iff
en)
,
(e)
@(
negedge
clk
iff
en)
.
Search WWH ::
Custom Search