# 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:
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.
## 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).
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.
The testbench tests the processor for 199869 cycles. Take the these instructions below for instance:
Let's take a look at the instruction fields of these type of instructions.
***
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:
***
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:
***
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:
***
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:
### 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
```
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.
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.
Sign in with Wallet
Connect another wallet