RTL Detective

Inspiration

A plausible RTL patch can compile and still be wrong by one clock cycle. Hardware engineers need a fast first responder that can propose a repair without asking them to trust an AI explanation.

What it does

RTL Detective validates a canonical synchronous FIFO or round-robin arbiter, runs directed and seeded-random transactions against a human-authored executable oracle, and records the exact failing cycle. It sends only the bounded failure evidence and untrusted DUT to NVIDIA Nemotron through Nebius Token Factory. The model proposes an investigation and candidate; deterministic Verilator evidence decides whether that candidate survives.

A successful claim requires every visible gate: baseline mismatch recorded, model request and token usage captured, failing reproducer saved, reproducer passed, independently locked regression passed, and verification assets unchanged. The result is a downloadable proof bundle with reports, hashes, traces, exact transactions, provider metadata, and logs.

How we built it

The service uses FastAPI, Pydantic, SQLite, server-sent events, and a responsive dark workbench. Nebius Token Factory provides OpenAI-compatible access to nvidia/nemotron-3-super-120b-a12b. Verilator 5.050 executes the oracle and candidate in a networkless, resource-bounded worker. The host restores the locked module header, constructs the canonical diff, and rejects path traversal, foreign files, test-disabling code, simulator control tasks, symlinks, and oversized input.

Challenges

The hardest part was separating a plausible model answer from evidence. Model-proposed stimulus can miss a known failure, so the host falls back to the exact baseline prefix instead of hiding the result or spending another request. A live review also caught a candidate specializing a locked parameter default; that led to deterministic header restoration and a stricter interface guard.

Accomplishments

A real hardened case-001 run made two Nebius requests to NVIDIA Nemotron, recorded 2,472 tokens, reproduced the cycle-7 mismatch, restored the locked header, and produced a candidate that passed an 8-transaction reproducer and an 80-transaction locked regression with all locked assets unchanged. The offline benchmark matched all 10 hidden labels, and the FIFO parameter matrix passed 18 configurations across 54 recorded seed/configuration combinations.

What we learned

AI should propose; deterministic evidence should decide. Precise claims, immutable artifacts, and honest unresolved outcomes make an agent more useful than a confident green badge.

What's next

Add more canonical RTL contract packs, persistent hosted evidence, and broader evaluation while keeping every claim bounded to replayable tests. Simulation is not formal proof.

Built With

• docker
• fastapi
• nebius
• nvidia
• python
• sqlite
• systemverilog
• verilator