L7Generator (Chisel/FIRRTL)
L6High-Level HDL
L5Compiler IR (MLIR/LLVM)39
L4Kernel / Instruction34
◆ L3 ORACLE HUB ◆
L3ISA Specification (Sail)43 traces
L2RTL (Verilog/VHDL)45
L1Silicon / Layout
L2
RTL ↔ ISA Specification
Yosys → SMT2 → Z3 ↔ Isla traces | EBMC SVA | rIC3 BTOR2
49 PASS8 SAT
| Target | Operations | Status | Time | Backends | ISA |
|---|
L3
ISA Specification — Oracle Hub
Isla symbolic traces from RISC-V Sail formal spec
43/43 AUDIT
| Trace Set | Count | Status | ISA |
|---|---|---|---|
| Scalar RV64I/M traces | 20 traces | AUDITED | RV64I/M |
| Vector RVV traces | 23 traces | AUDITED | RVV 1.0 |
L4
Kernel ↔ ISA Specification
Kernel SMT specs vs Isla instruction traces
34 PASS435ms
| Target | Kernels | Status | Time | ISA |
|---|---|---|---|---|
| ▶Vector Kernels (quantized ML) | 13 kernels | UNSAT | 344ms |
RVV |
| Q4_0 dequant | UNSAT | 28ms | ||
| Q4_1 dequant | UNSAT | 26ms | ||
| Q5_0 dequant | UNSAT | 30ms | ||
| Q5_1 dequant | UNSAT | 28ms | ||
| Q6_K dequant | UNSAT | 32ms | ||
| Q8_0 dequant | UNSAT | 24ms | ||
| Q8_1 dequant | UNSAT | 25ms | ||
| vecadd i8/i16/i32 | UNSAT | 60ms | ||
| ReLU | UNSAT | 25ms | ||
| conv1d | UNSAT | 38ms | ||
| vmacc dot | UNSAT | 28ms | ||
| ▶Scalar Instructions | 20 ops | UNSAT | 91ms |
RV64I/M |
| ADD/SUB/AND/OR/XOR | UNSAT | 20ms | ||
| SLL/SRL/SRA | UNSAT | 15ms | ||
| SLT/SLTU | UNSAT | 10ms | ||
| ADDW/SUBW/SLLW/SRLW/SRAW | UNSAT | 18ms | ||
| MUL/MULH/MULHU/DIV/REM | UNSAT | 28ms | ||
| Cross-ISA: RVV ↔ Wasm SIMD128 | 1 kernel | UNSAT | <1ms |
RVV+Wasm |
L5
Compiler IR ↔ ISA Specification
MLIR ↔ LLVM IR ↔ Isla trace equivalence
39 PASS
| Target | Proofs | Status | ISA |
|---|---|---|---|
| MLIR ↔ LLVM IR ↔ Isla (13 kernels × 3) | 39 proofs | UNSAT | RVV |
TC
Verification Toolchain
8 tools installed —
make check-toolsZ3
4.15.4 — SMT solver
Yosys
0.33 — SV→SMT2/BTOR2
EBMC
5.9 — bounded MC (SVA)
rIC3
1.5.2 — IC3/PDR (HWMCC gold)
Isla
Sail→SMT trace extraction
NEMU
XiangShan difftest (RVV)
Spike
1.1.1-dev — official ISS
Python
3.13 + pyboolector 3.2