M-Labs/riscv-formal-nmigen
6
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity
1d315b4735
riscv-formal-nmigen/insns
History
Donald Sebastian Leung 7c60451bfa Add README for instructions
2020-08-05 12:54:46 +08:00
..
insn_add.py Add ADD instruction 2020-08-04 12:20:52 +08:00
insn_addi.py Add ADDI instruction 2020-07-31 16:39:32 +08:00
insn_and.py Add AND instruction 2020-08-04 12:54:46 +08:00
insn_andi.py Add ANDI instruction 2020-07-31 16:51:59 +08:00
insn_auipc.py Add AUIPC instruction 2020-07-31 13:44:22 +08:00
insn_beq.py Fix BEQ instruction 2020-08-03 10:29:17 +08:00
insn_bge.py Add BGE instruction 2020-08-03 10:42:27 +08:00
insn_bgeu.py Add BGEU instruction 2020-08-03 11:33:57 +08:00
insn_blt.py Add BLT instruction 2020-08-03 10:38:54 +08:00
insn_bltu.py Add BLTU instruction 2020-08-03 11:30:16 +08:00
insn_bne.py ADD BNE instruction 2020-08-03 10:33:45 +08:00
insn_div.py Add DIV instruction 2020-08-04 17:09:21 +08:00
insn_divu.py Add DIVU instruction 2020-08-04 17:12:13 +08:00
insn_I_shift.py Add I-type (shift variation) instruction format 2020-08-03 14:44:33 +08:00
insn_I.py Add I-type instruction class 2020-07-31 14:26:27 +08:00
insn_jal.py Add JAL instruction 2020-07-31 14:06:55 +08:00
insn_jalr.py Fix JALR instruction 2020-07-31 16:15:17 +08:00
insn_lb.py Add LB instruction 2020-07-31 16:14:48 +08:00
insn_lbu.py Add LBU instruction 2020-07-31 16:31:25 +08:00
insn_lh.py Add LH instruction 2020-07-31 16:19:04 +08:00
insn_lhu.py Add LHU instruction 2020-07-31 16:35:06 +08:00
insn_lui.py Add LUI instruction 2020-07-31 13:40:40 +08:00
insn_lw.py Add LW instruction 2020-07-31 16:27:36 +08:00
insn_mul.py Add MUL instruction 2020-08-04 16:57:43 +08:00
insn_mulh.py Add MULH instruction 2020-08-04 17:00:43 +08:00
insn_mulhsu.py Add MULHSU instruction 2020-08-04 17:04:04 +08:00
insn_mulhu.py Add MULHU instruction 2020-08-04 17:06:49 +08:00
insn_or.py Add OR instruction 2020-08-04 12:51:48 +08:00
insn_ori.py Add ORI instruction 2020-07-31 16:49:59 +08:00
insn_R.py Add R-type instruction format 2020-08-04 12:06:01 +08:00
insn_rem.py Add REM instruction 2020-08-04 17:14:46 +08:00
insn_remu.py Add REMU instruction 2020-08-04 17:17:37 +08:00
insn_S.py Add S-type instruction format 2020-08-03 14:15:09 +08:00
insn_sb.py Add SB instruction 2020-08-03 14:23:40 +08:00
insn_SB.py Add SB-type instruction 2020-08-03 10:19:01 +08:00
insn_sh.py Add SH instruction 2020-08-03 14:27:08 +08:00
insn_sll.py Add SLL instruction 2020-08-04 12:31:36 +08:00
insn_slli.py Add SLLI instruction 2020-08-03 14:51:36 +08:00
insn_slt.py Add SLT instruction 2020-08-04 12:34:06 +08:00
insn_slti.py Add SLTI instruction 2020-07-31 16:42:29 +08:00
insn_sltiu.py Add SLTIU instruction 2020-07-31 16:45:15 +08:00
insn_sltu.py Add SLTU instruction 2020-08-04 12:37:26 +08:00
insn_sra.py Add SRA instruction 2020-08-04 12:47:35 +08:00
insn_srai.py Add SRAI instruction 2020-08-03 15:10:58 +08:00
insn_srl.py Add SRL instruction 2020-08-04 12:42:39 +08:00
insn_srli.py Add SRLI instruction 2020-08-03 14:54:02 +08:00
insn_sub.py Add SUB instruction 2020-08-04 12:25:12 +08:00
insn_sw.py Add SW instruction 2020-08-03 14:29:52 +08:00
insn_types.md Categorize RV32IM instructions by type 2020-07-31 11:56:22 +08:00
insn_U.py Add U-type instruction class 2020-07-31 13:29:48 +08:00
insn_UJ.py Add UJ-type instruction class 2020-07-31 13:57:52 +08:00
insn_xor.py Add XOR instruction 2020-08-04 12:39:20 +08:00
insn_xori.py Add XORI instruction 2020-07-31 16:48:00 +08:00
insn.py Add generic instruction class 2020-07-31 13:06:03 +08:00
isa_rv32i_gen.py Complete generator for RV32I ISA 2020-07-23 14:33:25 +08:00
isa_rv32i.py Complete generator for RV32I ISA 2020-07-23 14:33:25 +08:00
isa_rv32i.txt Add list of supported instructions for RV32I 2020-07-23 11:18:41 +08:00
isa_rv32im_gen.py Add RV32IM ISA 2020-07-24 13:51:04 +08:00
isa_rv32im.py Add RV32IM ISA 2020-07-24 13:51:04 +08:00
isa_rv32im.txt Add RV32IM ISA 2020-07-24 13:51:04 +08:00
README.md Add README for instructions 2020-08-05 12:54:46 +08:00

README.md

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