A crossing bug rarely looks like a CDC problem from the outside. It shows up as a coherence symptom: a message that should not exist, a hang, a lost value. Four bug classes cover most cases. The examples are illustrative, not reports of real designs.
Bug class | What is wrong | Symptom on the course model | Check that finds it |
|---|---|---|---|
Torn message | Message fields (type, address, transaction id) cross as separately synchronized bits instead of through a FIFO slot. | H receives a mix of two messages, for example Inv-Ack type with the id of a different transaction: an ack for a transaction with no pending entry, or a GetM for the wrong address. | CDC structural check: a multi-bit crossing with no recognised scheme. Protocol checker: response with no matching pending entry. |
Credit counter without synchronization | A binary credit count crosses directly. | Count 3 to 4 is 011 to 100. Sampled mid-change, the sender may see 111 = 7 credits, sends too many, and the receiver overwrites a slot: a lost message. | CDC structural check on the counter. Credit-conservation assertion. Overflow assertion on the receiver buffer. |
Reset domain crossing with stale credits | One side of the link is reset, the other keeps its credit count. | Receiver reset: buffered requests vanish, the sender's credits stay low, MSHRs wait forever. Sender reset: credits jump to full while slots are still occupied, so the next burst overflows. | RDC structural check. Credit-conservation assertion. Reset-aware simulation that resets one domain mid-traffic. |
Class merged at the crossing | Two classes share one in-order FIFO. | The P/Q deadlock of Part 5, inside the crossing. | Not a CDC check: review the class-to-FIFO map. Protocol-level deadlock search on a small model, or a stress test with a progress check. |
The last row matters most for this course: CDC and RDC tools check bits and resets, not message classes. Only a protocol view finds a merged class.
One invariant catches both credit bugs: for every crossing, the credits the sender holds, plus messages in the FIFO, plus credits on their way back, equals the depth. It is checked in simulation from a testbench view that sees both domains at once; it is not synthesizable logic across the crossing.
// snippet
// Simulation-only check: the testbench samples counts from both clock domains.
property p_credit_conservation;
@(posedge tb_clk) disable iff (!link_up)
(tx_credits + fifo_occupancy + credits_returning) == DEPTH;
endproperty
a_credit_conservation: assert property (p_credit_conservation);
a_no_overflow: assert property (@(posedge tb_clk) disable iff (!link_up)
fifo_occupancy <= DEPTH);Worked case: the cluster-to-H request crossing has depth 4. C0 has sent GetS(X) and GetS(Y), both still in the FIFO, so C0 holds 2 credits: 2 + 2 + 0 = 4. Now the H-side link logic alone takes a warm reset. The FIFO is cleared, and C0's two MSHRs (IS^D for X and Y) wait for Data that will never come. C0 still holds 2 credits: 2 + 0 + 0 = 2, and the assertion fires at the reset, long before any hang timeout. In the opposite bug, the cluster side alone resets: C0 gets 4 credits while 2 slots are still full, 4 + 2 + 0 = 6, and the next burst of four overflows the FIFO.
import random
DEPTH = 4
def new_link():
return {"credits": DEPTH, "fifo": [], "returning": 0}
def total(l):
return l["credits"] + len(l["fifo"]) + l["returning"]
def conserved(l):
return total(l) == DEPTH
def send(l, msg):
if l["credits"] == 0:
return False
l["credits"] -= 1
l["fifo"].append(msg)
return True
def receive(l):
l["fifo"].pop(0)
l["returning"] += 1
def credit_arrives(l):
l["returning"] -= 1
l["credits"] += 1
def traffic_step(l, rng):
r = rng.random()
if r < 0.4:
send(l, "GetS")
elif r < 0.7 and l["fifo"]:
receive(l)
elif l["returning"]:
credit_arrives(l)
def reset_receiver(l):
l["fifo"], l["returning"] = [], 0 # FIFO and credits on the way back are cleared
def reset_sender(l):
l["credits"] = DEPTH # sender believes every slot is free
def reset_both(l):
reset_receiver(l)
reset_sender(l)
# correct traffic alone keeps the invariant
rng = random.Random(7)
l = new_link()
for _ in range(2000):
traffic_step(l, rng)
assert conserved(l) and len(l["fifo"]) <= DEPTH
# each reset at a random point in seeded traffic, then traffic continues
seen = {"empty": 0, "busy": 0, "overflow": 0, "lost_for_good": 0}
for reset in (reset_receiver, reset_sender, reset_both):
for run in range(300):
rng = random.Random(1000 * len(reset.__name__) + run)
l = new_link()
for _ in range(rng.randrange(1, 40)):
traffic_step(l, rng)
idle = not l["fifo"] and l["returning"] == 0
seen["empty" if idle else "busy"] += 1
reset(l)
after = total(l)
if reset is reset_both:
assert conserved(l)
else:
assert conserved(l) == idle # one-sided reset is safe if and only if the link was idle
overflow = False
for _ in range(200):
traffic_step(l, rng)
assert total(l) == after # traffic never repairs a broken count
overflow = overflow or len(l["fifo"]) > DEPTH
if reset is reset_both:
assert conserved(l) and not overflow
if reset is reset_sender and overflow:
seen["overflow"] += 1
if reset is reset_receiver and total(l) < DEPTH:
seen["lost_for_good"] += 1
assert seen["empty"] and seen["busy"]
assert seen["overflow"] > 0 and seen["lost_for_good"] > 0
print("PASS: credit conservation survives reset_both, a one-sided reset is safe only on an idle link,",
"sender resets overflowed", seen["overflow"], "runs and receiver resets lost credits for good in", seen["lost_for_good"])The check first runs 2,000 seeded steps of correct traffic with the invariant holding throughout. It then applies each reset (receiver only, sender only, both) at a random point in 300 seeded runs and keeps the traffic going. Resetting both sides always restores the invariant. A one-sided reset keeps it if and only if the FIFO was empty and no credit was returning, and traffic never repairs a broken count: sender-only resets let more messages into the FIFO than it has slots, and receiver-only resets leave credits lost for good, the MSHR hang of the worked case.
The merged class. Its bits cross through a correct FIFO and its resets are fine, so CDC and RDC tools have nothing to report. Only a review of which classes share which FIFO, or a protocol-level deadlock search, finds it.