Verification Stack: Model → Silicon

L3 is the hub. Both chains converge at the ISA specification. Sail/Isla produces SMT formulas that serve as oracle for either chain. PL chain: MLIR → LLVM IR → assembly → ISA. HDL chain: Chisel → FIRRTL → Verilog → ISA. RVS spans L2–L5, anchoring both chains: upward (13 vector kernels, 39 compiler IR proofs) and downward (10 RISC-V cores, 151 ops UNSAT, 8 hack@DAC bugs). Zero hand-written RTL.

Formal Work by Layer × ISA

L7 (Model), L6 (Quantization), L1 (Silicon) omitted — not in our scope. Shown in overview above.

Why RISC-V and Wasm are center

Our pipeline requires both a formal L3 spec and a symbolic execution toolchain (the L3→L4 bridge). Only RISC-V and Wasm have both.

This is the technical reason RISC-V and Wasm are our primary targets. ARM has L3 but not the bridge; x86 has neither. Building an ASL→SMT symbolic executor (an "Isla for ARM") is a significant engineering effort and a potential future research direction — but not ours.

Verification Landscape: Team × Layer

Every known RISC-V / processor verification tool mapped to our 7-layer model. Columns = teams, rows = layers. Key finding: nobody else spans more than 2 layers, and nobody connects to L3 (Sail) except us.

Key observations

1. Single-layer tools dominate. 10 of 12 tools cover exactly 1 layer. VeriISLE spans 2 (L3–L4). Only RVS spans 4 (L2–L5).

2. Nobody connects to L3. chiRVFormal hand-translates Sail to Chisel. riscv-formal uses bespoke RVFI. ChiselFV uses user-written SVA. All introduce unverified trust gaps at the oracle.

3. Scalar-only barrier. Every RISC-V RTL/HCL tool is scalar-only. The vector state explosion ($2^{16{,}456}$ for VLEN=256) is a structural barrier, not an engineering gap.

4. Isla is underused. Published at CAV 2021, adopted by Islaris and VeriISLE, but ignored by the Chisel ecosystem. chiRVFormal (SETTA 2024) chose to hand-translate Sail instead of using Isla — 3 years after Isla was available.

Extended ecosystem (C-based, simulation, model checking)

Beyond the Chisel formal ecosystem, these tools use C-based specifications, simulation co-verification, or hardware model checking.

State Explosion: RTL vs ISA Specification

RTL verification via bounded model checking must model the full microarchitectural state. At L3, microarchitectural state does not exist.

For context: the number of atoms in the observable universe ≈ 2²⁶⁶. Ara’s BMC search space is 2^150,000. The state explosion is structural — it comes from the hardware’s physical register file width, not from poor encoding. No RTL abstraction can fix this without losing per-element soundness.

Verification Data Inventory by Layer

Every result indexed to the 7-layer model. L3 is the oracle hub — all proofs flow through it.

hack@DAC bug database: 130+ bugs catalogued, 9 ISA-level (L2) bugs in our strike zone. RVS detected Bug #14 (ALU, RV32) and Bug #3 (CSR privilege escalation) with zero hand-written properties in <5 ms each.

L2 Automation Pipelines (Zero Hand-Written RTL)

Every core uses an automated pipeline from original RTL sources to SMT2. No manual ALU extraction or hand-written Verilog.

Four automation paths: (1) Direct Yosys on Verilog/SV (CVA6, SERV), (2) sv2v for complex SystemVerilog (Ibex, CV32E40P, SweRV), (3) firtool + Yosys for Chisel/FIRRTL (Rocket, riscv-mini, BOOM, XiangShan), (4) expose -evert-dff for monolithic CPUs without separate ALU (PicoRV32). All pipelines are scripted in rebuild_bridges.sh.

RISC-V L4 Ecosystem: Extension × Concern

RISC-V is modular — each extension family has independent instructions. Within each, compute kernel verification decomposes into four concerns by solver technique.

"Trivial" = our pipeline handles it, but scalar ops lack the SIMD complexity that makes L4 verification a research contribution. The tool covers them; the paper does not.

Wasm L4 Ecosystem: Proposal × Concern

Wasm is also modular (proposals). The decomposition mirrors RISC-V — each row maps to a RISC-V extension.

RISC-V ↔ Wasm Correspondence

Wasm is structurally simpler: no PMA/PMP (linear memory), no arbitrary jumps (structured CF), no variable-length vectors (fixed 128-bit). This makes cross-ISA proofs tractable — the hard part is always on the RISC-V side.

Expansion Map: Adjacency-Based Territory Growth

Next targets are adjacent to conquered territory. Two parallel fronts: Compiler (L5) expands vertically, Crypto expands horizontally.

Why L5 first? We already hold both endpoints: MLIR/LLVM IR specs (top) and Isla ISA traces (bottom). The compiler codegen gap in between is the last unverified link — and nobody does it for any vector ISA. Vertically adjacent to our L4 territory, maximum infrastructure reuse, highest impact.

Roadmap & Conference Deadlines

ARM L4 Ecosystem: Extension × Concern

ARM has a mature ISA spec (ASL) and rich extension set. Included for landscape completeness; not in our research scope.

ARM's L3 (ASL) is strong — machine-readable, maintained by Arm Ltd. The gap is L4: nobody has built a symbolic kernel verifier on top of ASL for NEON/SVE/CE. ASLi (interpreter) exists but is not a symbolic executor. The closest analog to our Isla would be building an ASL-to-SMT pipeline, which is a significant engineering effort.

x86 L4 Ecosystem: Extension × Concern

x86 has the largest deployed SIMD surface area but the weakest formal spec. Included for completeness.

x86's fundamental problem is L3: there is no machine-readable formal ISA spec. Intel's Software Architecture Manual (SAE) is prose; ACL2 models (Centaur) cover a subset. This makes x86 the hardest target for our pipeline — you'd need to build the ISA model first. Alive2 covers LLVM optimizations (L5 partial) but not codegen to specific SIMD extensions.

Cell References

Click any cell above to jump here. Click a cell ID below to jump back.