← The journal

Case Study: Tracing a Hardware Failure to Evidence

An independent model, a controlled correction, and a result with clear boundaries.

What does an AI engineering agent need in order to investigate a hardware failure reliably?

Modern hardware development already has sophisticated tools for simulation, formal verification, debugging, waveform analysis, synthesis, and design navigation. At Memdance, we are exploring a narrower question: What changes if an AI agent can work with structured semantic and verification information maintained by the engineering system, instead of repeatedly reconstructing design meaning from source code, logs, waveforms, and tool output?

To test that idea, we built a deliberately small experiment around a FIFO. The FIFO itself is not particularly interesting—the experiment is. We wanted to determine whether an observed implementation-level failure could be connected back to the correct design behavior and associated verification requirement, and whether that connection would survive transformations and deliberate attempts to confuse the localization process. We also wanted verification evidence to retain its precise scope rather than silently becoming a stronger correctness claim than the evidence justified.


The Setup & Mismatch Detection

The test contains a small synchronous FIFO with an intentional defect in its read/write behavior. Alongside the implementation, we run an independent queue model that knows only the externally visible FIFO protocol.

Independent behavioral check
Implementation

Lowered FIFO netlist

Actual0
Semantic oracle

Independent queue model

Expected1
Mismatch detectedresult[0] · t = 3
The implementation and the independent model disagree on the same output bit at the same time step.

That separation is important. Two execution engines can agree perfectly with each other while faithfully executing the same incorrect design; execution agreement therefore does not establish that the implementation satisfies its intended behavior. The independent queue model provides a separate reference to answer: Given this sequence of FIFO operations, what should the externally visible result have been?

During the experiment, the implementation produced result[0] = 0 while the independent queue model expected result[0] = 1 at time t=3. At this point, we know only that the observed implementation behavior disagrees with the independent specification. We do not yet know which part of the design produced the behavior, which requirement is relevant, whether the relationship survives transformations, or whether a proposed fix actually addresses the root defect.


From Behavior to Design Contract

The system first localizes the failing implementation behavior back to the relevant semantic region of the design. Rather than reconstructing relationships solely through textual similarity, the identity chain is maintained directly by the compiler. An autonomous engineering agent should ideally be able to answer "What design behavior produced this observation?" without depending on convenient signal names, source locations, or object ordering.

From observation to requirement
  1. 01Observed failure
  2. 02Semantic localization
  3. 03Design behavior
  4. 04Verification requirement
Localize what produced the result, then identify the requirement that explains why it is incorrect.

Finding the part of the design responsible for an incorrect value explains what produced the behavior, but it does not explain why that behavior is incorrect. The experiment therefore connects the localized behavior to its associated verification requirement. For autonomous engineering, this distinction is critical: a useful investigation must connect an observation not only to implementation structure, but also to the engineering intent that gives that observation meaning.


Stress-Testing the Localization Engine

A localization mechanism can easily appear semantic while actually relying on structural coincidence—such as picking the first plausible memory, relying on fixed signal names, or matching source file line numbers. To challenge this, we deliberately introduced adversarial conditions into the design environment:

  • Decoy Insertion: Placed a structurally similar decoy FIFO earlier in the hierarchy.
  • Hierarchy & Naming Shifts: Added intermediate hierarchy levels, randomized internal net identifiers, and shifted source file offsets.
  • IR Transformation: Regenerated lower-level object ordering and net mappings.
CaseFailed NetTransformed ValueOriginal Semantic LocationTarget Position
Baseline1324top.queue, value 230 / 0
Nested Hierarchy + Decoy2464top.pipeline.queue, value 241 / 1

Despite the decoy occupying the earlier position and the real target moving deeper into the hierarchy, the system consistently localized the intended FIFO behavior. The investigation followed regenerated system-maintained relationships despite changes in names, hierarchy, source positions, and ordering.


Controlled Repair & Evidence Scoping

After retrieving the verification requirement associated with the affected behavior, the experiment evaluated a deliberately constrained set of three permitted candidate corrections. This demonstration is not an unconstrained LLM inventing arbitrary hardware changes; it tests whether a reproducible failure can be turned into a structured investigation whose candidate corrections are judged by independent evidence.

