From e1663e985e2bc6c6311b6e81c296f6c4fd794e2d Mon Sep 17 00:00:00 2001 From: Mudassir Ali <140052763+Mudassir10X@users.noreply.github.com> Date: Mon, 3 Jun 2024 19:58:34 +0500 Subject: [PATCH 1/3] Use multiple threads for LTO This uses the Make job server so that multiple threads can be used for LTO, which speeds up the build. --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index ea6244a43..da4029633 100644 --- a/Makefile +++ b/Makefile @@ -185,7 +185,7 @@ ifneq (,$(COVERAGE)) C_FLAGS += --coverage -O1 SAIL_FLAGS += -Oconstant_fold else -C_FLAGS += -O3 -flto +C_FLAGS += -O3 -flto=auto endif ifneq (,$(SAILCOV)) From 9194dd51e58ee6767d4494a04fdddb4635c6bfdc Mon Sep 17 00:00:00 2001 From: Tim Hutt Date: Tue, 21 May 2024 14:48:25 +0100 Subject: [PATCH 2/3] Change ext_data_get_addr to use bytes for width Instead of `word_width` which can only be up to 8 bytes, just use bytes. This allows larger accesses (the limit is increased to 4096), e.g. for `cbo.zero`. --- model/prelude_mem.sail | 11 +++++++++-- model/riscv_addr_checks.sail | 2 +- model/riscv_insts_aext.sail | 6 +++--- model/riscv_insts_base.sail | 4 ++-- model/riscv_insts_fext.sail | 4 ++-- model/riscv_insts_vext_mem.sail | 26 +++++++++++++------------- 6 files changed, 30 insertions(+), 23 deletions(-) diff --git a/model/prelude_mem.sail b/model/prelude_mem.sail index 345e78c20..03ac69e29 100644 --- a/model/prelude_mem.sail +++ b/model/prelude_mem.sail @@ -80,8 +80,15 @@ instantiation sail_mem_write with because it means width argument can be fast native integer. It would be even better if it could be <= 8 bytes so that data can also be a 64-bit int but CHERI needs 128-bit accesses for - capabilities and SIMD / vector instructions will also need more. */ -type max_mem_access : Int = 16 + capabilities and SIMD / vector instructions will also need more. + + The specific value does not matter (if it is >8) since anything up + to 2^64-1 will result in a native int being used for the width type. + + 4096 was chosen because it is a page size, and a reasonable maximum + for cbo.zero. + */ +type max_mem_access : Int = 4096 val write_ram : forall 'n, 0 < 'n <= max_mem_access. (write_kind, xlenbits, int('n), bits(8 * 'n), mem_meta) -> bool diff --git a/model/riscv_addr_checks.sail b/model/riscv_addr_checks.sail index f9c783574..0d29d4ca4 100644 --- a/model/riscv_addr_checks.sail +++ b/model/riscv_addr_checks.sail @@ -54,7 +54,7 @@ type ext_data_addr_error = unit /* Default data addr is just base register + immediate offset (may be zero). Extensions might override and add additional checks. */ -function ext_data_get_addr(base : regidx, offset : xlenbits, acc : AccessType(ext_access_type), width : word_width) +function ext_data_get_addr(base : regidx, offset : xlenbits, acc : AccessType(ext_access_type), width : range(1, max_mem_access)) -> Ext_DataAddr_Check(ext_data_addr_error) = let addr = X(base) + offset in Ext_DataAddr_OK(addr) diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail index 2e0eb9c73..426499771 100644 --- a/model/riscv_insts_aext.sail +++ b/model/riscv_insts_aext.sail @@ -64,7 +64,7 @@ function clause execute(LOADRES(aq, rl, rs1, width, rd)) = { /* Get the address, X(rs1) (no offset). * Extensions might perform additional checks on address validity. */ - match ext_data_get_addr(rs1, zeros(), Read(Data), width) { + match ext_data_get_addr(rs1, zeros(), Read(Data), size_bytes(width)) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => { let aligned : bool = @@ -120,7 +120,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = { /* Get the address, X(rs1) (no offset). * Extensions might perform additional checks on address validity. */ - match ext_data_get_addr(rs1, zeros(), Write(Data), width) { + match ext_data_get_addr(rs1, zeros(), Write(Data), size_bytes(width)) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => { let aligned : bool = @@ -205,7 +205,7 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = { /* Get the address, X(rs1) (no offset). * Some extensions perform additional checks on address validity. */ - match ext_data_get_addr(rs1, zeros(), ReadWrite(Data, Data), width) { + match ext_data_get_addr(rs1, zeros(), ReadWrite(Data, Data), size_bytes(width)) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => { match translateAddr(vaddr, ReadWrite(Data, Data)) { diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail index 8d86804ed..c119ce934 100644 --- a/model/riscv_insts_base.sail +++ b/model/riscv_insts_base.sail @@ -326,7 +326,7 @@ 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) { + match ext_data_get_addr(rs1, offset, Read(Data), size_bytes(width)) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width) @@ -382,7 +382,7 @@ 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) { + match ext_data_get_addr(rs1, offset, Write(Data), size_bytes(width)) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width) diff --git a/model/riscv_insts_fext.sail b/model/riscv_insts_fext.sail index fcd4bb841..5c89e9188 100644 --- a/model/riscv_insts_fext.sail +++ b/model/riscv_insts_fext.sail @@ -315,7 +315,7 @@ function clause execute(LOAD_FP(imm, rs1, rd, width)) = { 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) { + match ext_data_get_addr(rs1, offset, Read(Data), size_bytes(width)) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width) @@ -381,7 +381,7 @@ function clause execute (STORE_FP(imm, rs2, rs1, width)) = { let (aq, rl, con) = (false, false, false); /* Get the address, X(rs1) + offset. Some extensions perform additional checks on address validity. */ - match ext_data_get_addr(rs1, offset, Write(Data), width) { + match ext_data_get_addr(rs1, offset, Write(Data), size_bytes(width)) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width) diff --git a/model/riscv_insts_vext_mem.sail b/model/riscv_insts_vext_mem.sail index ce9cd6237..4da82e18f 100644 --- a/model/riscv_insts_vext_mem.sail +++ b/model/riscv_insts_vext_mem.sail @@ -81,7 +81,7 @@ function process_vlseg (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) = vstart = to_bits(16, i); foreach (j from 0 to (nf - 1)) { let elem_offset = (i * nf + j) * load_width_bytes; - match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), width_type) { + match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), load_width_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width_type) @@ -149,7 +149,7 @@ function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) if vm_val[i] then { /* active segments */ foreach (j from 0 to (nf - 1)) { let elem_offset = (i * nf + j) * load_width_bytes; - match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), width_type) { + match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), load_width_bytes) { Ext_DataAddr_Error(e) => { if i == 0 then { ext_handle_data_check_error(e); return RETIRE_FAIL } else { @@ -251,7 +251,7 @@ function process_vsseg (nf, vm, vs3, load_width_bytes, rs1, EMUL_pow, num_elem) vstart = to_bits(16, i); foreach (j from 0 to (nf - 1)) { let elem_offset = (i * nf + j) * load_width_bytes; - match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), width_type) { + match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), load_width_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width_type) @@ -322,7 +322,7 @@ function process_vlsseg (nf, vm, vd, load_width_bytes, rs1, rs2, EMUL_pow, num_e vstart = to_bits(16, i); foreach (j from 0 to (nf - 1)) { let elem_offset = i * rs2_val + j * load_width_bytes; - match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), width_type) { + match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), load_width_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width_type) @@ -388,7 +388,7 @@ function process_vssseg (nf, vm, vs3, load_width_bytes, rs1, rs2, EMUL_pow, num_ vstart = to_bits(16, i); foreach (j from 0 to (nf - 1)) { let elem_offset = i * rs2_val + j * load_width_bytes; - match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), width_type) { + match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), load_width_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width_type) @@ -460,7 +460,7 @@ function process_vlxseg (nf, vm, vd, EEW_index_bytes, EEW_data_bytes, EMUL_index vstart = to_bits(16, i); foreach (j from 0 to (nf - 1)) { let elem_offset : int = signed(vs2_val[i]) + j * EEW_data_bytes; - match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), width_type) { + match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), EEW_data_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width_type) @@ -551,7 +551,7 @@ function process_vsxseg (nf, vm, vs3, EEW_index_bytes, EEW_data_bytes, EMUL_inde vstart = to_bits(16, i); foreach (j from 0 to (nf - 1)) { let elem_offset : int = signed(vs2_val[i]) + j * EEW_data_bytes; - match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), width_type) { + match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), EEW_data_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width_type) @@ -644,7 +644,7 @@ function process_vlre (nf, vd, load_width_bytes, rs1, elem_per_reg) = { foreach (i from elem_to_align to (elem_per_reg - 1)) { vstart = to_bits(16, cur_elem); let elem_offset = cur_elem * load_width_bytes; - match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), width_type) { + match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), load_width_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width_type) @@ -668,7 +668,7 @@ function process_vlre (nf, vd, load_width_bytes, rs1, elem_per_reg) = { foreach (i from 0 to (elem_per_reg - 1)) { vstart = to_bits(16, cur_elem); let elem_offset = cur_elem * load_width_bytes; - match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), width_type) { + match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), load_width_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width_type) @@ -726,7 +726,7 @@ function process_vsre (nf, load_width_bytes, rs1, vs3, elem_per_reg) = { foreach (i from elem_to_align to (elem_per_reg - 1)) { vstart = to_bits(16, cur_elem); let elem_offset : int = cur_elem * load_width_bytes; - match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), width_type) { + match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), load_width_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width_type) @@ -760,7 +760,7 @@ function process_vsre (nf, load_width_bytes, rs1, vs3, elem_per_reg) = { foreach (i from 0 to (elem_per_reg - 1)) { vstart = to_bits(16, cur_elem); let elem_offset = cur_elem * load_width_bytes; - match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), width_type) { + match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), load_width_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width_type) @@ -828,7 +828,7 @@ function process_vm(vd_or_vs3, rs1, num_elem, evl, op) = { if i < evl then { /* active elements */ vstart = to_bits(16, i); if op == VLM then { /* load */ - match ext_data_get_addr(rs1, to_bits(sizeof(xlen), i), Read(Data), width_type) { + match ext_data_get_addr(rs1, to_bits(sizeof(xlen), i), Read(Data), 1) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width_type) @@ -844,7 +844,7 @@ function process_vm(vd_or_vs3, rs1, num_elem, evl, op) = { } } } else if op == VSM then { /* store */ - match ext_data_get_addr(rs1, to_bits(sizeof(xlen), i), Write(Data), width_type) { + match ext_data_get_addr(rs1, to_bits(sizeof(xlen), i), Write(Data), 1) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width_type) From a6b656da4e8f90a0d0003e2f883ba37717f3ba37 Mon Sep 17 00:00:00 2001 From: Tim Hutt Date: Wed, 15 May 2024 17:08:43 +0100 Subject: [PATCH 3/3] Remove unnecessary matches for loads/stores Simplify the load/store code by removing the unnecessary matches on the access size. I have not done it for float loads/stores because that requires a separate change to make the float code generic over size. This also simplifies the AMO operation by not extending and truncating the values so many times, and removing the use of to_bits. --- model/riscv_insts_aext.sail | 148 ++++++++++-------------------------- model/riscv_insts_base.sail | 79 ++++++++----------- 2 files changed, 72 insertions(+), 155 deletions(-) diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail index 426499771..7a7e4927d 100644 --- a/model/riscv_insts_aext.sail +++ b/model/riscv_insts_aext.sail @@ -53,46 +53,31 @@ mapping clause encdec = LOADRES(aq, rl, rs1, size, rd) * call to load_reservation in LR and cancel_reservation in SC. */ -val process_loadres : forall 'n, 0 < 'n <= xlen_bytes. (regidx, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> Retired -function process_loadres(rd, addr, value, is_unsigned) = - match extend_value(is_unsigned, value) { - MemValue(result) => { load_reservation(addr); X(rd) = result; RETIRE_SUCCESS }, - MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL } - } - function clause execute(LOADRES(aq, rl, rs1, width, rd)) = { + let width_bytes = size_bytes(width); + + // This is checked during decoding. + assert(width_bytes <= sizeof(xlen_bytes)); + /* Get the address, X(rs1) (no offset). * Extensions might perform additional checks on address validity. */ - match ext_data_get_addr(rs1, zeros(), Read(Data), size_bytes(width)) { + match ext_data_get_addr(rs1, zeros(), Read(Data), width_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => { - let aligned : bool = - /* BYTE and HALF would only occur due to invalid decodes, but it doesn't hurt - * to treat them as valid here; otherwise we'd need to throw an internal_error. - */ - match width { - BYTE => true, - HALF => vaddr[0..0] == 0b0, - WORD => vaddr[1..0] == 0b00, - DOUBLE => vaddr[2..0] == 0b000 - }; /* "LR faults like a normal load, even though it's in the AMO major opcode space." * - Andrew Waterman, isa-dev, 10 Jul 2018. */ - if not(aligned) + if not(is_aligned(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(addr, _) => - match (width, sizeof(xlen)) { - (BYTE, _) => process_loadres(rd, vaddr, mem_read(Read(Data), addr, 1, aq, aq & rl, true), false), - (HALF, _) => process_loadres(rd, vaddr, mem_read(Read(Data), addr, 2, aq, aq & rl, true), false), - (WORD, _) => process_loadres(rd, vaddr, mem_read(Read(Data), addr, 4, aq, aq & rl, true), false), - (DOUBLE, 64) => process_loadres(rd, vaddr, mem_read(Read(Data), addr, 8, aq, aq & rl, true), false), - _ => internal_error(__FILE__, __LINE__, "Unexpected AMO width") - } - } + TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + TR_Address(addr, _) => + match mem_read(Read(Data), addr, width_bytes, aq, aq & rl, true) { + MemValue(result) => { load_reservation(vaddr); X(rd) = sign_extend(result); RETIRE_SUCCESS }, + MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL } + }, + } } } } @@ -108,6 +93,11 @@ mapping clause encdec = STORECON(aq, rl, rs2, rs1, size, rd) /* NOTE: Currently, we only EA if address translation is successful. This may need revisiting. */ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = { + let width_bytes = size_bytes(width); + + // This is checked during decoding. + assert(width_bytes <= sizeof(xlen_bytes)); + if speculate_conditional () == false then { /* should only happen in rmem * rmem: allow SC to fail very early @@ -120,20 +110,10 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = { /* Get the address, X(rs1) (no offset). * Extensions might perform additional checks on address validity. */ - match ext_data_get_addr(rs1, zeros(), Write(Data), size_bytes(width)) { + match ext_data_get_addr(rs1, zeros(), Write(Data), width_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => { - let aligned : bool = - /* BYTE and HALF would only occur due to invalid decodes, but it doesn't hurt - * to treat them as valid here; otherwise we'd need to throw an internal_error. - */ - match width { - BYTE => true, - HALF => vaddr[0..0] == 0b0, - WORD => vaddr[1..0] == 0b00, - DOUBLE => vaddr[2..0] == 0b000 - }; - if not(aligned) + if not(is_aligned(vaddr, width)) then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); RETIRE_FAIL } else { if match_reservation(vaddr) == false then { @@ -144,25 +124,12 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = { * both result in a SAMO exception */ TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, TR_Address(addr, _) => { - let eares : MemoryOpResult(unit) = match (width, sizeof(xlen)) { - (BYTE, _) => mem_write_ea(addr, 1, aq & rl, rl, true), - (HALF, _) => mem_write_ea(addr, 2, aq & rl, rl, true), - (WORD, _) => mem_write_ea(addr, 4, aq & rl, rl, true), - (DOUBLE, 64) => mem_write_ea(addr, 8, aq & rl, rl, true), - _ => internal_error(__FILE__, __LINE__, "STORECON expected word or double") - }; + let eares = mem_write_ea(addr, width_bytes, aq & rl, rl, true); match (eares) { MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, MemValue(_) => { - rs2_val = X(rs2); - let res : MemoryOpResult(bool) = match (width, sizeof(xlen)) { - (BYTE, _) => mem_write_value(addr, 1, rs2_val[7..0], aq & rl, rl, true), - (HALF, _) => mem_write_value(addr, 2, rs2_val[15..0], aq & rl, rl, true), - (WORD, _) => mem_write_value(addr, 4, rs2_val[31..0], aq & rl, rl, true), - (DOUBLE, 64) => mem_write_value(addr, 8, rs2_val, aq & rl, rl, true), - _ => internal_error(__FILE__, __LINE__, "STORECON expected word or double") - }; - match (res) { + let rs2_val = X(rs2); + match mem_write_value(addr, width_bytes, rs2_val[width_bytes * 8 - 1 .. 0], aq & rl, rl, true) { MemValue(true) => { X(rd) = zero_extend(0b0); cancel_reservation(); RETIRE_SUCCESS }, MemValue(false) => { X(rd) = zero_extend(0b1); cancel_reservation(); RETIRE_SUCCESS }, MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL } @@ -202,77 +169,42 @@ mapping clause encdec = AMO(op, aq, rl, rs2, rs1, size, rd) /* NOTE: Currently, we only EA if address translation is successful. This may need revisiting. */ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = { + let 'width_bytes = size_bytes(width); + + // This is checked during decoding. + assert(width_bytes <= sizeof(xlen_bytes)); + /* Get the address, X(rs1) (no offset). * Some extensions perform additional checks on address validity. */ - match ext_data_get_addr(rs1, zeros(), ReadWrite(Data, Data), size_bytes(width)) { + match ext_data_get_addr(rs1, zeros(), ReadWrite(Data, Data), width_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => { match translateAddr(vaddr, ReadWrite(Data, Data)) { TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, TR_Address(addr, _) => { - let eares : MemoryOpResult(unit) = match (width, sizeof(xlen)) { - (BYTE, _) => mem_write_ea(addr, 1, aq & rl, rl, true), - (HALF, _) => mem_write_ea(addr, 2, aq & rl, rl, true), - (WORD, _) => mem_write_ea(addr, 4, aq & rl, rl, true), - (DOUBLE, 64) => mem_write_ea(addr, 8, aq & rl, rl, true), - _ => internal_error(__FILE__, __LINE__, "Unexpected AMO width") - }; - let is_unsigned : bool = match op { - AMOMINU => true, - AMOMAXU => true, - _ => false - }; - let rs2_val : xlenbits = match width { - BYTE => if is_unsigned then zero_extend(X(rs2)[7..0]) else sign_extend(X(rs2)[7..0]), - HALF => if is_unsigned then zero_extend(X(rs2)[15..0]) else sign_extend(X(rs2)[15..0]), - WORD => if is_unsigned then zero_extend(X(rs2)[31..0]) else sign_extend(X(rs2)[31..0]), - DOUBLE => X(rs2) - }; + let eares = mem_write_ea(addr, width_bytes, aq & rl, rl, true); + let rs2_val = X(rs2)[width_bytes * 8 - 1 .. 0]; match (eares) { MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, MemValue(_) => { - let mval : MemoryOpResult(xlenbits) = match (width, sizeof(xlen)) { - (BYTE, _) => extend_value(is_unsigned, mem_read(ReadWrite(Data, Data), addr, 1, aq, aq & rl, true)), - (HALF, _) => extend_value(is_unsigned, mem_read(ReadWrite(Data, Data), addr, 2, aq, aq & rl, true)), - (WORD, _) => extend_value(is_unsigned, mem_read(ReadWrite(Data, Data), addr, 4, aq, aq & rl, true)), - (DOUBLE, 64) => extend_value(is_unsigned, mem_read(ReadWrite(Data, Data), addr, 8, aq, aq & rl, true)), - _ => internal_error(__FILE__, __LINE__, "Unexpected AMO width") - }; - match (mval) { + match mem_read(ReadWrite(Data, Data), addr, width_bytes, aq, aq & rl, true) { MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, MemValue(loaded) => { - let result : xlenbits = + let result : bits('width_bytes * 8) = match op { AMOSWAP => rs2_val, AMOADD => rs2_val + loaded, AMOXOR => rs2_val ^ loaded, AMOAND => rs2_val & loaded, AMOOR => rs2_val | loaded, - - /* These operations convert bitvectors to integer values using [un]signed, - * and back using to_bits(). - */ - AMOMIN => to_bits(sizeof(xlen), min(signed(rs2_val), signed(loaded))), - AMOMAX => to_bits(sizeof(xlen), max(signed(rs2_val), signed(loaded))), - AMOMINU => to_bits(sizeof(xlen), min(unsigned(rs2_val), unsigned(loaded))), - AMOMAXU => to_bits(sizeof(xlen), max(unsigned(rs2_val), unsigned(loaded))) + AMOMIN => if rs2_val <_s loaded then rs2_val else loaded, + AMOMAX => if rs2_val >_s loaded then rs2_val else loaded, + AMOMINU => if rs2_val <_u loaded then rs2_val else loaded, + AMOMAXU => if rs2_val >_u loaded then rs2_val else loaded, }; - let rval : xlenbits = match width { - BYTE => sign_extend(loaded[7..0]), - HALF => sign_extend(loaded[15..0]), - WORD => sign_extend(loaded[31..0]), - DOUBLE => loaded - }; - let wval : MemoryOpResult(bool) = match (width, sizeof(xlen)) { - (BYTE, _) => mem_write_value(addr, 1, result[7..0], aq & rl, rl, true), - (HALF, _) => mem_write_value(addr, 2, result[15..0], aq & rl, rl, true), - (WORD, _) => mem_write_value(addr, 4, result[31..0], aq & rl, rl, true), - (DOUBLE, 64) => mem_write_value(addr, 8, result, aq & rl, rl, true), - _ => internal_error(__FILE__, __LINE__, "Unexpected AMO width") - }; - match (wval) { - MemValue(true) => { X(rd) = rval; RETIRE_SUCCESS }, + match mem_write_value(addr, width_bytes, sign_extend(result), aq & rl, rl, true) { + MemValue(true) => { X(rd) = sign_extend(loaded); RETIRE_SUCCESS }, MemValue(false) => { internal_error(__FILE__, __LINE__, "AMO got false from mem_write_value") }, MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL } } diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail index c119ce934..26915f22c 100644 --- a/model/riscv_insts_base.sail +++ b/model/riscv_insts_base.sail @@ -300,52 +300,45 @@ union clause ast = LOAD : (bits(12), regidx, regidx, bool, word_width, bool, boo 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)) -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 } +val extend_value : forall 'n, 0 < 'n <= xlen. (bool, bits('n)) -> xlenbits +function extend_value(is_unsigned, value) = if is_unsigned then zero_extend(value) else sign_extend(value) + +function is_aligned(vaddr : xlenbits, width : word_width) -> bool = + match width { + BYTE => true, + HALF => vaddr[0..0] == zeros(), + WORD => vaddr[1..0] == zeros(), + DOUBLE => vaddr[2..0] == zeros(), } +// Return true if the address is misaligned and we don't support misaligned access. 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 - } + not(plat_enable_misaligned_access()) & not(is_aligned(vaddr, width)) function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = { let offset : xlenbits = sign_extend(imm); + let width_bytes = size_bytes(width); + + // This is checked during decoding. + assert(width_bytes <= sizeof(xlen_bytes)); + /* Get the address, X(rs1) + offset. Some extensions perform additional checks on address validity. */ - match ext_data_get_addr(rs1, offset, Read(Data), size_bytes(width)) { + match ext_data_get_addr(rs1, offset, Read(Data), width_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, - Ext_DataAddr_OK(vaddr) => + 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") - } + + match mem_read(Read(Data), paddr, width_bytes, aq, rl, false) { + MemValue(result) => { X(rd) = extend_value(is_unsigned, result); RETIRE_SUCCESS }, + MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + }, } + }, } } @@ -380,9 +373,14 @@ mapping clause encdec = STORE(imm7 @ imm5, rs2, rs1, size, false, false) This may need revisiting. */ function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = { let offset : xlenbits = sign_extend(imm); + let width_bytes = size_bytes(width); + + // This is checked during decoding. + assert(width_bytes <= sizeof(xlen_bytes)); + /* Get the address, X(rs1) + offset. Some extensions perform additional checks on address validity. */ - match ext_data_get_addr(rs1, offset, Write(Data), size_bytes(width)) { + match ext_data_get_addr(rs1, offset, Write(Data), width_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width) @@ -390,25 +388,12 @@ function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = { 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) - }; + let eares = mem_write_ea(paddr, width_bytes, 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) { + match mem_write_value(paddr, width_bytes, rs2_val[width_bytes * 8 - 1 .. 0], aq, rl, false) { 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 }