---
# System prepended metadata

title: Term project - Analyze minrv32 and verify its internals
tags: [Computer Architecture]

---

# Term project - Analyze minrv32 and verify its internals 
###### tags: `Computer Architecture`
## minrv32 - A RISC-V core without Register File
[minrv32](https://github.com/arghhhh/minrv32) takes inspiration from the processors of [MOS 6502](https://en.wikipedia.org/wiki/MOS_Technology_6502), which included a [zero-page](https://en.wikipedia.org/wiki/Zero_page) addressing mode that uses one address byte in the instruction instead of the two needed to address the full 64 KB of memory. These type of architecture use the main memory as an extended pool of extra registers.


**Table of Contents**
[TOC] 

## Verilog Modules 
Let's take a look at the verilog modules of `minrv32` project first. We can find 4 verilog files in this project, including `comb_rv32.v`,`minlib.v`,`minrv32.v`and`rvfi_monitor`. Here is the main purpose of each file:
* `comb_rv32.v`: The developer separates out the combinational logic from the core and put it in this file.
* `minlib.v`: A module libaray.
* `minrv32.v`: A RISC-V (RV32I) Processor Core. 
* `rvfi_monitor`: An additional rvfi monitor for debugging.
### Combinational decode logic 
Remind that RISC-V base instruction formats is like: 
![](https://i.imgur.com/EnaJuRz.png)

In `comb_rv32.v` file, the following code specified the combinatorial RISC-V ISA decode logic:
* R type instruction decode logic
```clike=
wire [6:0] insn_field_opcode = insn[6:0];
wire [2:0] insn_field_funct3 = insn[14:12];
wire [6:0] insn_field_funct7 = insn[31:25];
wire [4:0] insn_field_rd     = insn[11:7];
wire [4:0] insn_field_rs1    = insn[19:15];
wire [4:0] insn_field_rs2    = insn[24:20];
```
* I, S, B, U, J type instruction decode logic 
```clike=
// For I-type sign-extended 12-bit
wire [31:0] immediate_12bit = { {20{insn[31]}}, insn[31:20] };
// For S-type sign-extended 12-bit
wire [31:0] immediate_12bit_for_stores = { immediate_12bit[31:5], insn[11:7] };
// For J-type sign-extended 21-bit, where the J-immediate encodes a signed offset in multiples of 2 bytes, so the LSB is 0
wire [31:0] immediate_for_jal = { {12{insn[31]}}, insn[19:12], insn[20], insn[30:21], 1'b0 };
// For B-type sign-extended 13-bit, where the B-immediate encodes a signed offset in multiples of 2 bytes, so the LSB is 0
wire [31:0] immediate_for_branches = { {20{insn[31]}}, insn[7], insn[ 30:25], insn[11:8], 1'b0 };
wire [31:0] pc_next_no_branch = insn_addr + 4;
wire [31:0] pc_next_branch = ( insn_addr + immediate_for_branches ) & 32'hFFFF_FFFE;
```

* After instructions breakdown into different field, instead of accessing register file, `minrv32` implements a combinational logic to control memory access. Take Load type instructions for example:
```clike=
if (insn_field_opcode == 7'b 00_000_11) begin // LOAD
	insn_decode_valid = (insn_field_funct3 != 3'b 011) && (insn_field_funct3 != 3'b 110) && (insn_field_funct3 != 3'b 111);
	rs1_addr_valid = 1 ;
	rd_addr_valid  = 1 ;
	mem_valid = 1;
	mem_addr = rs1_value + immediate_12bit;
	if (insn_field_funct3 == 3'b000 ) begin // LB  load byte
	        mem_rmask = 4'b0001;
	        rd_wdata = { {24{mem_rdata[7]}}, mem_rdata[7:0] };
	end
	if (insn_field_funct3 == 3'b100 ) begin // LBU  load byte unsigned
		mem_rmask = 4'b0001;
		rd_wdata = { 24'b0, mem_rdata[7:0] };
	end
	if (insn_field_funct3 == 3'b001 ) begin // LH  load half word
		mem_rmask = 4'b0011;
		rd_wdata = { {16{mem_rdata[15]}}, mem_rdata[15:0] };
	end
	if (insn_field_funct3 == 3'b101 ) begin // LHU load half word unsigned
		mem_rmask = 4'b0011;
		rd_wdata = { 16'b0, mem_rdata[15:0] };
	end
	if (insn_field_funct3 == 3'b010 ) begin // LW  load word
		mem_rmask = 4'b1111;
		rd_wdata = mem_rdata;
	end
end
```
The value of `insn_field_opcode` and `insn_field_funct3` signal line controls what the value of  `mem_rmask` and `rd_wdata` signal line will be. The data load from memory will be set to `rd_wdata` signal line.
:::info
**Note:** Since each instruction directly access zero-page memory. The only ISA state is the program counter! 
:::


### State logic and cache
In `minrv32.v` file, the following code specified the sequential state logic:

* **Program counter**
Program counter will be set to next value when the positive edge of the clock occurs.
```clike=
localparam PROGADDR_RESET = 'h10000;

// hardware should not need to know about the STACKADDR.  This will be removed...
localparam STACKADDR      = 'h10000;

reg  [31:0] pc;
wire [31:0] pc_next;

initial pc = PROGADDR_RESET;
always @(posedge clk) begin
	pc <= resetn ? ( insn_complete ? pc_next : pc ) : PROGADDR_RESET;
end
```


* **Cache**
If load/stores unable to access the memory region where RISC-V ISA register values are stored, there must be a processor trap to handle the exception. That is why we need additional cache(temporary register) to store the additional memory fetches.
In this implemention, cache consists of two registers named `rs1` and `rs2`. The circuit can be divided into two parts:
**1. A multiplexer** 
This multiplexer checks whether or not the cache access is valid (`rsX_addr_valid` and `cache_rsX_valid` value), then decide which cache register to access. 
```clike=
always @(*) begin
	cache_rs1_valid_next = cache_rs1_valid;
	cache_rs2_valid_next = cache_rs2_valid;
	cache_rs1_next = cache_rs1;
	cache_rs2_next = cache_rs2;
	rs_addr  = 0;

	if ( cache_clear_next ) begin
		cache_rs1_valid_next = 0;
		cache_rs2_valid_next = 0;
		cache_rs1_next = 0;
		cache_rs2_next = 0;
	end 
	//else
	 begin
		if ( rs1_addr_valid && !cache_rs1_valid ) begin
			rs_addr = rs1_addr;
			cache_rs1_next = rs_rdata;
			cache_rs1_valid_next = rs_ready;
		end else if ( rs2_addr_valid && !cache_rs2_valid ) begin
			rs_addr = rs2_addr;
			cache_rs2_next = rs_rdata;
			cache_rs2_valid_next = rs_ready;
		end
	end
end
```

   **2. Two Cache registers**
These registers save the `cache_rsX_next` value when positive edge of clock occurs.
```clike=
assign cache_clear_next = insn_complete;

// reg  cache_clear;
wire rs_ready = 1;  // a register read can always take place ... for now

reg        cache_rs1_valid;
reg        cache_rs2_valid;
reg        cache_rs1_valid_next ;
reg        cache_rs2_valid_next ;

assign rs1_rdata = cache_rs1;
assign rs2_rdata = cache_rs2;

always @(posedge clk  )
if ( !resetn ) begin
	cache_rs1_valid <= 0;
	cache_rs2_valid <= 0;
//	cache_clear     <= 1;
	cache_rs1       <= 0;
	cache_rs2       <= 0;
end else begin
	cache_rs1_valid <= cache_rs1_valid_next;
	cache_rs2_valid <= cache_rs2_valid_next;
//	cache_clear <= cache_clear_next;
	cache_rs1 <= cache_rs1_next;
	cache_rs2 <= cache_rs2_next;
end
```
### Zero page memory 
The zero page or base page is the block of memory at the very beginning of a computer's address space; that is, the page whose starting address is zero. However, its not perferable to set the starting address to zero sometimes.

In this project, zero-page haven't been implemented yet. To make `minrv32` testable, 32 registers were implemented temporarily to enable GTKwave to see the register contents.   
```clike=
reg [31:0] registers [ 0:31 ];
always @(posedge clk) begin
	if ( !resetn ) begin
		registers[ 0] <= 0;
// use USE_MYSTDLIB in Makefile to avoid needing the stack pointer to be set in hardware
// I think the bootloader would deal with setting the stack pointer otherwise...
// .. but there is no bootloader.
//		registers[ 2] <= STACKADDR;
	end
	if ( rd_request && insn_complete ) begin
		registers[ rd_addr ] <= rd_wdata;
	end
end
```
The architecture to arbitrate`rs1` and `rs2` register access is as following.
![](https://i.imgur.com/p10BIIZ.png)

## Verification
### Bounded model check(BMC) - riscv-formal proofs for minrv32
#### Tools for BMC - Yosys, SymbiYosys, and the SMT solvers (Boolector)
SymbiYosys (sby) is a front-end driver program for Yosys-based formal hardware verification flows. SymbiYosys provides flows for Bounded verification of safety properties (assertions). In this project, it will be used to verify `minrv32` .
Here are two introduction video:
[An introduction to Formal Verification Part 1](https://www.youtube.com/watch?v=8UwSUY1dECw)
[An introduction to Formal Verification Part 2](https://www.youtube.com/watch?v=tgTt-8UqSMU)
#### Verification process
After `Yosys`, `SymbiYosys`, and the `SMT solvers` are installed, go to the `minrv32-formal` file and input these instructions below into the terminal:
```bash
$ python3 genchecks.py
$ make -C checks -j$(nproc) > check.txt
```
`genchecks.py` in the `minrv32-formal` file will generate 43 checks(.sby file) for you.
Then the verification flows (`Yosys`, `SymbiYosys`) will verify `minrv32` by carrying out these 43 bounded model check(BMC).
![](https://i.imgur.com/pRIrXjn.png)
Take `causal_ch0.sby` for example, its content is like:
```
[options]
mode bmc
expect pass,fail
append 0
tbtop wrapper.uut
depth 6
skip 5

[engines]
smtbmc boolector

[script]  
read_verilog -sv causal_ch0.sv
read_verilog -sv /root/minrv32/minrv32-formal/wrapper.sv
read_verilog /root/minrv32/minrv32-formal/../minlib.v
read_verilog /root/minrv32/minrv32-formal/../comb_rv32.v
read_verilog /root/minrv32/minrv32-formal/../minrv32.v
prep -flatten -nordff -top rvfi_testbench
chformal -early

[files]  
/root/minrv32/minrv32-formal/../../riscv-formal/checks/rvfi_macros.vh
/root/minrv32/minrv32-formal/../../riscv-formal/checks/rvfi_channel.sv
/root/minrv32/minrv32-formal/../../riscv-formal/checks/rvfi_testbench.sv
/root/minrv32/minrv32-formal/../../riscv-formal/checks/rvfi_causal_check.sv

[file defines.sv]
`define RISCV_FORMAL
`define RISCV_FORMAL_NRET 1
`define RISCV_FORMAL_XLEN 32
`define RISCV_FORMAL_ILEN 32
`define RISCV_FORMAL_CHECKER rvfi_causal_check
`define RISCV_FORMAL_RESET_CYCLES 2
`define RISCV_FORMAL_CHECK_CYCLE 5
`define RISCV_FORMAL_CHANNEL_IDX 0
`define RISCV_FORMAL_ALTOPS
`define PICORV32_CSR_RESTRICT
`define PICORV32_TESTBUG_NONE
`define DEBUGNETS
`include "rvfi_macros.vh"

[file causal_ch0.sv]
`include "defines.sv"
`include "rvfi_channel.sv"
`include "rvfi_testbench.sv"
`include "rvfi_causal_check.sv"
```
  
This defines the configuration of a bounded model check (BMC). In `[script]` section, the commands will pass through the yosys. Then the files in `[files]`section will operating on the verilog. 
#### Results
Finally, will can see the result of the verfication:
:point_down:
:::spoiler Result of BMC (Click here) 
```
make: Entering directory '/home/smallhanley/minrv32/minrv32-formal/checks'
sby -f insn_add_ch0.sby
sby -f insn_addi_ch0.sby
sby -f insn_and_ch0.sby
sby -f insn_andi_ch0.sby
SBY 23:09:06 [insn_add_ch0] Removing directory 'insn_add_ch0'.
SBY 23:09:06 [insn_add_ch0] Writing 'insn_add_ch0/src/defines.sv'.
SBY 23:09:06 [insn_add_ch0] Writing 'insn_add_ch0/src/insn_add_ch0.sv'.
SBY 23:09:06 [insn_add_ch0] Copy '/home/smallhanley/minrv32/minrv32-formal/../../riscv-formal/checks/rvfi_macros.vh' to 'insn_add_ch0/src/rvfi_macros.vh'.
SBY 23:09:06 [insn_add_ch0] Copy '/home/smallhanley/minrv32/minrv32-formal/../../riscv-formal/checks/rvfi_channel.sv' to 'insn_add_ch0/src/rvfi_channel.sv'.
SBY 23:09:06 [insn_add_ch0] Copy '/home/smallhanley/minrv32/minrv32-formal/../../riscv-formal/checks/rvfi_testbench.sv' to 'insn_add_ch0/src/rvfi_testbench.sv'.
SBY 23:09:06 [insn_add_ch0] Copy '/home/smallhanley/minrv32/minrv32-formal/../../riscv-formal/checks/rvfi_insn_check.sv' to 'insn_add_ch0/src/rvfi_insn_check.sv'.
SBY 23:09:06 [insn_add_ch0] Copy '/home/smallhanley/minrv32/minrv32-formal/../../riscv-formal/insns/insn_add.v' to 'insn_add_ch0/src/insn_add.v'.
SBY 23:09:06 [insn_add_ch0] engine_0: smtbmc boolector
SBY 23:09:06 [insn_add_ch0] base: starting process "cd insn_add_ch0/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 23:09:06 [insn_andi_ch0] Removing directory 'insn_andi_ch0'.

.
.
.
sby -f causal_ch0.sby
SBY 23:09:39 [causal_ch0] Removing directory 'causal_ch0'.
SBY 23:09:39 [causal_ch0] Writing 'causal_ch0/src/defines.sv'.
SBY 23:09:39 [causal_ch0] Writing 'causal_ch0/src/causal_ch0.sv'.
SBY 23:09:39 [causal_ch0] Copy '/home/smallhanley/minrv32/minrv32-formal/../../riscv-formal/checks/rvfi_macros.vh' to 'causal_ch0/src/rvfi_macros.vh'.
SBY 23:09:39 [causal_ch0] Copy '/home/smallhanley/minrv32/minrv32-formal/../../riscv-formal/checks/rvfi_channel.sv' to 'causal_ch0/src/rvfi_channel.sv'.
SBY 23:09:39 [causal_ch0] Copy '/home/smallhanley/minrv32/minrv32-formal/../../riscv-formal/checks/rvfi_testbench.sv' to 'causal_ch0/src/rvfi_testbench.sv'.
SBY 23:09:39 [causal_ch0] Copy '/home/smallhanley/minrv32/minrv32-formal/../../riscv-formal/checks/rvfi_causal_check.sv' to 'causal_ch0/src/rvfi_causal_check.sv'.
SBY 23:09:39 [causal_ch0] engine_0: smtbmc boolector
SBY 23:09:39 [causal_ch0] base: starting process "cd causal_ch0/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 23:09:39 [causal_ch0] base: /home/smallhanley/minrv32/minrv32-formal/../minrv32.v:414: Warning: Identifier `\pc_next_valid' is implicitly declared.
.
.
.

SBY 23:10:20 [reg_ch0] engine_0: ##   0:00:40  Status: passed
SBY 23:10:20 [reg_ch0] engine_0: finished (returncode=0)
SBY 23:10:20 [reg_ch0] engine_0: Status returned by engine: pass
SBY 23:10:20 [reg_ch0] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:41 (41)
SBY 23:10:20 [reg_ch0] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:41 (41)
SBY 23:10:20 [reg_ch0] summary: engine_0 (smtbmc boolector) returned pass
SBY 23:10:20 [reg_ch0] DONE (PASS, rc=0)
make: Leaving directory '/home/smallhanley/minrv32/minrv32-formal/checks'

```
:::
`minrv32` passed all the 43 BMCs.
### Performance evaluation
:::info
Prerequisites: 
* Install [riscv-gnu-toolchain](https://github.com/riscv/riscv-gnu-toolchain)
* [Add the path to the environment variable](https://mindchasers.com/dev/rv-getting-started) so that we can source when we need to work with the toolchain
:::
We can use `dhrystone`, a  synthetic computing benchmark program, to evaluate the performance of minrv32.
:point_down:
:::spoiler Result of running the dhrystone (Click here)
```bash
~/minrv32/dhrystone$ make test
riscv32-unknown-elf-gcc -c -MD -O3 -march=rv32i -DTIME -DRISCV -DUSE_MYSTDLIB -ffreestanding -nostdlib -Wno-implicit-int -Wno-implicit-function-declaration dhry_1.c
riscv32-unknown-elf-gcc -c -MD -O3 -march=rv32i -DTIME -DRISCV -DUSE_MYSTDLIB -ffreestanding -nostdlib -Wno-implicit-int -Wno-implicit-function-declaration dhry_2.c
riscv32-unknown-elf-gcc -c -MD -O3 -march=rv32i -DTIME -DRISCV -DUSE_MYSTDLIB -ffreestanding -nostdlib stdlib.c
riscv32-unknown-elf-gcc -c -MD -O3 -march=rv32i -DTIME -DRISCV -DUSE_MYSTDLIB -ffreestanding -nostdlib start.S
riscv32-unknown-elf-gcc -MD -O3 -march=rv32i -DTIME -DRISCV -DUSE_MYSTDLIB -ffreestanding -nostdlib -Wl,-Bstatic,-T,sections.lds,-Map,dhry.map,--strip-debug -o dhry.elf dhry_1.o dhry_2.o stdlib.o start.o -lgcc
chmod -x dhry.elf
riscv32-unknown-elf-objcopy -O verilog dhry.elf dhry.hex
riscv32-unknown-elf-objdump --disassemble dhry.elf > dhry.elf.S
vvp -N testbench.vvp
VCD info: dumpfile testbench.vcd opened for output.
START

Dhrystone Benchmark, Version 2.1 (Language: C)

Program compiled without 'register' attribute

Please give the number of runs through the benchmark: 
Execution starts, 100 runs through Dhrystone
Execution ends

Final values of the variables used in the benchmark:

Int_Glob:            5
        should be:   5
Bool_Glob:           1
        should be:   1
Ch_1_Glob:           A
        should be:   A
Ch_2_Glob:           B
        should be:   B
Arr_1_Glob[8]:       7
        should be:   7
Arr_2_Glob[8][7]:    110
        should be:   Number_Of_Runs + 10
Ptr_Glob->
  Ptr_Comp:          81572
        should be:   (implementation-dependent)
  Discr:             0
        should be:   0
  Enum_Comp:         2
        should be:   2
  Int_Comp:          17
        should be:   17
  Str_Comp:          DHRYSTONE PROGRAM, SOME STRING
        should be:   DHRYSTONE PROGRAM, SOME STRING
Next_Ptr_Glob->
  Ptr_Comp:          81572
        should be:   (implementation-dependent), same as above
  Discr:             0
        should be:   0
  Enum_Comp:         1
        should be:   1
  Int_Comp:          18
        should be:   18
  Str_Comp:          DHRYSTONE PROGRAM, SOME STRING
        should be:   DHRYSTONE PROGRAM, SOME STRING
Int_1_Loc:           5
        should be:   5
Int_2_Loc:           13
        should be:   13
Int_3_Loc:           7
        should be:   7
Enum_Loc:            1
        should be:   1
Str_1_Loc:           DHRYSTONE PROGRAM, 1'ST STRING
        should be:   DHRYSTONE PROGRAM, 1'ST STRING
Str_2_Loc:           DHRYSTONE PROGRAM, 2'ND STRING
        should be:   DHRYSTONE PROGRAM, 2'ND STRING

Number_Of_Runs: 100
User_Time: 199869 cycles, 39022 insn
Cycles_Per_Instruction: 5.121
Dhrystones_Per_Second_Per_MHz: 500
DMIPS_Per_MHz: 0.284
DONE
TRAP
```
:::
The average CPI is 5.121 cycles. We can confirm this result by run the verilog code with testbench.

### Dumping Object Files
We can use `riscv32-unknown-elf-objdump` to objdump the test elf file. Then, we can get the riscv asm of our test program and use it to trace the cpu.
``` bash
~/minrv32/dhrystone$ riscv32-unknown-elf-objdump -d dhry.elf

dhry.elf:     file format elf32-littleriscv


Disassembly of section .memory:

00000000 <start-0x10000>:
	...

00010000 <start>:
   10000:	10000537          	lui	a0,0x10000
   10004:	05300593          	li	a1,83
   10008:	05400613          	li	a2,84
   1000c:	04100693          	li	a3,65
   10010:	05200713          	li	a4,82
   10014:	00a00793          	li	a5,10
   10018:	00b52023          	sw	a1,0(a0) # 10000000 <end+0xffebd03>
   1001c:	00c52023          	sw	a2,0(a0)
   10020:	00d52023          	sw	a3,0(a0)
   10024:	00e52023          	sw	a4,0(a0)
   10028:	00c52023          	sw	a2,0(a0)
   1002c:	00f52023          	sw	a5,0(a0)
   10030:	00000537          	lui	a0,0x0
   10034:	00000517          	auipc	a0,0x0
   10038:	00051513          	slli	a0,a0,0x0
   1003c:	01f51513          	slli	a0,a0,0x1f
   10040:	00000593          	li	a1,0
   10044:	00b51533          	sll	a0,a0,a1
   10048:	01f00593          	li	a1,31
   1004c:	00b51533          	sll	a0,a0,a1
   10050:	00010137          	lui	sp,0x10
   10054:	63c030ef          	jal	ra,13690 <main>
   10058:	10000537          	lui	a0,0x10000
   1005c:	04400593          	li	a1,68
   10060:	04f00613          	li	a2,79
   10064:	04e00693          	li	a3,78
   10068:	04500713          	li	a4,69
   1006c:	00a00793          	li	a5,10
   10070:	00b52023          	sw	a1,0(a0) # 10000000 <end+0xffebd03>
   10074:	00c52023          	sw	a2,0(a0)
   10078:	00d52023          	sw	a3,0(a0)
   1007c:	00e52023          	sw	a4,0(a0)
   10080:	00f52023          	sw	a5,0(a0)
   10084:	00100073          	ebreak
    .            .                        .
    .            .                        .
    .            .                        .
```


### Using GTKWave to view the waves
To view the waves of the testing, we use GTKwave to open the vcd file which was generated after `make test` (testbench.vcd). 

`minrv32` takes 5 CSR cycles to execute an instruction and 1 CSR cycle to signal instruction complete. You can find that the average CPI in `Dhrystone Benchmark` is about 5.121.
![](https://i.imgur.com/83xG9aP.png)


The testbench tests the processor for 199869 cycles. Take the these instructions below for instance:
![](https://i.imgur.com/pwc53a3.png)

Let's take a look at the instruction fields of these type of instructions.
![](https://i.imgur.com/YPQffk5.png)
***
The first instruction(lui) `0x10000537` will be break down into these fields:
* op code : `0b0110111`
* rd : `0b01010`
* imm[31:12] : `0b00010000000000000000`
The view of wave is like:
![](https://i.imgur.com/39aKZL0.png)

***
The second instruction(sw) `0x00b52023` will be break down into these fields:
* op code : `0b0100011`
* rs1 : `0b01010`
* rs2 : `0b01011`
* imm[11:5] : `0b0000000`
* imm[4:0] : `0b00000`
The view of wave is like:
![](https://i.imgur.com/va8uJdz.png)

***
The third instruction(aupic) `0x00000517` will be break down into these fields:
* op code : `0b0010111`
* rd : `0b01010`
* imm[31:12] : `0b00000000000000000000`
The view of wave is like:
![](https://i.imgur.com/4La6Z9p.png)
***
The fourth instruction(jal) `0x63c030ef` will be break down into  these fields:
op code: `0b0010011`
* op code : `0b1101111`
* rd : `0b00001`
* imm[31:12] : `0b1100011110000000011`
The view of wave is like:
![](https://i.imgur.com/7SElM3V.png)


### Issue about `sb`, `sh`, `lb`, `lbu`, `lh`, `lhu`
In `minrv32`, there are some control signals to control the read / write width, including 4-bit-signal `mem_rmask` and `mem_wstrb`. Every bit is mapped to one byte (address) of one word (4 bytes), and determines if the address should be read / write. Let's take instruction `sh` for example. We can write the following C code for the small test about store half (`sh`).
```c=
// test.c
int main(void){
        volatile short a = 10;    // instruction sh
        return 0;
}

```
Then, we can use riscv toolchain gcc to generate ELF file.
```
$ riscv32-unknown-elf-gcc -MD -O3 -march=rv32i -DTIME -DRISCV -DUSE_MYSTDLIB -ffreestanding -nostdlib -Wl,-Bstatic,-T,sections.lds,-Map,dhry.map,--strip-debug -o test.elf test.c -lgcc
```
The following is the objdump file of `test.elf`, the program will end at 10014 instruction `ret`.
```
~/minrv32/dhrystone$ riscv32-unknown-elf-objdump -d test.elf

test.elf:     file format elf32-littleriscv


Disassembly of section .memory:

00000000 <main-0x10000>:
	...

00010000 <main>:
   10000:	ff010113          	addi	sp,sp,-16
   10004:	00a00793          	li	a5,10
   10008:	00f11723          	sh	a5,14(sp)
   1000c:	00000513          	li	a0,0
   10010:	01010113          	addi	sp,sp,16
   10014:	00008067          	ret
   10018:	3a434347          	fmsub.d	ft6,ft6,ft4,ft7,rmm
   1001c:	2820                	fld	fs0,80(s0)
   1001e:	29554e47          	fmsub.s	ft8,fa0,fs5,ft5,rmm
   10022:	3120                	fld	fs0,96(a0)
   10024:	2e30                	fld	fa2,88(a2)
   10026:	2e32                	fld	ft8,264(sp)
   10028:	0030                	addi	a2,sp,8
   1002a:	1b41                	addi	s6,s6,-16
   1002c:	0000                	unimp
   1002e:	7200                	flw	fs0,32(a2)
   10030:	7369                	lui	t1,0xffffa
   10032:	01007663          	bgeu	zero,a6,1003e <main+0x3e>
   10036:	0011                	c.nop	4
   10038:	0000                	unimp
   1003a:	1004                	addi	s1,sp,32
   1003c:	7205                	lui	tp,0xfffe1
   1003e:	3376                	fld	ft6,376(sp)
   10040:	6932                	flw	fs2,12(sp)
   10042:	7032                	flw	ft0,44(sp)
   10044:	0030                	addi	a2,sp,8
```
![](https://i.imgur.com/HvuayXA.png)

To make a instruction memory that can be run with testbench, we can transform ELF file to HEX file.
```
$ riscv32-unknown-elf-objcopy -O verilog test.elf test.hex
```
Then, modify the testbench.v.
```clike
initial $readmemh("test.hex", memory);
```
In this way, the testbench can read the hex file to the reg `memory` as a program memory. However, minrv32 doesn't implement the real memory file, so we only can verify it through gtkwave signal or $display.

![](https://i.imgur.com/nh8Blct.png)

The instruction 0x00F11723 is `sh	a5,14(sp)` in risc-v assembly. We can see that `func3` is 001, which will decode to instruction `sh`. Then, the control signal `mem_wstrb` will be sended to memory or we say testbench here. The instruction, store half, will put the less 16 bits (2 byte) `mem_wdata` in the memory, so the control signal `mem_wstrb` will be 3 (0011). At the same time, `mem_addr` 0x0000000A (sp + 14) will be sent to memory, which means the memory address we store data.

The followinng verilog code is how testbench receives data and store to reg `memory`.
```c
if (mem_wstrb[0]) memory[mem_addr + 0] <= mem_wdata[ 7: 0];
if (mem_wstrb[1]) memory[mem_addr + 1] <= mem_wdata[15: 8];
if (mem_wstrb[2]) memory[mem_addr + 2] <= mem_wdata[23:16];
if (mem_wstrb[3]) memory[mem_addr + 3] <= mem_wdata[31:24];
```
Something interesting is that in some implementation, the memory address indicator is designed to a multiple of 4. That is, we will left shift the `mem_addr` 2 times before sending to memory. This will make the instruction decoding more complex. However, `minrv32` doesn't, so the design of `mem_wstrb` signal is simplier and we can just plus 0, 1, 2, 3 to `mem_addr` to decide which bytes we should write.