← The journal

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:

  1. Request A is issued: source = 2, epoch = 12, tag = 7
  2. Tracker reset: Before Request A completes, the primary tracker undergoes a reset sequence.
  3. Request B is issued: The same tag is allocated to a new request: source = 2, epoch = 13, tag = 7
  4. 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.

One tag, two transaction lifetimes
  1. 01

    Request A is issued

    source = 2 · epoch = 12 · tag = 7

  2. 02

    The primary tracker resets

    Request A has not completed.

  3. 03

    Request B reuses the tag

    source = 2 · epoch = 13 · tag = 7

  4. 04

    Late response A arrives

    tag = 7 · payload = 0x55

Expected

Reject

The response belongs to expired epoch 12.

Observed defect

Invalid completion proposed

The defective check matches source OR epoch.

Matching the reused tag and source does not make a response valid for a new lifetime.

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.

Observed trace, including the decoy
TimeEvent
t = 1Request A: source=2, epoch=12, tag=7
t = 2Decoy request in the parallel tracker: source=5, epoch=13, tag=7
t = 3Reset the primary tracker.
t = 4Request B: source=2, epoch=13, tag=7
t = 5Late response A: payload=0x55. Completion output: expected 0, actual 1.
The decoy legitimately holds the same tag while the primary tracker changes ownership.

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:

From an observed completion to a falsified contract
  1. 01Observed completion
  2. 02Transaction ownership
  3. 03Source / epoch / tag predicate
  4. 04Falsified contract
Explain why the observed completion violates the transaction’s ownership requirement.

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:

Same response bits, different preserved histories
Identical response stimulus: tag = 7 · payload = 0x55
Preserved history 1

Request A remains outstanding

Current owner: source=2, epoch=12.

ACCEPT

Preserved history 2

Reset cancelled Request A

Request B reused tag 7: source=2, epoch=13.

REJECT

The repaired design produces the correct outcome for each history under the same response stimulus.
  • 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.

Evidence belongs to a particular design artifact
Repaired design artifact · v2
Bounded regression suite

4,096 / 4,096 passed

The result remains bounded regression evidence.

Valid evidence bound

Pre-fix evidence · v1

Hash mismatch detected

Earlier evidence does not apply to the repaired design.

Rejected as stale

Artifact binding preserves applicability; it does not turn a bounded result into an unbounded proof.

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.

Structured engineering meaning
  1. 01Design topology
  2. 02Execution history
  3. 03Ownership rules
  4. 04Verification intent
  5. 05Evidence scope
The investigation keeps observations connected to ownership, intent, and the scope of its evidence.

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.