Interaction Tree Semantics for RISC-V: Bridging Compiler and Hardware Verification

TL;DR

This paper introduces a formal semantics for RISC-V using Interaction Trees, enabling cross-level verification from compiler IR to hardware, validated through case studies and an executable simulator.

Contribution

It provides the first comprehensive formal semantics of RISC-V in Rocq, supporting cross-level verification and covering many extensions, with machine-checked correctness and practical validation.

Findings

Proved semantic equivalence between LLVM IR and RISC-V code.

Validated instruction reordering safety for macro-operation fusion.

Confirmed hardware ALU correctness against RISC-V ISA contract.

Abstract

The Instruction Set Architecture (ISA) is the contract between compilers and processors; proving this contract formally demands cross-level connection to existing mechanized compilers and hardware implementations. As an open, modular ISA gaining adoption across embedded, mobile, and cloud platforms, RISC-V makes a formally verified ISA specification particularly valuable. However, existing formal RISC-V specifications focus on hardware tooling rather than cross-level verification: they provide no machine-checked instruction-level properties and lack support for verifying this contract across levels. We address these limitations with a formal semantics of the RISC-V ISA in Rocq, built on Interaction Trees (ITrees). By leveraging ITree bisimulation and refinement, our semantics enables cross-level verification from compiler IR to hardware within a single framework. Our formalization covers a wide spectrum of RISC-V extensions. The correctness of individual instruction semantics is backed by machine-checked lemmas in Rocq. We further validate it by extracting an executable simulator that passes all standard RISC-V test suites. Three case studies demonstrate the effectiveness of our semantics for cross-level verification: first, we prove semantic equivalence via bisimulation between LLVM IR and RISC-V code on an array access pattern via Vellvm (LLVM ITree semantics); second, we apply translation validation to a specific instruction reordering for macro-operation fusion, distinguishing safe reorderings from those that break program-counter-relative addressing; third, we prove that a K\^oika hardware ALU correctly implements all R-type integer operations (e.g., ADD, SUB, AND) against our ISA contract.