Skip to content

Commit 7d6e117

Browse files
committed
fix(tomasulo): align LQ/SQ model full semantics with RTL pointer-based logic
The verification models used count == depth for full, while RTL uses pointer-based full (head_idx == tail_idx with differing MSBs). This caused random tests to gate allocation on the wrong predicate, so hole/occupancy scenarios from out-of-order frees were never exercised. Change both models to pointer-based full and add a deterministic SQ hole regression (test_pointer_full_with_hole) to match the existing LQ test. Strengthen the LQ hole test with model-agreement assertions.
1 parent c4c7c5d commit 7d6e117

File tree

4 files changed

+81
-6
lines changed

4 files changed

+81
-6
lines changed

verif/cocotb_tests/tomasulo/load_queue/lq_model.py

Lines changed: 10 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -219,8 +219,16 @@ def count(self) -> int:
219219

220220
@property
221221
def full(self) -> bool:
222-
"""Return whether the load queue model is full."""
223-
return self.count == self.depth
222+
"""Pointer-based full (matches RTL).
223+
224+
With out-of-order frees and partial flush, holes can exist between
225+
head and tail. The RTL reports full when the pointer space is
226+
exhausted even if some entries are invalid, so the model must too.
227+
"""
228+
return (
229+
self.head_ptr % self.depth == self.tail_ptr % self.depth
230+
and self.head_ptr != self.tail_ptr
231+
)
224232

225233
@property
226234
def empty(self) -> bool:

verif/cocotb_tests/tomasulo/load_queue/test_load_queue.py

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -837,9 +837,13 @@ async def test_tail_retraction_non_contiguous_hole(dut: Any) -> None:
837837
dut_if.clear_alloc()
838838

839839
assert dut_if.full, "LQ should be full after allocating remaining slots"
840-
# Valid count: 3 original + 4 new = 7 (idx 2 is a hole, still invalid)
841-
count = dut_if.count # type: ignore[unreachable]
840+
assert model.full, "Model pointer-full must agree with DUT" # type: ignore[unreachable]
841+
# Valid count: 3 original + 4 new = 7 (idx 2 is a hole, still invalid).
842+
# Pointer-based full fires with fewer than DEPTH valid entries — this is
843+
# accepted capacity loss from tail-only allocation with out-of-order frees.
844+
count = dut_if.count
842845
assert count == 7, f"Expected 7 valid entries (with hole), got {count}"
846+
assert model.count == 7, f"Model count must match DUT (got {model.count})"
843847

844848

845849
# ============================================================================

verif/cocotb_tests/tomasulo/store_queue/sq_model.py

Lines changed: 11 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -161,8 +161,17 @@ def count(self) -> int:
161161

162162
@property
163163
def full(self) -> bool:
164-
"""Return whether the store queue is full."""
165-
return self.count == self.depth
164+
"""Pointer-based full (matches RTL).
165+
166+
With out-of-order frees (SC discard, partial flush), holes can
167+
exist between head and tail. The RTL reports full when the
168+
pointer space is exhausted even if some entries are invalid,
169+
so the model must too.
170+
"""
171+
return (
172+
self.head_ptr % self.depth == self.tail_ptr % self.depth
173+
and self.head_ptr != self.tail_ptr
174+
)
166175

167176
@property
168177
def empty(self) -> bool:

verif/cocotb_tests/tomasulo/store_queue/test_store_queue.py

Lines changed: 54 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1293,3 +1293,57 @@ async def test_forward_lh_from_fsd_stalls(dut: Any) -> None:
12931293
assert fwd.match, "LH at FSD base should match"
12941294
assert not fwd.can_forward, "Sub-word load from DOUBLE store cannot forward"
12951295
dut_if.clear_sq_check()
1296+
1297+
1298+
# ============================================================================
1299+
# Test 38: Non-contiguous hole — pointer-full with fewer than DEPTH valid
1300+
# ============================================================================
1301+
@cocotb.test()
1302+
async def test_pointer_full_with_hole(dut: Any) -> None:
1303+
"""Partial flush creates a hole; pointer-full fires with < DEPTH valid entries.
1304+
1305+
Allocate out-of-ROB-order so partial flush creates:
1306+
idx 0(V:tag0) 1(V:tag1) 2(I:tag5) 3(V:tag2) 4(I:tag6) 5(I:tag7)
1307+
Tail retracts from 6→4 (stops at valid idx 3). Then allocate 4 more
1308+
to exhaust pointer space: pointer-full with only 7 valid entries.
1309+
Pointer-based full in the model must agree with the DUT.
1310+
"""
1311+
dut_if, model = await setup(dut)
1312+
dut_if.drive_rob_head_tag(0)
1313+
1314+
# Allocate 6 entries with tags that create a hole after flush.
1315+
# Tags 5, 6, 7 are younger than flush_tag=4; tags 0, 1, 2 are not.
1316+
for tag in [0, 1, 5, 2, 6, 7]:
1317+
dut_if.drive_alloc(rob_tag=tag, size=MEM_SIZE_WORD)
1318+
model.alloc(tag, False, MEM_SIZE_WORD)
1319+
await dut_if.step()
1320+
dut_if.clear_alloc()
1321+
1322+
assert dut_if.count == 6, f"Expected 6 entries, got {dut_if.count}"
1323+
assert model.count == 6
1324+
1325+
# Partial flush: tags 5, 6, 7 flushed (younger than 4 relative to head 0)
1326+
dut_if.drive_partial_flush(flush_tag=4)
1327+
model.partial_flush(4, 0)
1328+
await dut_if.step()
1329+
dut_if.clear_partial_flush()
1330+
1331+
assert dut_if.count == 3, f"Expected 3 valid entries, got {dut_if.count}"
1332+
assert model.count == 3
1333+
assert not dut_if.full, "SQ should not be full after partial flush"
1334+
assert not model.full, "Model should not be full after partial flush"
1335+
1336+
# Allocate 4 more entries to exhaust pointer space (tail wraps to head)
1337+
for i in range(4):
1338+
dut_if.drive_alloc(rob_tag=10 + i, size=MEM_SIZE_WORD)
1339+
model.alloc(10 + i, False, MEM_SIZE_WORD)
1340+
await dut_if.step()
1341+
dut_if.clear_alloc()
1342+
1343+
# Pointer-full with 7 valid entries (idx 2 is a hole)
1344+
assert dut_if.full, "SQ should be pointer-full after filling remaining slots"
1345+
assert model.full, "Model pointer-full must agree with DUT" # type: ignore[unreachable]
1346+
assert (
1347+
dut_if.count == 7
1348+
), f"Expected 7 valid entries (with hole), got {dut_if.count}"
1349+
assert model.count == 7, f"Model count must match DUT (got {model.count})"

0 commit comments

Comments
 (0)