diff options
author | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2019-04-24 17:56:32 -0700 |
---|---|---|
committer | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2019-04-24 17:58:26 -0700 |
commit | 3442aba5aa6545e76e066a199be45809784d495a (patch) | |
tree | 902e43defc518f9ec7004e288ab1c23165f60d88 /model/riscv_insts_aext.sail | |
parent | ca5788f07ad099c3891a193d4d3d95ea71863961 (diff) | |
download | sail-riscv-3442aba5aa6545e76e066a199be45809784d495a.zip sail-riscv-3442aba5aa6545e76e066a199be45809784d495a.tar.gz sail-riscv-3442aba5aa6545e76e066a199be45809784d495a.tar.bz2 |
Add extended model from cheri-merge.
Diffstat (limited to 'model/riscv_insts_aext.sail')
-rw-r--r-- | model/riscv_insts_aext.sail | 228 |
1 files changed, 123 insertions, 105 deletions
diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail index 7042583..f38b28f 100644 --- a/model/riscv_insts_aext.sail +++ b/model/riscv_insts_aext.sail @@ -41,31 +41,37 @@ function process_loadres(rd, addr, value, is_unsigned) = function clause execute(LOADRES(aq, rl, rs1, width, rd)) = { if haveAtomics() then { - let vaddr : xlenbits = X(rs1); - 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] == 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 (~ (aligned)) - then { handle_mem_exception(vaddr, E_Load_Addr_Align); false } - else match translateAddr(vaddr, Read, Data) { - TR_Failure(e) => { handle_mem_exception(vaddr, e); false }, - TR_Address(addr) => - match (width, sizeof(xlen)) { - (WORD, _) => process_loadres(rd, vaddr, mem_read(addr, 4, aq, rl, true), false), - (DOUBLE, 64) => process_loadres(rd, vaddr, mem_read(addr, 8, aq, rl, true), false), - _ => internal_error("LOADRES expected WORD or DOUBLE") + let pre_vaddr : xlenbits = X(rs1); + /* Let extensions get the first check on address validity. */ + match ext_data_check_addr(pre_vaddr, Read, Data, width) { + Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); false }, + 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] == 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 (~ (aligned)) + then { handle_mem_exception(vaddr, E_Load_Addr_Align); false } + else match translateAddr(vaddr, Read, Data) { + TR_Failure(e) => { handle_mem_exception(vaddr, e); false }, + TR_Address(addr) => + match (width, sizeof(xlen)) { + (WORD, _) => process_loadres(rd, vaddr, mem_read(addr, 4, aq, rl, true), false), + (DOUBLE, 64) => process_loadres(rd, vaddr, mem_read(addr, 8, aq, rl, true), false), + _ => internal_error("LOADRES expected WORD or DOUBLE") + } } - } + } + } } else { handle_illegal(); false @@ -93,45 +99,51 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = { /* normal non-rmem case * rmem: SC is allowed to succeed (but might fail later) */ - vaddr : xlenbits = X(rs1); - 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] == 0b0, - WORD => vaddr[1..0] == 0b00, - DOUBLE => vaddr[2..0] == 0b000 - }; - if (~ (aligned)) - then { handle_mem_exception(vaddr, E_SAMO_Addr_Align); false } - else { - if match_reservation(vaddr) == false then { - /* cannot happen in rmem */ - X(rd) = EXTZ(0b1); cancel_reservation(); true - } else { - match translateAddr(vaddr, Write, Data) { - TR_Failure(e) => { handle_mem_exception(vaddr, e); false }, - TR_Address(addr) => { - let eares : MemoryOpResult(unit) = match (width, sizeof(xlen)) { - (WORD, _) => mem_write_ea(addr, 4, aq, rl, true), - (DOUBLE, 64) => mem_write_ea(addr, 8, aq, rl, true), - _ => internal_error("STORECON expected word or double") - }; - match (eares) { - MemException(e) => { handle_mem_exception(addr, e); false }, - MemValue(_) => { - rs2_val = X(rs2); - let res : MemoryOpResult(bool) = match (width, sizeof(xlen)) { - (WORD, _) => mem_write_value(addr, 4, rs2_val[31..0], aq, rl, true), - (DOUBLE, 64) => mem_write_value(addr, 8, rs2_val, aq, rl, true), + pre_vaddr : xlenbits = X(rs1); + /* Let extensions get the first check on address validity. */ + match ext_data_check_addr(pre_vaddr, Read, Data, width) { + Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); false }, + 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] == 0b0, + WORD => vaddr[1..0] == 0b00, + DOUBLE => vaddr[2..0] == 0b000 + }; + if (~ (aligned)) + then { handle_mem_exception(vaddr, E_SAMO_Addr_Align); false } + else { + if match_reservation(vaddr) == false then { + /* cannot happen in rmem */ + X(rd) = EXTZ(0b1); cancel_reservation(); true + } else { + match translateAddr(vaddr, Write, Data) { + TR_Failure(e) => { handle_mem_exception(vaddr, e); false }, + TR_Address(addr) => { + let eares : MemoryOpResult(unit) = match (width, sizeof(xlen)) { + (WORD, _) => mem_write_ea(addr, 4, aq, rl, true), + (DOUBLE, 64) => mem_write_ea(addr, 8, aq, rl, true), _ => internal_error("STORECON expected word or double") }; - match (res) { - MemValue(true) => { X(rd) = EXTZ(0b0); cancel_reservation(); true }, - MemValue(false) => { X(rd) = EXTZ(0b1); cancel_reservation(); true }, - MemException(e) => { handle_mem_exception(addr, e); false } + match (eares) { + MemException(e) => { handle_mem_exception(addr, e); false }, + MemValue(_) => { + rs2_val = X(rs2); + let res : MemoryOpResult(bool) = match (width, sizeof(xlen)) { + (WORD, _) => mem_write_value(addr, 4, rs2_val[31..0], aq, rl, true), + (DOUBLE, 64) => mem_write_value(addr, 8, rs2_val, aq, rl, true), + _ => internal_error("STORECON expected word or double") + }; + match (res) { + MemValue(true) => { X(rd) = EXTZ(0b0); cancel_reservation(); true }, + MemValue(false) => { X(rd) = EXTZ(0b1); cancel_reservation(); true }, + MemException(e) => { handle_mem_exception(addr, e); false } + } + } } } } @@ -171,53 +183,59 @@ mapping clause encdec = AMO(op, aq, rl, rs2, rs1, size, rd) This may need revisiting. */ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = { if haveAtomics() then { - vaddr : xlenbits = X(rs1); - match translateAddr(vaddr, ReadWrite, Data) { - TR_Failure(e) => { handle_mem_exception(vaddr, e); false }, - TR_Address(addr) => { - let eares : MemoryOpResult(unit) = match (width, sizeof(xlen)) { - (WORD, _) => mem_write_ea(addr, 4, aq & rl, rl, true), - (DOUBLE, 64) => mem_write_ea(addr, 8, aq & rl, rl, true), - _ => internal_error ("AMO expected WORD or DOUBLE") - }; - rs2_val : xlenbits = X(rs2); - match (eares) { - MemException(e) => { handle_mem_exception(addr, e); false }, - MemValue(_) => { - let rval : MemoryOpResult(xlenbits) = match (width, sizeof(xlen)) { - (WORD, _) => extend_value(false, mem_read(addr, 4, aq, aq & rl, true)), - (DOUBLE, 64) => extend_value(false, mem_read(addr, 8, aq, aq & rl, true)), + pre_vaddr : xlenbits = X(rs1); + /* Let extensions get the first check on address validity. */ + match ext_data_check_addr(pre_vaddr, Read, Data, width) { + Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); false }, + Ext_DataAddr_OK(vaddr) => { + match translateAddr(vaddr, ReadWrite, Data) { + TR_Failure(e) => { handle_mem_exception(vaddr, e); false }, + TR_Address(addr) => { + let eares : MemoryOpResult(unit) = match (width, sizeof(xlen)) { + (WORD, _) => mem_write_ea(addr, 4, aq & rl, rl, true), + (DOUBLE, 64) => mem_write_ea(addr, 8, aq & rl, rl, true), _ => internal_error ("AMO expected WORD or DOUBLE") }; - match (rval) { - MemException(e) => { handle_mem_exception(addr, e); false }, - MemValue(loaded) => { - result : xlenbits = - 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))) - }; - - let wval : MemoryOpResult(bool) = match (width, sizeof(xlen)) { - (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("AMO expected WORD or DOUBLE") + rs2_val : xlenbits = X(rs2); + match (eares) { + MemException(e) => { handle_mem_exception(addr, e); false }, + MemValue(_) => { + let rval : MemoryOpResult(xlenbits) = match (width, sizeof(xlen)) { + (WORD, _) => extend_value(false, mem_read(addr, 4, aq, aq & rl, true)), + (DOUBLE, 64) => extend_value(false, mem_read(addr, 8, aq, aq & rl, true)), + _ => internal_error ("AMO expected WORD or DOUBLE") }; - match (wval) { - MemValue(true) => { X(rd) = loaded; true }, - MemValue(false) => { internal_error("AMO got false from mem_write_value") }, - MemException(e) => { handle_mem_exception(addr, e); false } + match (rval) { + MemException(e) => { handle_mem_exception(addr, e); false }, + MemValue(loaded) => { + result : xlenbits = + 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))) + }; + + let wval : MemoryOpResult(bool) = match (width, sizeof(xlen)) { + (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("AMO expected WORD or DOUBLE") + }; + match (wval) { + MemValue(true) => { X(rd) = loaded; true }, + MemValue(false) => { internal_error("AMO got false from mem_write_value") }, + MemException(e) => { handle_mem_exception(addr, e); false } + } + } } } } |