1. Purpose and governing principle
Coding, testing, release/offering, and implementation of a practical AI-assisted debugging system for RTL [Register Transfer Level] and digital hardware that discovers, ranks and revises intermediate verification waypoints. A formal engine [not an LLM] determines reachability, validates counter-examples and establishes proofs relative to a specified model and assumptions. The prototype is intended as a developer-operated system, not an autonomous sign-off tool.
Core division of labour: AI = hypothesis generation, search-space prioritisation and explanation. Formal verification = executable checking, counterexample production and proof. A candidate waypoint is never assumed to be necessary or reachable merely because AI/person proposed it.
2. Inputs, outputs and trust boundary
Outputs: ranked candidate waypoints; machine-readable property templates; executable formal jobs; checked trace segments; explanatory summaries; and a reproducible evidence report. All AI outputs must carry provenance and a status of proposed, checked, refuted, inconclusive or confirmed-under-assumptions.
3. Minimal executable architecture
Ingest & normalise → structural/temporal retrieval → LLM hypothesis agent → waypoint compiler and validator → formal job runner → trace analyser → critique/rerank loop → evidence report.
a. Retrieval: pair source-linked RTL/SVA excerpts with a deterministic signal dependency graph; do not rely on vector search alone.
b. Candidate generation: produce a small ordered set of predicates and temporal relationships that may lead from reset or an observed state to the failure.
c. Validation gate: syntax/type-check assertions; resolve signal names and clock domains; verify assumptions; require human approval before relaxing constraints or changing the analysis cone.
d. Formal interface: engine-neutral adapter with one concrete backend for the first build (e.g., a locally available commercial or open formal tool).
4. Waypoint object and state model
Represent each waypoint as an auditable typed object, rather than a free-text suggestion. Example conceptual schema:
Initial prototype will use a linear sequence W1 → W2 → failure. Store it as a directed graph from the outset so later builds can branch, backtrack or compare mutually exclusive hypotheses. Never treat failure to find a waypoint within a bound or resource limit as proof that it is unreachable.
5. AI–formal feedback loop
A single iteration is deliberately narrow, inspectable and repeatable:
a) Parse target error and available RTL/trace evidence; retrieve a limited, source-linked context.
b) 02 Propose 3–5 candidate waypoints with explicit predicates, ranking and rationale.
c) Reject malformed, unresolved or unsafe candidates before invoking the engine.
d) Execute cover/reachability checks, retaining exact design, constraints, seeds, bounds and budgets.
e) For SAT/covered results, replay or independently validate traces under the intended assumptions; use reachable endpoint states to seed subsequent segments where supported.
f) For UNSAT/proved results, record precisely what was proved and under what scope; for timeout/unknown, mark inconclusive.
g) Feed structured results—not just prose—back to AI for critique, repair, reordering or alternative-waypoint proposals.
h) Stop on validated failure trace, proof of the requested property, exhausted budget or manual termination.
6. Guardrails: proof, validity and reproducibility
a) Proof semantics: “SAT” establishes an example in the encoded model; “UNSAT” may be bounded only unless the engine certifies unbounded proof. Never conflate those statuses.
b) Trace legality: distinguish model-consistent traces from physically or protocol-legal ones; check reset reachability, environmental constraints and abstraction soundness.
c) AI containment: the LLM cannot alter trusted properties, weaken assumptions or pronounce a proof. Changes require an explicit diff and approval.
d) Evidence: store tool versions, model hashes, prompt/model identifiers, selected retrieved context, SVA text, run configurations and trace artefacts.
7. Working hypothesis
AI should make good verification waypoints easier to discover, explain and revise. It does not replace model-checking, nor does it transform a plausible narrative into mathematical evidence. The prototype succeeds when an engineer can reproduce every critical assertion and counterexample independently of the AI that suggested them.
Use a compact, deliberately constructed RTL bug (for example, a FIFO/counter wraparound or out-of-order memory operation), with a known counterexample and at least two plausible intermediate conditions. Keep the historical Anton case as methodological inspiration only; do not imply that its archived performance results measure the new AI system.
Decision gates: (1) choose an accessible formal backend and supported SVA subset; (2) choose a test RTL design and legal-input assumptions; (3) specify the candidate JSON contract and precise solver outcome taxonomy; (4) implement baseline and logging before attaching an LLM; (5) only then test whether AI reduces human debugging effort.