Analyze minrv32 and implement compressed instruction set

Our contribution to compressed instruction RV32IC

contributed by < Jack, Ching-Hong Fang, anfong-query>

tags: RISC-V, Computer Architure 2021, Term project

---

Table of Contents

• Analyze minrv32 and implement compressed instruction set
  • Introduction
  • RISCV formal checking
    • Environment Setting (Ubuntu-20.04)
  • Implement Compressed ISA (RV32C)
    • Opcode and instruction format
    • Make RV32I compatible with RV32IC
    • Register in RVC
    • The compressed instructions that we implement
  • Consideration When Implementing

Introduction

minrv32 is a minimal RISC-V Implementation without a register file. It is inspired by the "MOS Technology 6502" which has very few registers. The main feature of minRV32 is that it has only one register (program counter) for this cpu. It can use "zero page" as registers. That is, all of the register files (i.e. a0, s1, t3) may be fetched from the memory.

RISCV formal checking

RISCV-formal is a RISC-V processors verificater and use the SymbiYosys as the formal verification flow. All properties are expressed using immediate assumptions for maximal compatibility with other tools.

Environment Setting (Ubuntu-20.04)

1. Git clone the riscv-formal into the directory that is beside the minrv32 directory, at the same heirarchical level
2. Install Yosys, SymbiYosys, Z3, Boolector and some prerequisites from here.
3. Go to minrv32/minrv32-formal directory and run the command below to generate the testing case.

$ python3 genchecks.py

To verify the compressed instruction, we must modify the isa from rv32i to rv32ic in minrv32/minrv32-formal/checks.cfg first.

4. Execute the command below to validate the design through riscv formal verification.

$ make -C checks -j$(nproc) 

Implement Compressed ISA (RV32C)

To distinguish between the normal instruction (RV32I) and compressed instruction (RV32IC), we can focus on inst[1:0]. If it is 2'b11, it must be RV32I instruction.

Below is the code we modify from the original version, arghhhh/minrv32.

