Finding What's Missing: Why LLMs are actually useful for Hardware Security
A client recently came to us with a problem that is quickly becoming the industry standard: they were doing everything “right” and yet they still felt blind.
They had the full suite - the $100k commercial licenses, the dedicated formal verification teams, the weeks of simulation. But they were stuck in a loop of verifying the code they had already written. They asked us the one question that most EDA vendors tend to dodge: How do we find the bugs we haven’t thought of yet?
It turns out, every tool in their multi-million dollar arsenal was effectively just a very expensive version of grep.
They all look for what’s there. Nobody is looking for what’s not.
The Syntactic Blind Spot
Here is how a standard security audit goes: The tool scans your RTL for signal names that look interesting. key_i? Generate a clearing assertion. lock_en? Check for stickiness. Map to a CWE, output some SVA, and call it a day.
Cadence JasperGold SecureCheck does this. Synopsys VC Formal does this. It’s “syntactic” verification. It checks the grammar of your security, but it has no idea what the story is about.
It can find a broken guard. It can’t find a guard that was never written in the first place.
We tried something
We were building an assertion generator for a client, doing the usual thing - classifying signals, mapping templates. It was fine. It was boring. But the client kept asking: What about the bugs we don’t have patterns for?
So we did something that felt too simple to work. We stopped asking the LLM to generate assertions for these signals and just gave it the whole module. The prompt was basically: Read this. What could go wrong?
We stopped treating RTL as a string of text to be regexed and started treating it as a reading comprehension problem.
The [redacted] Gap
We pointed it at a major, Tier-1 silicon root-of-trust project. This is a design with hundreds of formal assertions, multiple security reviews, and a dedicated verification team. It is “proven” secure.
The LLM read the lifecycle controller and flagged one specific state: PostTransSt:
That’s it. A no-op. The FSM finishes a 128-bit transition, enters this state, and does... nothing. The secret transition token—the keys to the kingdom—just sits there in the clear. It’s readable via JTAG because the designer simply forgot to add the line that clears it.
A pattern matcher will never catch a no-op. A linter doesn’t flag code that isn’t there. You have to understand that the token was used two states ago to realize that this state is suspiciously quiet.
The LLM caught the silence.
The “Babysitter” Loop
Look, LLMs hallucinate. If you ask one to write SVA, it’ll invent signal names and imagine state transitions like a bored intern. Most “AI for Hardware” projects die here.
We didn’t try to stop the hallucinations; we just built a loop to catch them. After the LLM proposes a finding, a second pass re-reads the original RTL to “fact-check” the AI.
Does this signal actually exist? * Is this state transition real? If the LLM makes something up, the loop kicks it back with a “Try again, that signal isn’t on the port list.”
The result? We hit 97.6% assertion correctness on security modules. Not because the LLM is a genius, but because we stopped treating it like a calculator and started treating it like a sloppy researcher who needs a proofreader.
The Honest Math
I’m not selling magic.
On security-oriented modules (debug, CSR, crypto), AssertX is a beast. It caught 13/15 HACK@DAC bugs and found confirmed gaps in PULP’s riscv-dbg.
But on protocol-heavy stuff like AXI interconnects or PCIe? It’s still struggling. Our false-positive rate on unfamiliar codebases is 35%. That’s too high for an “autopilot,” but it’s perfect for a supervised audit.
You spend your time reviewing high-intent assertions instead of staring at a blank VS Code window trying to remember how to write a complex SVA property.
The Point
Formal tools prove what you specify. But they can’t imagine what you forgot to specify.
The future isn’t AI replacing formal verification. It’s the LLM proposing the “what,” and the formal tools proving the “how.” One generates the questions; the other provides the answers.
We’re open-sourcing the core. One command: assertx scan your_module.sv.
I’m looking for verification engineers who are tired of the “Blind Spot” to break this thing. If you want to run it on a module and give me 15 minutes of brutal, honest feedback, DM me.