Term project - Analyze minrv32 and verify its internals

# 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.

Syntax	Example	Reference
# Header	Header	基本排版
- Unordered List	Unordered List
1. Ordered List	Ordered List
- [ ] Todo List	Todo List
> Blockquote	Blockquote
Bold font	Bold font
Italics font	Italics font
~~Strikethrough~~	~~Strikethrough~~
19^th^	19^th
H~2~O	H₂O
++Inserted text++	Inserted text
==Marked text==	Marked text
[link text](https:// "title")	Link
![image alt](https:// "title")	Image
`Code`	`Code`	在筆記中貼入程式碼
```javascript var i = 0; ```	`var i = 0;`
:smile:		Emoji list
{%youtube youtube_id %}	Externals
$L^aT_eX$	L^aT_eX
:::info This is a alert area. :::	This is a alert area.