+ assign rs1_addr = rs1_addr_valid ? (c_insn_field_opcode == 2'b11) ? insn_field_rs1 : c_rs1_addr : 5'b0;
+ assign rs2_addr = rs2_addr_valid ? (c_insn_field_opcode == 2'b11) ? insn_field_rs2 : c_insn_field_rs2 : 5'b0;
+ assign rd_addr  = rd_addr_valid  ? (c_insn_field_opcode == 2'b11) ? insn_field_rd  : c_rd_addr  : 5'b0;

- assign rs1_addr = rs1_addr_valid ? insn_field_rs1 : 5'b0;
- assign rs2_addr = rs2_addr_valid ? insn_field_rs2 : 5'b0;
- assign rd_addr  = rd_addr_valid  ? insn_field_rd : 5'b0;

Opcode and instruction format

Make RV32I compatible with RV32IC

Before we implement compressed instructions, we found that the B and J type instructions in rv32i do not pass the formal verification for rv32ic. After comparing the sby files, we found that it will set ialign16 to 1, if we define RISCV_FORMAL_COMPRESSED.

Consulting the riscv-spec-v2.2, we realize that misaligned exceptions are not possible on machines support 16-bit aligned instruction, such as compressed instruction set extension, C.

Therefore, we remove the code below in comb_rv32.v. Finally, B and J type pass the verification for rv32ic.

gen_trap = |pc_next[1:0];

Also, in order to make riscv-formal verification work for RV32IC, we have to modify rvfi_rs1_rdata, rvfi_rs2_rdata and rvfi_rd_rdata. Therefore, it can get the correct rs1, rs2 and rd value.

+ assign rvfi_rs1_rdata  = `valid_data_or_x( rvfi_valid && rs1_addr != 0, ( rs1_addr_valid ) ? ((c_insn_field_opcode == 2'b11) ? rs1_value : c_rs1_value) : 32'b0 );
+ assign rvfi_rs2_rdata  = `valid_data_or_x( rvfi_valid && rs2_addr != 0, ( rs2_addr_valid ) ? ((c_insn_field_opcode == 2'b11) ? rs2_value : c_rs2_value) : 32'b0 );
+ assign rvfi_rd_wdata   = `valid_data_or_x( rvfi_valid, ( rd_addr_valid && ( rd_addr != 0 ) ) ? rd_wdata  : 32'b0 );

- assign rvfi_rs1_rdata  = `valid_data_or_x( rvfi_valid && rs1_addr != 0, ( rs1_addr_valid ) ? rs1_value : 32'b0 );
- assign rvfi_rs2_rdata  = `valid_data_or_x( rvfi_valid && rs2_addr != 0, ( rs2_addr_valid ) ? rs2_value : 32'b0 );
- assign rvfi_rd_wdata   = `valid_data_or_x( rvfi_valid, ( rd_addr_valid && ( insn_field_rd != 0 ) ) ? rd_wdata  : 32'b0 );

Register in RVC

RVC uses a simple compression scheme that offers shorter 16-bit versions of common 32-bit RISC-V instructions when:

1. the immediate or address offset is small
2. one of the registers is the zero register (x0), the ABI link register (x1), or the ABI stack pointer (x2)
3. the destination register and the first source register are identical
4. the registers used are the 8 most popular ones.

Below are the instructions that using the special register to decrease the needs of bits.

• Using link register (x1)
  C.JAL (x1 as rd)
  C.JALR (x1 as rd)

• Using stack pointer (x2)
  C.ADDI16SP (x2 as rs1)
  C.ADDI14SPN (x2 as rs1)
  C.LWSP (x2 as rs1)
  C.SWSP (x2 as rs1)

• Using the 8 most popular RVI registers
  The instructions below only use x8 to x15 register for their rs1 or rs2 or rd.
  C.LW
  C.SW
  C.SRLI
  C.SRAI
  C.ANDI
  C.SUB
  C.XOR
  C.OR
  C.AND
  C.BEQZ
  C.BNEZ

The compressed instructions that we implement

We implement the instructions in riscv-formal/insns/isa_rv32ic.txt, which includes 25 compressed instructions and we pass all the riscv formal verification.

To look at the contribution we made, please refer to this page.

isa_rv32ic.txt

add
addi
and
andi
auipc
beq
bge
bgeu
blt
bltu
bne
c_add
c_addi
c_addi16sp
c_addi4spn
c_and
c_andi
c_beqz
c_bnez
c_j
c_jal
c_jalr
c_jr
c_li
c_lui
c_lw
c_lwsp
c_mv
c_or
c_slli
c_srai
c_srli
c_sub
c_sw
c_swsp
c_xor
jal
jalr
lb
lbu
lh
lhu
lui
lw
or
ori
sb
sh
sll
slli
slt
slti
sltiu
sltu
sra
srai
srl
srli
sub
sw
xor
xori

Partial result of BMC

SBY 21:23:14 [insn_auipc_ch0] DONE (PASS, rc=0)
SBY 21:23:16 [insn_andi_ch0] DONE (PASS, rc=0)
SBY 21:23:16 [insn_and_ch0] DONE (PASS, rc=0)
SBY 21:23:17 [insn_addi_ch0] DONE (PASS, rc=0)
SBY 21:23:17 [insn_add_ch0] DONE (PASS, rc=0)
SBY 21:23:17 [insn_bgeu_ch0] DONE (PASS, rc=0)
SBY 21:23:17 [insn_bge_ch0] DONE (PASS, rc=0)
SBY 21:23:19 [insn_beq_ch0] DONE (PASS, rc=0)
SBY 21:23:24 [insn_c_addi16sp_ch0] DONE (PASS, rc=0)
SBY 21:23:26 [insn_c_addi4spn_ch0] DONE (PASS, rc=0)
SBY 21:23:27 [insn_bne_ch0] DONE (PASS, rc=0)
SBY 21:23:27 [insn_blt_ch0] DONE (PASS, rc=0)
SBY 21:23:28 [insn_c_and_ch0] DONE (PASS, rc=0)
SBY 21:23:29 [insn_c_addi_ch0] DONE (PASS, rc=0)
SBY 21:23:29 [insn_c_add_ch0] DONE (PASS, rc=0)
SBY 21:23:29 [insn_bltu_ch0] DONE (PASS, rc=0)
SBY 21:23:32 [insn_c_andi_ch0] DONE (PASS, rc=0)
SBY 21:23:35 [insn_c_jal_ch0] DONE (PASS, rc=0)
SBY 21:23:36 [insn_c_j_ch0] DONE (PASS, rc=0)
SBY 21:23:36 [insn_c_li_ch0] DONE (PASS, rc=0)
SBY 21:23:36 [insn_c_jalr_ch0] DONE (PASS, rc=0)
SBY 21:23:37 [insn_c_jr_ch0] DONE (PASS, rc=0)
SBY 21:23:38 [insn_c_beqz_ch0] DONE (PASS, rc=0)
SBY 21:23:39 [insn_c_bnez_ch0] DONE (PASS, rc=0)
SBY 21:23:39 [insn_c_lui_ch0] DONE (PASS, rc=0)
SBY 21:23:42 [insn_c_lw_ch0] DONE (PASS, rc=0)
SBY 21:23:43 [insn_c_mv_ch0] DONE (PASS, rc=0)
SBY 21:23:43 [insn_c_or_ch0] DONE (PASS, rc=0)
SBY 21:23:43 [insn_c_lwsp_ch0] DONE (PASS, rc=0)
SBY 21:23:47 [insn_c_srli_ch0] DONE (PASS, rc=0)
SBY 21:23:49 [insn_c_sub_ch0] DONE (PASS, rc=0)
SBY 21:23:49 [insn_c_slli_ch0] DONE (PASS, rc=0)
SBY 21:23:50 [insn_c_srai_ch0] DONE (PASS, rc=0)
SBY 21:23:50 [insn_c_sw_ch0] DONE (PASS, rc=0)
SBY 21:23:51 [insn_c_xor_ch0] DONE (PASS, rc=0)
SBY 21:23:53 [insn_jal_ch0] DONE (PASS, rc=0)
SBY 21:23:54 [insn_c_swsp_ch0] DONE (PASS, rc=0)
SBY 21:23:59 [insn_lui_ch0] DONE (PASS, rc=0)
SBY 21:23:59 [insn_jalr_ch0] DONE (PASS, rc=0)
SBY 21:24:01 [insn_lb_ch0] DONE (PASS, rc=0)
SBY 21:24:01 [insn_lhu_ch0] DONE (PASS, rc=0)
SBY 21:24:02 [insn_lbu_ch0] DONE (PASS, rc=0)
SBY 21:24:03 [insn_lh_ch0] DONE (PASS, rc=0)
SBY 21:24:05 [insn_lw_ch0] DONE (PASS, rc=0)
SBY 21:24:05 [insn_or_ch0] DONE (PASS, rc=0)
SBY 21:24:08 [insn_ori_ch0] DONE (PASS, rc=0)
SBY 21:24:10 [insn_sb_ch0] DONE (PASS, rc=0)
SBY 21:24:10 [insn_sh_ch0] DONE (PASS, rc=0)
SBY 21:24:10 [insn_sll_ch0] DONE (PASS, rc=0)
SBY 21:24:14 [insn_slt_ch0] DONE (PASS, rc=0)
SBY 21:24:14 [insn_slli_ch0] DONE (PASS, rc=0)
SBY 21:24:14 [insn_sltiu_ch0] DONE (PASS, rc=0)
SBY 21:24:16 [insn_slti_ch0] DONE (PASS, rc=0)
SBY 21:24:18 [insn_sltu_ch0] DONE (PASS, rc=0)
SBY 21:24:19 [insn_srai_ch0] DONE (PASS, rc=0)
SBY 21:24:20 [insn_sra_ch0] DONE (PASS, rc=0)
SBY 21:24:20 [insn_srl_ch0] DONE (PASS, rc=0)
SBY 21:24:23 [insn_srli_ch0] DONE (PASS, rc=0)
SBY 21:24:24 [insn_sw_ch0] DONE (PASS, rc=0)
SBY 21:24:24 [insn_sub_ch0] DONE (PASS, rc=0)
SBY 21:24:24 [insn_xor_ch0] DONE (PASS, rc=0)
SBY 21:24:25 [insn_xori_ch0] DONE (PASS, rc=0)

Consideration When Implementing

1. No pipeline (1 stage)
   Stall until instruction complete.
2. Wait for register access
   Because instruction directly access zero memory, we must wait until rs1 and rs2 are ready if we need them. Below are the examples.

Fig 1, For C.ADD, instruction completeion need to wait until rs1 and rs2 are ready.

---

Fig 2, For C.JALR, instruction completeion need to wait until rs1 is ready. Because C.JALR do not need rs2 fetching, we don't need to wait on rs2 ready.

---

Fig 3, For C.J, instruction completeion do not need to wait. Because C.J does not use any register file.