Saved in:
| Main Author: | |
|---|---|
| Format: | Recurso digital |
| Language: | |
| Published: |
Zenodo
2026
|
| Subjects: | |
| Online Access: | https://doi.org/10.5281/zenodo.20111982 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
Table of Contents:
- Reproducibility artifact for FMCAD 2026 paper on end-to-end ISA-compliance verification of BOOM v3 (SmallBoomV3Config) and portability checks on Rocket and XiangShan. Contains all SymbiYosys (.sby) configurations, RVFI wrappers (boom_*_wrapper.sv), per-instruction Sail-derived checkers (insns64_sail/), divider lemma attempts, and shared lib/. Reproduces the 62 RV64IM compliance proofs (49 RV64I + 5 MUL + 8 DIV/REM), the ghost-accumulator divider lemma (62s under Boolector), and the cross-core sweeps on Rocket (42 RV64I) and XiangShan (47). Builds atop riscv-formal (SymbioticEDA @ 4f29e83a, 2021-11-26) and Sail RISC-V (bacam @ dc3864d).