riscv-formal-nmigen/insns/README.md

1.7 KiB

RISC-V Instructions

Refer to the table below for the instructions currently supported. At the time of writing, it covers the instructions in the RV32I base ISA except FENCE, ECALL and EBREAK, as well as the RV32M extension*.

Instruction type Instructions
U-type lui, auipc
UJ-type jal
I-type jalr, lb, lh, lw, lbu, lhu, addi, slti, sltiu, xori, ori, andi
SB-type beq, bne, blt, bge, bltu, bgeu
S-type sb, sh, sw
I-type (shift variation) slli, srli, srai
R-type add, sub, sll, slt, sltu, xor, srl, sra, or, and, mul, mulh, mulhsu, mulhu, div, divu, rem, remu

* Due to limitations with modern solvers, they are sometimes unable to verify assertions involving multiplication and/or division; therefore, the core under test is expected to implement alternative operations for the RV32M extensions for the purposes of formal verification only, replacing multiplication/division operations with addition/subtraction and XORing with selected bitmasks.

Caveats

At the time of writing, the set of instructions supported in this port of riscv-formal is a mere subset of those supported in the original riscv-formal; for example, compressed instructions and 64-bit ISAs/extensions are not supported. Also note that the original riscv-formal contains tunable parameters that have been fixed to certain values in this translation:

Parameter from riscv-formal Fixed value in riscv-formal-nmigen
RISCV_FORMAL_ILEN 32
RISCV_FORMAL_XLEN 32
RISCV_FORMAL_CSR_MISA undefined
RISCV_FORMAL_COMPRESSED undefined
RISCV_FORMAL_ALIGNED_MEM undefined
RISCV_FORMAL_ALTOPS defined