Three permitted candidate corrections
CandidateOriginal failureBroader checkingDecision
AFailFail—
BFailFail—
CPassPassAccepted
Candidate C passes both checks. Acceptance remains scoped to this controlled experiment.

Replay & Bounded Exploration (4,096 Traces)

After applying Candidate C, the original counterexample passed upon replay. The system then explored the complete finite input space of all 4,096 four-event queue traces.

  • Before Repair: Counterexample found, retained, and replay-verifiable.
  • After Repair: Original failure passed, and all 4,096 traces satisfied the independent queue model.

We explicitly do not claim the FIFO is universally proven correct; we claim that no counterexample was found in the complete finite search space defined for this experiment. The requirement remains marked as open, with the new evidence explicitly recorded as bounded. A bounded result should remain bounded, and a proof should be called a proof only when the relevant obligation has actually been discharged.


Evidence Integrity & Reproducibility

Automated systems can produce a particularly dangerous failure mode: producing a confident conclusion supported by stale evidence that no longer applies to the modified design.

  • Stale Evidence Rejection: We deliberately attempted six forms of stale or tampered artifact reuse (presenting pre-repair state or mismatched validation info). All six were rejected.
  • Deterministic Investigation: The baseline experiment was repeated independently, and all 30 retained artifacts reproduced byte-for-byte.
Integrity and repeatability

Reproducibility

30 artifacts
Reproduced byte-for-byte

Evidence integrity

6 stale or tampered cases
All rejected

Observed failureNew scoped evidence
Reproducibility and integrity support the investigation while the behavioral result stays bounded.

Summary of Findings & Boundaries

To maintain engineering rigor, we explicitly separate what this experiment demonstrates from what remains unaddressed:

What This Experiment Demonstrates

  1. Semantic Localization: Implementation-level failures connect reliably to design behavior without relying on string matching.
  2. Adversarial Resilience: Identity chains survive signal renaming, hierarchy shifts, line offsets, and structural decoy insertion.
  3. Contract Binding: Observed defects connect directly to actionable engineering assertions.
  4. Independent Acceptance & Replayability: Corrections are judged by external models, and counterexamples remain part of the retained evidence suite.
  5. Scoped Evidence & Determinism: Outdated proof artifacts are automatically invalidated, bounded results stay bounded, and artifacts reproduce byte-for-byte.

What This Experiment Does Not Demonstrate

  • Scalability to 10-Billion-Transistor SoCs: Demonstrates identity preservation across IR transformations, not large-scale SoC footprint management or multi-gigabyte netlist traversal.
  • Zero Compiler Overhead: Maintaining rich compiler state (clock maps, provenance, dependency graphs) adds runtime memory and compile overhead. The trade-off under evaluation is whether compiler compute saves orders of magnitude in automated debugging time.
  • Replacement of Commercial EDA Toolchains: Memdance complements established signoff engines from Synopsys, Cadence, or Siemens by exporting standard artifacts (SystemVerilog) rather than attempting a total replacement.
  • Arbitrary Repair Synthesis & Physical Signoff: Does not cover unconstrained AI synthesis, layout placement, timing closure, PPA optimization, or general specification completeness.

Why This Matters for AI Agents

Experienced hardware engineers already have sophisticated ways to trace drivers, navigate hierarchy, inspect waveforms, and perform formal analysis. However, the economics change when the primary consumer of that context is an autonomous agent.

Two ways to investigate

Traditional agent flow

  1. 01Unstructured logs / waveforms
  2. 02Probabilistic text parsing
  3. 03Fragile assumptions

Memdance queryable substrate

  1. 01Structured compiler state
  2. 02Direct programmatic query
  3. 03Deterministic tracing
The distinction in this experiment is how the agent obtains and follows the engineering context.

For an agent, there is a fundamental difference between parsing raw text logs and asking structured programmatic queries: What design behavior produced this observation? Which engineering requirement governs it? What evidence supports it, and does that evidence belong to the current design state?

Maintaining a dependable connection between observed hardware behavior, design meaning, and verification evidence provides a significantly better substrate for increasingly autonomous hardware engineering.