diff --git a/Makefile b/Makefile index 8004a56f5..468e4c59a 100644 --- a/Makefile +++ b/Makefile @@ -90,6 +90,7 @@ SAIL_VM_SRCS += riscv_vmem_pte.sail SAIL_VM_SRCS += riscv_vmem_ptw.sail SAIL_VM_SRCS += riscv_vmem_tlb.sail SAIL_VM_SRCS += riscv_vmem.sail +SAIL_VM_SRCS += riscv_vmem_utils.sail # Non-instruction sources PRELUDE = prelude.sail $(SAIL_XLEN) $(SAIL_FLEN) $(SAIL_VLEN) prelude_mem_metadata.sail prelude_mem.sail diff --git a/c_emulator/riscv_platform.c b/c_emulator/riscv_platform.c index 5b9852800..6e7765d2f 100644 --- a/c_emulator/riscv_platform.c +++ b/c_emulator/riscv_platform.c @@ -57,6 +57,16 @@ bool sys_enable_vext(unit u) return rv_enable_vext; } +bool sys_misaligned_order_decreasing(unit u) +{ + return rv_misaligned_order_decreasing; +} + +bool sys_misaligned_to_byte(unit u) +{ + return rv_misaligned_to_byte; +} + uint64_t sys_pmp_count(unit u) { return rv_pmp_count; @@ -108,7 +118,7 @@ mach_bits plat_rom_size(unit u) } // Provides entropy for the scalar cryptography extension. -mach_bits plat_get_16_random_bits() +mach_bits plat_get_16_random_bits(unit u) { return rv_16_random_bits(); } diff --git a/c_emulator/riscv_platform.h b/c_emulator/riscv_platform.h index 3cc6f0270..90855bf74 100644 --- a/c_emulator/riscv_platform.h +++ b/c_emulator/riscv_platform.h @@ -11,6 +11,9 @@ bool sys_enable_writable_misa(unit); bool sys_enable_writable_fiom(unit); bool sys_enable_vext(unit); +bool sys_misaligned_order_decreasing(unit); +bool sys_misaligned_to_byte(unit); + uint64_t sys_pmp_count(unit); uint64_t sys_pmp_grain(unit); @@ -26,7 +29,7 @@ mach_bits plat_rom_base(unit); mach_bits plat_rom_size(unit); // Provides entropy for the scalar cryptography extension. -mach_bits plat_get_16_random_bits(); +mach_bits plat_get_16_random_bits(unit); mach_bits plat_clint_base(unit); mach_bits plat_clint_size(unit); diff --git a/c_emulator/riscv_platform_impl.c b/c_emulator/riscv_platform_impl.c index 077fc50dc..2ebbc2838 100644 --- a/c_emulator/riscv_platform_impl.c +++ b/c_emulator/riscv_platform_impl.c @@ -6,6 +6,10 @@ uint64_t rv_pmp_count = 0; uint64_t rv_pmp_grain = 0; +/* Defaults for misaligned access behavior in the generated simulator */ +bool rv_misaligned_order_decreasing = false; +bool rv_misaligned_to_byte = false; + bool rv_enable_svinval = false; bool rv_enable_zcb = false; bool rv_enable_zfinx = false; diff --git a/c_emulator/riscv_platform_impl.h b/c_emulator/riscv_platform_impl.h index c4289e679..2ae4116e2 100644 --- a/c_emulator/riscv_platform_impl.h +++ b/c_emulator/riscv_platform_impl.h @@ -11,6 +11,9 @@ extern uint64_t rv_pmp_count; extern uint64_t rv_pmp_grain; +extern bool rv_misaligned_order_decreasing; +extern bool rv_misaligned_to_byte; + extern bool rv_enable_svinval; extern bool rv_enable_zcb; extern bool rv_enable_zfinx; diff --git a/c_emulator/riscv_sim.c b/c_emulator/riscv_sim.c index 3a9bfc08d..c275c85b2 100644 --- a/c_emulator/riscv_sim.c +++ b/c_emulator/riscv_sim.c @@ -54,6 +54,8 @@ const char *RV32ISA = "RV32IMAC"; #define OPT_PMP_COUNT 1002 #define OPT_PMP_GRAIN 1003 #define OPT_ENABLE_SVINVAL 1004 +#define OPT_MISALIGNED_ORDER_DEC 1005 +#define OPT_MISALIGNED_TO_BYTE 1006 #define OPT_ENABLE_ZCB 10014 static bool do_dump_dts = false; @@ -125,6 +127,8 @@ static struct option options[] = { {"enable-misaligned", no_argument, 0, 'm' }, {"pmp-count", required_argument, 0, OPT_PMP_COUNT }, {"pmp-grain", required_argument, 0, OPT_PMP_GRAIN }, + {"misaligned-order-decreasing", no_argument, 0, OPT_MISALIGNED_ORDER_DEC}, + {"misaligned-to-byte", no_argument, 0, OPT_MISALIGNED_TO_BYTE }, {"enable-next", no_argument, 0, 'N' }, {"ram-size", required_argument, 0, 'z' }, {"disable-compressed", no_argument, 0, 'C' }, @@ -308,6 +312,18 @@ static int process_args(int argc, char **argv) } rv_pmp_grain = pmp_grain; break; + case OPT_MISALIGNED_ORDER_DEC: + fprintf(stderr, + "misaligned access virtual addresses will be translated in " + "decreasing order.\n"); + rv_misaligned_order_decreasing = true; + break; + case OPT_MISALIGNED_TO_BYTE: + fprintf(stderr, + "misaligned accesses will be split into individual " + "byte operations.\n"); + rv_misaligned_to_byte = true; + break; case 'C': fprintf(stderr, "disabling RVC compressed instructions.\n"); rv_enable_rvc = false; diff --git a/model/prelude.sail b/model/prelude.sail index 028af2126..50c2ea857 100644 --- a/model/prelude.sail +++ b/model/prelude.sail @@ -10,6 +10,7 @@ default Order dec $include $include +$include $include $include $include "mapping.sail" diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail index 0f4da8372..2fcd282f1 100644 --- a/model/riscv_insts_aext.sail +++ b/model/riscv_insts_aext.sail @@ -40,6 +40,12 @@ function amo_width_valid(size : word_width) -> bool = { } } +val extend_value : forall 'n, 0 < 'n <= xlen_bytes. (bool, MemoryOpResult(bits(8 * 'n))) -> MemoryOpResult(xlenbits) +function extend_value(is_unsigned, value) = match (value) { + MemValue(v) => MemValue(if is_unsigned then zero_extend(v) else sign_extend(v) : xlenbits), + MemException(e) => MemException(e) +} + /* ****************************************************************** */ union clause ast = LOADRES : (bool, bool, regidx, word_width, regidx) diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail index 9c4630b33..97f7bef4a 100644 --- a/model/riscv_insts_base.sail +++ b/model/riscv_insts_base.sail @@ -297,55 +297,43 @@ union clause ast = LOAD : (bits(12), regidx, regidx, bool, word_width, bool, boo /* unsigned loads are only present for widths strictly less than xlen, signed loads also present for widths equal to xlen */ -mapping clause encdec = LOAD(imm, rs1, rd, is_unsigned, size, false, false) if (size_bytes(size) < sizeof(xlen_bytes)) | (not(is_unsigned) & size_bytes(size) <= sizeof(xlen_bytes)) - <-> imm @ rs1 @ bool_bits(is_unsigned) @ size_enc(size) @ rd @ 0b0000011 if (size_bytes(size) < sizeof(xlen_bytes)) | (not(is_unsigned) & size_bytes(size) <= sizeof(xlen_bytes)) +function valid_load_encdec(width : word_width, is_unsigned : bool) -> bool = + (size_bytes(width) < sizeof(xlen_bytes)) | (not(is_unsigned) & size_bytes(width) <= sizeof(xlen_bytes)) -val extend_value : forall 'n, 0 < 'n <= xlen_bytes. (bool, MemoryOpResult(bits(8 * 'n))) -> MemoryOpResult(xlenbits) -function extend_value(is_unsigned, value) = match (value) { - MemValue(v) => MemValue(if is_unsigned then zero_extend(v) else sign_extend(v) : xlenbits), - MemException(e) => MemException(e) -} - -val process_load : forall 'n, 0 < 'n <= xlen_bytes. (regidx, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> Retired -function process_load(rd, vaddr, value, is_unsigned) = - match extend_value(is_unsigned, value) { - MemValue(result) => { X(rd) = result; RETIRE_SUCCESS }, - MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL } - } - -function check_misaligned(vaddr : xlenbits, width : word_width) -> bool = - if plat_enable_misaligned_access() then false - else match width { - BYTE => false, - HALF => vaddr[0] == bitone, - WORD => vaddr[0] == bitone | vaddr[1] == bitone, - DOUBLE => vaddr[0] == bitone | vaddr[1] == bitone | vaddr[2] == bitone - } +mapping clause encdec = LOAD(imm, rs1, rd, is_unsigned, width, false, false) if valid_load_encdec(width, is_unsigned) + <-> imm @ rs1 @ bool_bits(is_unsigned) @ size_enc(width) @ rd @ 0b0000011 if valid_load_encdec(width, is_unsigned) function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = { let offset : xlenbits = sign_extend(imm); /* Get the address, X(rs1) + offset. Some extensions perform additional checks on address validity. */ match ext_data_get_addr(rs1, offset, Read(Data), width) { - Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, - Ext_DataAddr_OK(vaddr) => - if check_misaligned(vaddr, width) - then { handle_mem_exception(vaddr, E_Load_Addr_Align()); RETIRE_FAIL } - else match translateAddr(vaddr, Read(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, - TR_Address(paddr, _) => - match (width) { - BYTE => - process_load(rd, vaddr, mem_read(Read(Data), paddr, 1, aq, rl, false), is_unsigned), - HALF => - process_load(rd, vaddr, mem_read(Read(Data), paddr, 2, aq, rl, false), is_unsigned), - WORD => - process_load(rd, vaddr, mem_read(Read(Data), paddr, 4, aq, rl, false), is_unsigned), - DOUBLE if sizeof(xlen) >= 64 => - process_load(rd, vaddr, mem_read(Read(Data), paddr, 8, aq, rl, false), is_unsigned), - _ => report_invalid_width(__FILE__, __LINE__, width, "load") - } + Ext_DataAddr_Error(e) => { + ext_handle_data_check_error(e); + RETIRE_FAIL + }, + + Ext_DataAddr_OK(vaddr) => { + if check_misaligned(vaddr, width) then { + handle_mem_exception(vaddr, E_Load_Addr_Align()); + return RETIRE_FAIL + }; + + let bytes = size_bytes(width); + if bytes > sizeof(xlen_bytes) then { + report_invalid_width(__FILE__, __LINE__, width, "load") + } else match vmem_read(vaddr, bytes, aq, rl, false) { + Err(vaddr, e) => { + handle_mem_exception(vaddr, e); + RETIRE_FAIL + }, + + Ok(data) => { + X(rd) = if is_unsigned then zero_extend(data) else sign_extend(data); + RETIRE_SUCCESS + } } + } } } @@ -367,61 +355,47 @@ mapping maybe_u = { false <-> "" } -mapping clause assembly = LOAD(imm, rs1, rd, is_unsigned, size, aq, rl) - <-> "l" ^ size_mnemonic(size) ^ maybe_u(is_unsigned) ^ maybe_aq(aq) ^ maybe_rl(rl) ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_12(imm) ^ "(" ^ reg_name(rs1) ^ ")" +mapping clause assembly = LOAD(imm, rs1, rd, is_unsigned, width, aq, rl) + <-> "l" ^ size_mnemonic(width) ^ maybe_u(is_unsigned) ^ maybe_aq(aq) ^ maybe_rl(rl) ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_12(imm) ^ "(" ^ reg_name(rs1) ^ ")" /* ****************************************************************** */ union clause ast = STORE : (bits(12), regidx, regidx, word_width, bool, bool) -mapping clause encdec = STORE(imm7 @ imm5, rs2, rs1, size, false, false) if size_bytes(size) <= sizeof(xlen_bytes) - <-> imm7 : bits(7) @ rs2 @ rs1 @ 0b0 @ size_enc(size) @ imm5 : bits(5) @ 0b0100011 if size_bytes(size) <= sizeof(xlen_bytes) +mapping clause encdec = STORE(imm7 @ imm5, rs2, rs1, width, false, false) if size_bytes(width) <= sizeof(xlen_bytes) + <-> imm7 : bits(7) @ rs2 @ rs1 @ 0b0 @ size_enc(width) @ imm5 : bits(5) @ 0b0100011 if size_bytes(width) <= sizeof(xlen_bytes) -/* NOTE: Currently, we only EA if address translation is successful. - This may need revisiting. */ function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = { let offset : xlenbits = sign_extend(imm); /* Get the address, X(rs1) + offset. Some extensions perform additional checks on address validity. */ match ext_data_get_addr(rs1, offset, Write(Data), width) { - Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, - Ext_DataAddr_OK(vaddr) => - if check_misaligned(vaddr, width) - then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); RETIRE_FAIL } - else match translateAddr(vaddr, Write(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, - TR_Address(paddr, _) => { - let eares : MemoryOpResult(unit) = match width { - BYTE => mem_write_ea(paddr, 1, aq, rl, false), - HALF => mem_write_ea(paddr, 2, aq, rl, false), - WORD => mem_write_ea(paddr, 4, aq, rl, false), - DOUBLE => mem_write_ea(paddr, 8, aq, rl, false) - }; - match (eares) { - MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, - MemValue(_) => { - let rs2_val = X(rs2); - let res : MemoryOpResult(bool) = match (width) { - BYTE => mem_write_value(paddr, 1, rs2_val[7..0], aq, rl, false), - HALF => mem_write_value(paddr, 2, rs2_val[15..0], aq, rl, false), - WORD => mem_write_value(paddr, 4, rs2_val[31..0], aq, rl, false), - DOUBLE if sizeof(xlen) >= 64 - => mem_write_value(paddr, 8, rs2_val, aq, rl, false), - _ => report_invalid_width(__FILE__, __LINE__, width, "store"), - }; - match (res) { - MemValue(true) => RETIRE_SUCCESS, - MemValue(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"), - MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL } - } - } - } + Ext_DataAddr_Error(e) => { + ext_handle_data_check_error(e); + RETIRE_FAIL + }, + + Ext_DataAddr_OK(vaddr) => { + if check_misaligned(vaddr, width) then { + handle_mem_exception(vaddr, E_SAMO_Addr_Align()); + return RETIRE_FAIL + }; + + let bytes = size_bytes(width); + if bytes > sizeof(xlen_bytes) then { + report_invalid_width(__FILE__, __LINE__, width, "store") + } else match vmem_write_from_register(vaddr, bytes, unsigned(rs2), aq, rl, false) { + Ok() => RETIRE_SUCCESS, + Err(vaddr, e) => { + handle_mem_exception(vaddr, e); + return RETIRE_FAIL } } + } } } -mapping clause assembly = STORE(imm, rs2, rs1, size, aq, rl) - <-> "s" ^ size_mnemonic(size) ^ maybe_aq(aq) ^ maybe_rl(rl) ^ spc() ^ reg_name(rs2) ^ sep() ^ hex_bits_12(imm) ^ opt_spc() ^ "(" ^ opt_spc() ^ reg_name(rs1) ^ opt_spc() ^ ")" +mapping clause assembly = STORE(imm, rs2, rs1, width, aq, rl) + <-> "s" ^ size_mnemonic(width) ^ maybe_aq(aq) ^ maybe_rl(rl) ^ spc() ^ reg_name(rs2) ^ sep() ^ hex_bits_12(imm) ^ opt_spc() ^ "(" ^ opt_spc() ^ reg_name(rs1) ^ opt_spc() ^ ")" /* ****************************************************************** */ union clause ast = ADDIW : (bits(12), regidx, regidx) diff --git a/model/riscv_mem.sail b/model/riscv_mem.sail index ccf4d2fa9..881762a54 100644 --- a/model/riscv_mem.sail +++ b/model/riscv_mem.sail @@ -38,6 +38,14 @@ function is_aligned_addr forall 'n. (addr : xlenbits, width : int('n)) -> bool = unsigned(addr) % width == 0 +function check_misaligned(vaddr : xlenbits, width : word_width) -> bool = { + if plat_enable_misaligned_access() then { + false + } else { + not(is_aligned_addr(vaddr, size_bytes(width))) + } +} + function read_kind_of_flags (aq : bool, rl : bool, res : bool) -> option(read_kind) = match (aq, rl, res) { (false, false, false) => Some(Read_plain), diff --git a/model/riscv_vmem_utils.sail b/model/riscv_vmem_utils.sail new file mode 100644 index 000000000..8bbfc60ea --- /dev/null +++ b/model/riscv_vmem_utils.sail @@ -0,0 +1,131 @@ +/*=======================================================================================*/ +/* This Sail RISC-V architecture model, comprising all files and */ +/* directories except where otherwise noted is subject the BSD */ +/* two-clause license in the LICENSE file. */ +/* */ +/* SPDX-License-Identifier: BSD-2-Clause */ +/*=======================================================================================*/ + +/* This file implements utility functions for accessing memory that + * can be used by instruction definitions. + */ + +/* This is a external option that controls the order in which the model + * performs misaligned accesses. + */ +val sys_misaligned_order_decreasing = { + ocaml: "Platform.misaligned_order_decreasing", + _: "sys_misaligned_order_decreasing" +} : unit -> bool + +/* This is an external option that, when true, causes all misaligned accesses + * to be split into single byte operations. + */ +val sys_misaligned_to_byte = { + ocaml: "Platform.misaligned_to_byte", + _: "sys_misaligned_to_byte" +} : unit -> bool + +val split_misaligned : forall 'width, 'width in {1, 2, 4, 8}. + (xlenbits, int('width)) -> {'n 'bytes, 'width == 'n * 'bytes & 'bytes > 0. (int('n), int('bytes))} + +function split_misaligned(vaddr, width) = { + let misaligned_to_byte = sys_misaligned_to_byte(); + match width { + 1 => (1, 1), + + 2 if is_aligned_addr(vaddr, 2) => (1, 2), + 2 => (2, 1), + + 4 if is_aligned_addr(vaddr, 4) => (1, 4), + 4 if is_aligned_addr(vaddr, 2) & not(misaligned_to_byte) => (2, 2), + 4 => (4, 1), + + 8 if is_aligned_addr(vaddr, 8) => (1, 8), + 8 if is_aligned_addr(vaddr, 4) & not(misaligned_to_byte) => (2, 4), + 8 if is_aligned_addr(vaddr, 2) & not(misaligned_to_byte) => (4, 2), + 8 => (8, 1) + } +} + +type valid_misaligned_order('n, 'first, 'last, 'step) -> Bool = + ('first == 0 & 'last == 'n - 1 & 'step == 1) + | ('first == 'n - 1 & 'last == 0 & 'step == -1) + +val misaligned_order : forall 'n. + int('n) -> {'first 'last 'step, valid_misaligned_order('n, 'first, 'last, 'step). (int('first), int('last), int('step))} + +function misaligned_order(n) = { + if sys_misaligned_order_decreasing() then { + (0, n - 1, 1) + } else { + (n - 1, 0, -1) + } +} + +val vmem_read : forall 'width, 'width in {1, 2, 4, 8} & 'width <= xlen_bytes. + (xlenbits, int('width), bool, bool, bool) -> result(bits(8 * 'width), (xlenbits, ExceptionType)) + +function vmem_read(vaddr, bytes, aq, rl, res) = { + /* If the load is misaligned, split into `n` (single-copy-atomic) memory operations, + each of `bytes` width. If the load is aligned, then `n` = 1 and bytes will remain + unchanged. */ + let (n, bytes) = split_misaligned(vaddr, bytes); + var data = zeros(8 * n * bytes); + + let (first, last, step) = misaligned_order(n); + + foreach (i from first to last by step) { + let vaddr = vaddr + (i * bytes); + match translateAddr(vaddr, Read(Data)) { + TR_Failure(e, _) => return Err(vaddr, e), + + TR_Address(paddr, _) => match mem_read(Read(Data), paddr, bytes, aq, rl, res) { + MemException(e) => return Err(vaddr, e), + + MemValue(v) => { + data[(8 * (i + 1) * bytes) - 1 .. 8 * i * bytes] = v + }, + } + } + }; + + Ok(data) +} + +val vmem_write_from_register : forall 'width, 'width in {1, 2, 4, 8} & 'width <= xlen_bytes. + (xlenbits, int('width), range(0, 31), bool, bool, bool) -> result(unit, (xlenbits, ExceptionType)) + +function vmem_write_from_register(vaddr, bytes, reg, aq, rl, res) = { + /* If the store is misaligned, split into `n` (single-copy-atomic) memory operations, + each of `bytes` width. If the load is aligned, then `n` = 1 and bytes will remain + unchanged. */ + let (n, bytes) = split_misaligned(vaddr, bytes); + + let (first, last, step) = misaligned_order(n); + + foreach (i from first to last by step) { + let vaddr = vaddr + (i * bytes); + match translateAddr(vaddr, Write(Data)) { + TR_Failure(e, _) => return Err(vaddr, e), + + /* NOTE: Currently, we only announce the effective address if address translation is successful. + This may need revisiting. */ + TR_Address(paddr, _) => match mem_write_ea(paddr, bytes, aq, rl, false) { + MemException(e) => return Err(vaddr, e), + + MemValue(()) => { + let reg_val = X(reg); + match mem_write_value(paddr, bytes, reg_val[(8 * (i + 1) * bytes) - 1 .. 8 * i * bytes], aq, rl, false) { + MemException(e) => return Err(vaddr, e), + MemValue(true) => (), + MemValue(false) => + internal_error(__FILE__, __LINE__, "got false from mem_write_value"), + } + } + } + } + }; + + Ok() +} diff --git a/ocaml_emulator/platform.ml b/ocaml_emulator/platform.ml index 69f271496..a35ae666f 100644 --- a/ocaml_emulator/platform.ml +++ b/ocaml_emulator/platform.ml @@ -97,6 +97,9 @@ let enable_writable_fiom () = !config_enable_writable_fiom let pmp_count () = !config_pmp_count let pmp_grain () = !config_pmp_grain +let misaligned_to_byte () = false +let misaligned_order_decreasing () = false + let rom_base () = arch_bits_of_int64 P.rom_base let rom_size () = arch_bits_of_int !rom_size_ref