Case Study: The Response Was Correct. The Transaction Was Wrong.
Tag reuse, reset, and transaction ownership: a controlled experiment in preserved history and bounded verification evidence.
A hardware response can contain the exact right bits and still be wrong.
Not because the payload is corrupted. Not because the tag is malformed or the physical interface is broken. But because the response belongs to a transaction lifetime that no longer exists.
That distinction is easy for a human designer to describe on a whiteboard, but preserving it reliably across reset, tag reuse, concurrency, hierarchy, and automated investigation requires more than present-time signal values.
At Memdance, we are building an AI-native hardware engineering stack designed to keep design meaning, execution state, verification obligations, and verification evidence connected across the engineering flow.
In our previous case study, we examined how semantic design identity can be preserved across spatial transformations (e.g., in FIFO structures). In this experiment, we turn to a temporal challenge: Can our engineering stack distinguish two interface responses that look identical at the signal layer, but belong to entirely different transaction lifetimes?
The short answer is yes. The broader lesson is that correctness in hardware design often depends on preserved execution history rather than present-time values.
1. A Simple Defect with Deeper Implications
An independently authored ownership specification supplied the intended behavior. A separate event oracle derived transaction owners from input events, without reading tracker registers or relying on known-good design outputs.
To test this boundary, we constructed a deliberately compact scenario centered on a transaction tracker with tag reuse and epoch tracking:
- Request A is issued:
source = 2,epoch = 12,tag = 7 - Tracker reset: Before Request A completes, the primary tracker undergoes a reset sequence.
- Request B is issued: The same tag is allocated to a new request:
source = 2,epoch = 13,tag = 7 - Late response arrives: The delayed completion payload (
0x55) for Request A finally returns to the interface.
To the receiving interface, this response appears plausible: tag = 7 points to an active entry, the payload is uncorrupted, and source = 2 matches the current owner. However, because the response belongs to epoch 12 rather than epoch 13, the correct hardware behavior is to reject the payload.
- 01
Request A is issued
source = 2 · epoch = 12 · tag = 7 - 02
The primary tracker resets
Request A has not completed.
- 03
Request B reuses the tag
source = 2 · epoch = 13 · tag = 7 - 04
Late response A arrives
tag = 7 · payload = 0x55
Reject
The response belongs to expired epoch 12.
Invalid completion proposed
The defective check matches source OR epoch.
The Injected Defect
We injected a bug into the transaction-identity comparison logic. Instead of requiring a strict conjunction (source AND epoch), we weakened the ownership check to a disjunction (source OR epoch):
- Correct Predicate:
(response.source == entry.source) AND (response.epoch == entry.epoch) - Defective Predicate:
(response.source == entry.source) OR (response.epoch == entry.epoch)
This creates an insidious class of bug: the response payload looks valid, points to an occupied entry, and satisfies part of the identity check. A diagnosis based only on present-time interface values would not be sufficient to distinguish matching bits from valid ownership.
2. Root-Cause Analysis and Decoy Trackers
At t=5, the design proposed a completion where the independent oracle expected rejection. The ownership monitor rejected that proposal before the clock event committed. The failure therefore demonstrates an invalid completion proposal; it does not show corrupt state escaping the monitor.
| Time | Event |
|---|---|
| t = 1 | Request A: source=2, epoch=12, tag=7 |
| t = 2 | Decoy request in the parallel tracker: source=5, epoch=13, tag=7 |
| t = 3 | Reset the primary tracker. |
| t = 4 | Request B: source=2, epoch=13, tag=7 |
| t = 5 | Late response A: payload=0x55. Completion output: expected 0, actual 1. |
Preserving Meaning Beyond Stale-Packet Detection
Detecting that a transaction failed at t=5 is straightforward. The real challenge for an automated engineering system is explaining why it failed without human intervention.
To achieve this, the system must maintain an explicit semantic chain connecting signal-level observations back to verification obligations:
- 01Observed completion
- 02Transaction ownership
- 03Source / epoch / tag predicate
- 04Falsified contract
The Role of Decoy State
To ensure the system did not achieve "accidental success" via naive tag lookup, we introduced a second parallel tracker (source=5, epoch=13, tag=7) that legitimately held tag 7 during the same window.
Without this decoy, a shallow diagnostic tool might correctly identify tag 7 simply because it was the only candidate in the design. With the decoy active, the investigation had to distinguish transaction ownership rather than succeed through tag matching alone. It localized the failure to the primary tracker’s identity policy rather than the secondary tracker.
3. Evaluating the Fix Space: Why Partial Repairs Fail
The maintained structure also lets us evaluate candidate repair policies against explicit property requirements. Following the initial failure, a deterministic search evaluated four defined candidate identity policies. No LLM inferred the protocol or generated arbitrary repairs in this experiment:
| Identity Policy | Rejects Stale Epoch? | Rejects Wrong Requester? | Overall Result |
|---|---|---|---|
| Source OR Epoch (Defective) | No | No | Fail |
| Source Only | No | Yes | Fail |
| Epoch Only | Yes | No | Fail |
| Source AND Epoch (Correct) | Yes | Yes | Pass |
This evaluation demonstrates why simple "patch-and-pass" iterations are dangerous in complex IP design. Checking source alone addresses requester mismatched bugs but leaves the design vulnerable to epoch reuse; checking epoch alone prevents stale lifetime bugs but fails under multi-requester concurrency. Only the complete conjunction (Source AND Epoch) satisfies the verification contract.
After the repair, the original scenario passed in direct and compiled execution. Additional event sequences covered misrouted responses, completion and tag reuse on the same clock edge, late duplicates, and legitimate completion of the competing request.
4. Central Result: Counterfactual Replay ("Same Bits, Different Histories")
Same response. Same visible state. Different correct result. The difference was transaction ownership preserved in history.
To directly test whether system behavior depended on preserved temporal context rather than static interface values, we executed a counterfactual experiment on the repaired design.
We restored two distinct, preserved execution histories and presented the exact same response stimulus (tag=7, payload=0x55) to both:
Request A remains outstanding
Current owner: source=2, epoch=12.
ACCEPT
Reset cancelled Request A
Request B reused tag 7: source=2, epoch=13.
REJECT
- Preserved History 1: Request A was still outstanding (
source=2, epoch=12). Result:ACCEPT - Preserved History 2: Reset occurred, canceling Request A; Request B reused tag 7 (
source=2, epoch=13). Result:REJECT
Prior to packet arrival, the public interface outputs of both executions were identical. The design was identical. The incoming payload was identical.
Yet History 1 accepted the transaction, while History 2 rejected it. This demonstrates the central result of the experiment: correctness was not encoded in the response bits alone, but depended on preserved transaction history.
For both histories, restored execution matched uninterrupted execution. The captured ownership keys also agreed with the independently reconstructed event history. The differing verdicts were therefore checked against both the history and the uninterrupted run.
5. Evidence Scoping and Artifact Binding
Following the fix, we subjected the repaired design to a bounded verification sweep across the identity space:
- 2 independent trackers
- 8 unique source IDs
- 16 epoch values
- 8 tag values
- 2 execution modes
The bounded sweep covered 2,048 response-identity cases in each of two execution modes, for 4,096 executions in total. All passed.
Those are 2,048 distinct probes repeated in direct and compiled execution. They start from one fixed reset-and-reuse history with payload 0x55; they are not 4,096 distinct transaction histories.
Explicit Evidence Scoping
In the Memdance framework, passing a 4,096-execution sweep does not automatically promote a property to an unbounded formal proof. The system explicitly logs these results as bounded regression evidence, leaving the formal obligation open until unbounded proof targets are met. Preserving the exact mathematical scope of verification evidence prevents false confidence during integration.
4,096 / 4,096 passed
The result remains bounded regression evidence.
Valid evidence bound
Hash mismatch detected
Earlier evidence does not apply to the repaired design.
Rejected as stale
Artifact Hash Binding
In this experiment, evidence from the pre-repair design was rejected against the repaired artifact because the design identity had changed. This prevents that evidence from silently being treated as applicable to the new design.
A stale source edit was also rejected against the repaired source. Evidence applicability and edit applicability were both checked against the artifacts they were meant to describe.
A complete repeat reproduced 53 generated artifacts byte-for-byte. A separate run renamed instances, shifted source positions, and inserted an unused lookalike predicate; localization still reached the intended tracker. These perturbations test names and positions, not arbitrary optimization passes.
The response-key sweep does not exhaust arbitrary histories, payloads, backpressure, or epoch wrap. Epochs are supplied by the fixture; epoch generation is outside this experiment. Execution and replay were checked at the design level, not on a physical netlist.
6. Takeaways for AI-Native Hardware Engineering
Generative AI models excel at syntax generation and local pattern matching. However, robust hardware design requires managing state and identity across time and abstraction layers.
- 01Design topology
- 02Execution history
- 03Ownership rules
- 04Verification intent
- 05Evidence scope
When autonomous systems evaluate hardware failures, asking "What value is on this bus?" is rarely sufficient. They must be able to resolve:
- Which requester owns this payload?
- Which generation or epoch issued the request?
- Did an intervening reset invalidate the lifetime of this transaction?
- Which specific verification contract governs this event?
Maintaining those relationships gives engineering agents a stronger substrate for investigation than source text, logs, or present-time values alone.
Our goal at Memdance is to determine how far that model can be pushed across increasingly difficult hardware-engineering problems. Systemic confidence in hardware must always be built on reproducible evidence—never on plausible-looking code.