Skip to main contentCrate rvsail
Source - bridge
- RTL bridge verification: Verilog -> Yosys -> SMT2 -> Z3.
- composer
- KernelComposer: compose multiple instruction traces via Z3 substitution.
- llvm_ir
- LLVM IR → Z3 bitvector expressions.
- manifest
- TOML manifest schemas for kernel and bridge verification.
- mlir
- MLIR arith+vector dialect → Z3 bitvector expressions.
- rvfi_codegen
- RVFI codegen: convert Isla SMT traces to riscv-formal instruction checker Verilog.
- sexpr
- S-expression tokenizer and parser for Isla trace files.
- trace
- IslaTrace: parse Isla SMT trace files and convert to Z3 expressions.
- verify
- Three-layer verification runner.