diff --git a/model/riscv_addr_checks.sail b/model/riscv_addr_checks.sail index f9c783574..48b390999 100644 --- a/model/riscv_addr_checks.sail +++ b/model/riscv_addr_checks.sail @@ -59,6 +59,13 @@ function ext_data_get_addr(base : regidx, offset : xlenbits, acc : AccessType(ex let addr = X(base) + offset in Ext_DataAddr_OK(addr) +/* Default AMO data addr is just base register. + Extensions might override and add additional checks. */ +function ext_data_get_amo_addr(base : regidx, acc : AccessType(ext_access_type), width : amo_word_width) + -> Ext_DataAddr_Check(ext_data_addr_error) = + let addr = X(base) in + Ext_DataAddr_OK(addr) + function ext_handle_data_check_error(err : ext_data_addr_error) -> unit = () diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail index 0f4da8372..a55565064 100644 --- a/model/riscv_insts_aext.sail +++ b/model/riscv_insts_aext.sail @@ -32,7 +32,7 @@ function lrsc_width_str(width : word_width) -> string = * RISC-V only appears to define LR / SC / AMOs for word and double, although * there seem to be encodings reserved for other widths. */ -function amo_width_valid(size : word_width) -> bool = { +function lrsc_width_valid(size : word_width) -> bool = { match(size) { WORD => true, DOUBLE => sizeof(xlen) >= 64, @@ -43,9 +43,8 @@ function amo_width_valid(size : word_width) -> bool = { /* ****************************************************************** */ union clause ast = LOADRES : (bool, bool, regidx, word_width, regidx) -mapping clause encdec = LOADRES(aq, rl, rs1, size, rd) if amo_width_valid(size) - <-> 0b00010 @ bool_bits(aq) @ bool_bits(rl) @ 0b00000 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if amo_width_valid(size) - +mapping clause encdec = LOADRES(aq, rl, rs1, size, rd) if lrsc_width_valid(size) + <-> 0b00010 @ bool_bits(aq) @ bool_bits(rl) @ 0b00000 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if lrsc_width_valid(size) /* We could set load-reservations on physical or virtual addresses. * For now we set them on virtual addresses, since it makes the @@ -108,8 +107,8 @@ mapping clause assembly = LOADRES(aq, rl, rs1, size, rd) /* ****************************************************************** */ union clause ast = STORECON : (bool, bool, regidx, regidx, word_width, regidx) -mapping clause encdec = STORECON(aq, rl, rs2, rs1, size, rd) if amo_width_valid(size) - <-> 0b00011 @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if amo_width_valid(size) +mapping clause encdec = STORECON(aq, rl, rs2, rs1, size, rd) if lrsc_width_valid(size) + <-> 0b00011 @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if lrsc_width_valid(size) /* NOTE: Currently, we only EA if address translation is successful. This may need revisiting. */ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = { @@ -192,7 +191,7 @@ mapping clause assembly = STORECON(aq, rl, rs2, rs1, size, rd) <-> "sc." ^ size_mnemonic(size) ^ maybe_aq(aq) ^ maybe_rl(rl) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs2) ^ sep() ^ "(" ^ reg_name(rs1) ^ ")" /* ****************************************************************** */ -union clause ast = AMO : (amoop, bool, bool, regidx, regidx, word_width, regidx) +union clause ast = AMO : (amoop, bool, bool, regidx, regidx, amo_word_width, regidx) mapping encdec_amoop : amoop <-> bits(5) = { AMOSWAP <-> 0b00001, @@ -203,11 +202,33 @@ mapping encdec_amoop : amoop <-> bits(5) = { AMOMIN <-> 0b10000, AMOMAX <-> 0b10100, AMOMINU <-> 0b11000, - AMOMAXU <-> 0b11100 + AMOMAXU <-> 0b11100, + AMOCAS <-> 0b00101 +} + +/** + * RISC-V only appears to define AMO for word and double, although + * there seem to be encodings reserved for other widths. + * zacas: amocas.d supported for RV32 and amocas.q for RV64 + * amocas that operate on 2*XLEN data requires the first register + * of the register pair to be even numbered. RV32 supports amocas.d. + */ +function amo_encoding_valid(size : amo_word_width, op : amoop, rs2 : regidx, rd : regidx ) -> bool = { + match(size, sizeof(xlen), op) { + (AMO_WORD, 32, AMOCAS) => haveZacas(), + (AMO_WORD, 64, AMOCAS) => haveZacas(), + (AMO_WORD, _, _) => true, + (AMO_DOUBLE, 32, AMOCAS) => if rs2[0..0] != 0b0 | rd[0..0] != 0b0 then false else haveZacas(), + (AMO_DOUBLE, 64, AMOCAS) => haveZacas(), + (AMO_DOUBLE, _, _) => sizeof(xlen) >= 64, + (AMO_QUAD, 64, AMOCAS) => if rs2[0..0] != 0b0 | rd[0..0] != 0b0 then false else haveZacas(), + (AMO_QUAD, _, _) => false, + _ => false + } } -mapping clause encdec = AMO(op, aq, rl, rs2, rs1, size, rd) if amo_width_valid(size) - <-> encdec_amoop(op) @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if amo_width_valid(size) +mapping clause encdec = AMO(op, aq, rl, rs2, rs1, size, rd) if amo_encoding_valid(size, op, rs2, rd) + <-> encdec_amoop(op) @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ amo_size_enc(size) @ rd @ 0b0101111 if amo_encoding_valid(size, op, rs2, rd) /* NOTE: Currently, we only EA if address translation is successful. This may need revisiting. */ @@ -216,17 +237,18 @@ 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_amo_addr(rs1, ReadWrite(Data, Data), width) { 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), + (AMO_BYTE, _) => mem_write_ea(addr, 1, aq & rl, rl, true), + (AMO_HALF, _) => mem_write_ea(addr, 2, aq & rl, rl, true), + (AMO_WORD, _) => mem_write_ea(addr, 4, aq & rl, rl, true), + (AMO_DOUBLE, _) => mem_write_ea(addr, 8, aq & rl, rl, true), + (AMO_QUAD, 64) => mem_write_ea(addr, 16, aq & rl, rl, true), _ => internal_error(__FILE__, __LINE__, "Unexpected AMO width") }; let is_unsigned : bool = match op { @@ -234,58 +256,136 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = { AMOMAXU => true, _ => false }; + let rd_val : xlenbits = match width { + AMO_BYTE => if is_unsigned then zero_extend(X(rd)[7..0]) else sign_extend(X(rd)[7..0]), + AMO_HALF => if is_unsigned then zero_extend(X(rd)[15..0]) else sign_extend(X(rd)[15..0]), + AMO_WORD => if is_unsigned then zero_extend(X(rd)[31..0]) else sign_extend(X(rd)[31..0]), + AMO_DOUBLE => X(rd), + AMO_QUAD => X(rd) + }; 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) + AMO_BYTE => if is_unsigned then zero_extend(X(rs2)[7..0]) else sign_extend(X(rs2)[7..0]), + AMO_HALF => if is_unsigned then zero_extend(X(rs2)[15..0]) else sign_extend(X(rs2)[15..0]), + AMO_WORD => if is_unsigned then zero_extend(X(rs2)[31..0]) else sign_extend(X(rs2)[31..0]), + AMO_DOUBLE => X(rs2), + AMO_QUAD => X(rs2) + }; + /* AMOCAS.W for RV32 and AMOCAS.Q for RV64 operate on a pair of + * register. When the first register of a source register pair is + * x0, then both halves of the pair read as zero. + */ + let rd_plus_one : regidx = + match (width, sizeof(xlen), op) { + (AMO_DOUBLE, 32, AMOCAS) => if (rd != zreg) then (rd + 1) else zeros(), + (AMO_QUAD, 64, AMOCAS) => if (rd != zreg) then (rd + 1) else zeros(), + _ => zeros() + }; + let rs2_plus_one : regidx = + match (width, sizeof(xlen), op) { + (AMO_DOUBLE, 32, AMOCAS) => if (rs2 != zreg) then (rs2 + 1) else zeros(), + (AMO_QUAD, 64, AMOCAS) => if (rs2 != zreg) then (rs2 + 1) else zeros(), + _ => zeros() + }; + let rd_plus_one_val : xlenbits = zero_extend(X(rd_plus_one)); + let rs2_plus_one_val : xlenbits = zero_extend(X(rs2_plus_one)); + /* AMOCAS has release semantics only if AMOCAS is successful */ + let amo_rd_rl : bool = match op { + AMOCAS => false, + _ => aq & rl }; 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)), + (AMO_BYTE, _) => extend_value(is_unsigned, mem_read(ReadWrite(Data, Data), addr, 1, aq, amo_rd_rl, true)), + (AMO_HALF, _) => extend_value(is_unsigned, mem_read(ReadWrite(Data, Data), addr, 2, aq, amo_rd_rl, true)), + (AMO_WORD, _) => extend_value(is_unsigned, mem_read(ReadWrite(Data, Data), addr, 4, aq, amo_rd_rl, true)), + (AMO_DOUBLE, 64) => extend_value(is_unsigned, mem_read(ReadWrite(Data, Data), addr, 8, aq, amo_rd_rl, true)), + (AMO_DOUBLE, 32) => extend_value(is_unsigned, mem_read(ReadWrite(Data, Data), addr, 4, aq, amo_rd_rl, true)), + (AMO_QUAD, 64) => extend_value(is_unsigned, mem_read(ReadWrite(Data, Data), addr, 8, aq, amo_rd_rl, true)), _ => internal_error(__FILE__, __LINE__, "Unexpected AMO width") }; + let mval_high : MemoryOpResult(xlenbits) = match (width, sizeof(xlen)) { + (AMO_DOUBLE, 32) => extend_value(is_unsigned, mem_read(ReadWrite(Data, Data), addr+4, 4, aq, amo_rd_rl, true)), + (AMO_QUAD, 64) => extend_value(is_unsigned, mem_read(ReadWrite(Data, Data), addr+8, 8, aq, amo_rd_rl, true)), + _ => MemValue(zeros()) + }; match (mval) { MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, MemValue(loaded) => { - let result : xlenbits = - match op { - AMOSWAP => rs2_val, - AMOADD => rs2_val + loaded, - AMOXOR => rs2_val ^ loaded, - AMOAND => rs2_val & loaded, - AMOOR => rs2_val | loaded, + match (mval_high) { + MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL }, + MemValue(loaded_high) => { + let result : xlenbits = + match op { + AMOSWAP => rs2_val, + AMOADD => rs2_val + loaded, + AMOXOR => rs2_val ^ loaded, + AMOAND => rs2_val & loaded, + AMOOR => rs2_val | loaded, + AMOCAS => rs2_val, - /* 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))) - }; - 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 }, - MemValue(false) => { internal_error(__FILE__, __LINE__, "AMO got false from mem_write_value") }, - MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL } + /* 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))) + }; + let result_high : xlenbits = + match op { + AMOCAS => rs2_plus_one_val, + _ => zeros(), + }; + let amo_does_write : bool = + match (op, sizeof(xlen), width) { + (AMOCAS, 32, AMO_WORD) => if ( loaded == rd_val ) then true else false, + (AMOCAS, 32, AMO_DOUBLE) => if ( loaded == rd_val & loaded_high == rd_plus_one_val ) then true else false, + (AMOCAS, 64, AMO_WORD) => if ( loaded == rd_val ) then true else false, + (AMOCAS, 64, AMO_DOUBLE) => if ( loaded == rd_val ) then true else false, + (AMOCAS, 64, AMO_QUAD) => if ( loaded == rd_val & loaded_high == rd_plus_one_val ) then true else false, + (_, _, _) => true + }; + let rval : xlenbits = match width { + AMO_BYTE => sign_extend(loaded[7..0]), + AMO_HALF => sign_extend(loaded[15..0]), + AMO_WORD => sign_extend(loaded[31..0]), + AMO_DOUBLE => loaded, + AMO_QUAD => loaded + }; + let rval_high : xlenbits = match width { + AMO_DOUBLE => loaded_high, + AMO_QUAD => loaded_high, + _ => zeros() + }; + let wval : MemoryOpResult(bool) = match (width, sizeof(xlen), amo_does_write) { + (AMO_BYTE, _, true) => mem_write_value(addr, 1, result[7..0], aq & rl, rl, true), + (AMO_HALF, _, true) => mem_write_value(addr, 2, result[15..0], aq & rl, rl, true), + (AMO_WORD, _, true) => mem_write_value(addr, 4, result[31..0], aq & rl, rl, true), + (AMO_DOUBLE, 32, true) => mem_write_value(addr, 4, result, aq & rl, rl, true), + (AMO_DOUBLE, 64, true) => mem_write_value(addr, 8, result, aq & rl, rl, true), + (AMO_QUAD, 64, true) => mem_write_value(addr, 8, result, aq & rl, rl, true), + _ => MemValue(true) + }; + match (wval) { + MemValue(true) => { + let wval_high : MemoryOpResult(bool) = + match (width, sizeof(xlen), amo_does_write) { + (AMO_DOUBLE, 32, true) => mem_write_value(addr+4, 4, result_high, aq & rl, rl, true), + (AMO_QUAD, 64, true) => mem_write_value(addr+8, 8, result_high, aq & rl, rl, true), + _ => MemValue(true) + }; + match (wval_high) { + MemValue(true) => { X(rd) = rval; X(rd_plus_one) = rval_high; RETIRE_SUCCESS}, + MemValue(false) => { internal_error(__FILE__, __LINE__, "AMO got false from mem_write_value") }, + MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL } + } + }, + MemValue(false) => { internal_error(__FILE__, __LINE__, "AMO got false from mem_write_value") }, + MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL } + } + } } } } @@ -310,8 +410,9 @@ mapping amo_mnemonic : amoop <-> string = { AMOMIN <-> "amomin", AMOMAX <-> "amomax", AMOMINU <-> "amominu", - AMOMAXU <-> "amomaxu" + AMOMAXU <-> "amomaxu", + AMOCAS <-> "amocas" } mapping clause assembly = AMO(op, aq, rl, rs2, rs1, width, rd) - <-> amo_mnemonic(op) ^ "." ^ size_mnemonic(width) ^ maybe_aq(aq) ^ maybe_rl(rl) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs2) ^ sep() ^ "(" ^ reg_name(rs1) ^ ")" + <-> amo_mnemonic(op) ^ "." ^ amo_size_mnemonic(width) ^ maybe_aq(aq) ^ maybe_rl(rl) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs2) ^ sep() ^ "(" ^ reg_name(rs1) ^ ")" diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 3e730202b..fa16ad611 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -160,6 +160,9 @@ function haveZmmul() -> bool = true /* Zicond extension support */ function haveZicond() -> bool = true +/* Zacas extension support. */ +function haveZacas() -> bool = true + bitfield Mstatush : bits(32) = { MBE : 5, SBE : 4 diff --git a/model/riscv_types.sail b/model/riscv_types.sail index e9a5a1990..b312095ba 100644 --- a/model/riscv_types.sail +++ b/model/riscv_types.sail @@ -333,7 +333,7 @@ enum ropw = {RISCV_ADDW, RISCV_SUBW, RISCV_SLLW, enum sopw = {RISCV_SLLIW, RISCV_SRLIW, RISCV_SRAIW} /* RV64-only shift ops */ enum amoop = {AMOSWAP, AMOADD, AMOXOR, AMOAND, AMOOR, - AMOMIN, AMOMAX, AMOMINU, AMOMAXU} /* AMO ops */ + AMOMIN, AMOMAX, AMOMINU, AMOMAXU, AMOCAS} /* AMO ops */ enum csrop = {CSRRW, CSRRS, CSRRC} /* CSR ops */ enum brop_zba = {RISCV_SH1ADD, RISCV_SH2ADD, RISCV_SH3ADD} @@ -389,6 +389,33 @@ mapping size_bytes : word_width <-> {1, 2, 4, 8} = { DOUBLE <-> 8, } +enum amo_word_width = {AMO_BYTE, AMO_HALF, AMO_WORD, AMO_DOUBLE, AMO_QUAD} + +mapping amo_size_enc : amo_word_width <-> bits(3) = { + AMO_BYTE <-> 0b000, + AMO_HALF <-> 0b001, + AMO_WORD <-> 0b010, + AMO_DOUBLE <-> 0b011, + AMO_QUAD <-> 0b100, +} + +mapping amo_size_mnemonic : amo_word_width <-> string = { + AMO_BYTE <-> "b", + AMO_HALF <-> "h", + AMO_WORD <-> "w", + AMO_DOUBLE <-> "d", + AMO_QUAD <-> "q", +} + +val amo_word_width_bytes : amo_word_width -> {'s, 's == 1 | 's == 2 | 's == 4 | 's == 8 | 's == 16 . atom('s)} +function amo_word_width_bytes width = match width { + AMO_BYTE => 1, + AMO_HALF => 2, + AMO_WORD => 4, + AMO_DOUBLE => 8, + AMO_QUAD => 16 +} + /*! * Raise an internal error reporting that width w is invalid for access kind, k, * and current xlen. The file name and line number should be passed in as the