# Analyze minrv32 and implement compressed instruction set

[Our contribution to compressed instruction RV32IC](https://github.com/Chi-you/minrv32/compare/bcf8db..4562a7)

contributed by < [`Jack`](https://github.com/Chi-you), [`Ching-Hong Fang`](https://github.com/chinghongfang), [`anfong-query`](https://github.com/anfong-query)>
###### tags: `RISC-V`, `Computer Architure 2021`, `Term project`

---
**Table of Contents**
[toc]

## Introduction

minrv32 is a minimal RISC-V Implementation without a register file. It is inspired by the "[MOS Technology 6502](https://en.wikipedia.org/wiki/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](https://en.wikipedia.org/wiki/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](https://github.com/SymbioticEDA/riscv-formal) is a RISC-V processors verificater and use the [SymbiYosys](https://symbiyosys.readthedocs.io/en/latest/quickstart.html) 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](https://github.com/SymbioticEDA/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](https://symbiyosys.readthedocs.io/en/latest/install.html).
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](https://github.com/arghhhh/minrv32/blob/master/comb_rv32.v).

+ 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](https://riscv.org/wp-content/uploads/2017/05/riscv-spec-v2.2.pdf), 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](https://github.com/Chi-you/minrv32/compare/9b94c5c..6e73277).

:::spoiler {state="close"} 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

:::

:::spoiler {state="close"} 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.