Guardat en:
| Autor principal: | |
|---|---|
| Format: | Recurso digital |
| Idioma: | |
| Publicat: |
Zenodo
2026
|
| Matèries: | |
| Accés en línia: | https://doi.org/10.5281/zenodo.20111982 |
| Etiquetes: |
Afegir etiqueta
Sense etiquetes, Sigues el primer a etiquetar aquest registre!
|
| _version_ | 1866901903360655360 |
|---|---|
| author | Wu, Yi-De |
| author_facet | Wu, Yi-De |
| 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). |
| format | Recurso digital |
| id | zenodo_https___doi_org_10_5281_zenodo_20111982 |
| institution | Zenodo |
| language | |
| publishDate | 2026 |
| publisher | Zenodo |
| record_format | zenodo |
| spellingShingle | rvsail v0.16.0 — FMCAD 2026 artifact: BOOM v3 ISA-Compliance proof bundle Wu, Yi-De formal verification RISC-V BOOM ISA compliance FMCAD 2026 SymbiYosys Sail 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). |
| title | rvsail v0.16.0 — FMCAD 2026 artifact: BOOM v3 ISA-Compliance proof bundle |
| topic | formal verification RISC-V BOOM ISA compliance FMCAD 2026 SymbiYosys Sail |
| url | https://doi.org/10.5281/zenodo.20111982 |