Skip to main content

Module riscv

logicaffeine_compile::codegen_sva::protocols

Module riscv

Expand description

RISC-V ISA Formal Verification Templates

Pre-verified instruction semantics as parameterizable SVA templates. Users describe their CPU configuration, templates generate SVA properties.

Structs§

RiscvConfig: RISC-V CPU configuration.

Enums§

RiscvExtension: RISC-V extension identifiers.

Functions§

riscv_alu_properties: Generate ALU instruction properties.
riscv_branch_properties: Generate branch instruction properties.
riscv_decoder_properties: Generate decoder mutual exclusion properties.
riscv_memory_properties: Generate memory access properties.
riscv_register_properties: Generate register file properties.