ISAudit: Finding Bugs in RISC-V Cores by Checking Against the ISA Specification

Hardware flaws are permanent: a CPU bug cannot be patched once fabricated, so it can only be fixed before tape-out. Whether a core behaves as specified by its instruction set architecture (ISA) is thus settled by pre-silicon verification. Yet existing techniques check proxies for the ISA specification rather than the specification itself, either a reference implementation that can itself be wrong or hand-written properties that cover only a subset of the specification, so a core can pass every check and still violate the specification. While Large Language Models (LLMs) offer automation potential, letting one interpret the specification and judge conformance directly faces two challenges: interpretation fidelity, where a prose clause may be misinterpreted, and verdict trust, where even a correct interpretation yields a verdict without mechanically checkable evidence. To bridge this gap, we introduce ISAudit, a specification-grounded auditing framework that makes the LLM’s interpretation of the specification executable and checkable. It first turns each normative statement into a formal property traceable to its source clause, binds it to the RTL, and derives two heterogeneous representations, each iteratively refined using the other to improve fidelity. Once the two representations reach a fixed point, it checks the settled property with a model checker, backing each violation with a concrete counterexample for triage. Evaluation on five opensource RISC-V cores shows that ISAudit uncovers 33 previously unknown bugs, outperforming baselines by 200–3,200%.