diff options
| -rw-r--r-- | Makefile | 4 | ||||
| -rw-r--r-- | model/riscv_insts_aext.sail | 207 | ||||
| -rw-r--r-- | model/riscv_insts_base.sail | 23 | ||||
| -rw-r--r-- | model/riscv_insts_begin.sail | 6 | ||||
| -rw-r--r-- | model/riscv_insts_end.sail | 10 | ||||
| -rw-r--r-- | model/riscv_insts_helpers.sail | 37 |
6 files changed, 166 insertions, 121 deletions
@@ -21,8 +21,8 @@ SAIL_DEFAULT_INST = riscv_insts_base.sail riscv_insts_aext.sail riscv_insts_cext SAIL_SEQ_INST = $(SAIL_DEFAULT_INST) riscv_jalr_seq.sail SAIL_RMEM_INST = $(SAIL_DEFAULT_INST) riscv_jalr_rmem.sail riscv_insts_rmem.sail -SAIL_SEQ_INST_SRCS = riscv_insts_begin.sail $(SAIL_SEQ_INST) riscv_insts_end.sail -SAIL_RMEM_INST_SRCS = riscv_insts_begin.sail $(SAIL_RMEM_INST) riscv_insts_end.sail +SAIL_SEQ_INST_SRCS = riscv_insts_begin.sail riscv_insts_helpers.sail $(SAIL_SEQ_INST) riscv_insts_end.sail +SAIL_RMEM_INST_SRCS = riscv_insts_begin.sail riscv_insts_helpers.sail $(SAIL_RMEM_INST) riscv_insts_end.sail # System and platform sources SAIL_SYS_SRCS = riscv_csr_map.sail diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail index 490a06e..0410f50 100644 --- a/model/riscv_insts_aext.sail +++ b/model/riscv_insts_aext.sail @@ -26,52 +26,52 @@ union clause ast = LOADRES : (bool, bool, regidx, word_width, regidx) mapping clause encdec = LOADRES(aq, rl, rs1, size, rd) <-> 0b00010 @ bool_bits(aq) @ bool_bits(rl) @ 0b00000 @ rs1 @ 0b0 @ size_bits(size) @ rd @ 0b0101111 -/* We could set load-reservations on physical or virtual addresses. - * For now we set them on virtual addresses, since it makes the - * sequential model of SC a bit simpler, at the cost of an explicit - * call to load_reservation in LR and cancel_reservation in SC. - */ +val default_loadres : (bool, bool, regidx, word_width, regidx) -> Retired effect {escape, wreg, rreg, wmv, wmvt, eamem, rmem, barr, exmem} +function default_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) { + Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, + Ext_DataAddr_OK(vaddr) => { + let aligned : bool = + /* BYTE and HALF would not occur due to the above check, but it doesn't hurt + * to treat them as valid here. + */ + 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); 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)) { + (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), -val process_loadres : forall 'n, 0 < 'n <= xlen_bytes. (regidx, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> Retired effect {escape, rreg, wreg} -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 } + /* should never get here due to extension hook */ + _ => internal_error("LOADRES expected WORD or DOUBLE") + } + } + } } +} function clause execute(LOADRES(aq, rl, rs1, width, rd)) = { if haveAtomics() then { - /* 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) { - 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] == 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); 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)) { - (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") - } - } - } + /* dispatch defined combinations to the default implementation, others to the extension hook. */ + /* for now, we assume that these extensions need misa.A set. */ + match (width, sizeof(xlen)) { + (WORD, _) => default_loadres(aq, rl, rs1, width, rd), + (DOUBLE, 64) => default_loadres(aq, rl, rs1, width, rd), + _ => ext_execute(LOADRES(aq, rl, rs1, width, rd)) } } else { handle_illegal(); @@ -89,63 +89,59 @@ mapping clause encdec = STORECON(aq, rl, rs2, rs1, size, rd) <-> 0b00011 @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_bits(size) @ rd @ 0b0101111 /* NOTE: Currently, we only EA if address translation is successful. This may need revisiting. */ -function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = { - if speculate_conditional () == false then { - /* should only happen in rmem - * rmem: allow SC to fail very early - */ - X(rd) = EXTZ(0b1); RETIRE_SUCCESS - } else { - if haveAtomics() then { - /* normal non-rmem case - * rmem: SC is allowed to succeed (but might fail later) - */ - /* 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) { - 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] == 0b0, - WORD => vaddr[1..0] == 0b00, - DOUBLE => vaddr[2..0] == 0b000 - }; - if (~ (aligned)) - then { handle_mem_exception(vaddr, E_SAMO_Addr_Align); RETIRE_FAIL } - else { - if match_reservation(vaddr) == false then { - /* cannot happen in rmem */ - X(rd) = EXTZ(0b1); cancel_reservation(); RETIRE_SUCCESS - } else { - match translateAddr(vaddr, Write, Data) { - TR_Failure(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, - 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), +val default_storecon : (bool, bool, regidx, regidx, word_width, regidx) -> Retired effect {escape, wreg, rreg, wmv, wmvt, eamem, rmem, barr, exmem} +function default_storecon (aq, rl, rs2, rs1, width, rd) = { + /* normal non-rmem case + * rmem: SC is allowed to succeed (but might fail later) + */ + /* 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) { + 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] == 0b0, + WORD => vaddr[1..0] == 0b00, + DOUBLE => vaddr[2..0] == 0b000 + }; + if (~ (aligned)) + then { handle_mem_exception(vaddr, E_SAMO_Addr_Align); RETIRE_FAIL } + else { + if match_reservation(vaddr) == false then { + /* cannot happen in rmem */ + X(rd) = EXTZ(0b1); cancel_reservation(); RETIRE_SUCCESS + } else { + match translateAddr(vaddr, Write, Data) { + TR_Failure(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + 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), + + /* should never get here due to extension hook */ + _ => internal_error("STORECON expected word or double") + }; + match (eares) { + MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL }, + 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), + + /* should never get here due to extension hook */ _ => internal_error("STORECON expected word or double") }; - match (eares) { - MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL }, - 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(); RETIRE_SUCCESS }, - MemValue(false) => { X(rd) = EXTZ(0b1); cancel_reservation(); RETIRE_SUCCESS }, - MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL } - } - } + match (res) { + MemValue(true) => { X(rd) = EXTZ(0b0); cancel_reservation(); RETIRE_SUCCESS }, + MemValue(false) => { X(rd) = EXTZ(0b1); cancel_reservation(); RETIRE_SUCCESS }, + MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL } } } } @@ -153,6 +149,25 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = { } } } + } + } +} + +function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = { + if speculate_conditional () == false then { + /* should only happen in rmem + * rmem: allow SC to fail very early + */ + X(rd) = EXTZ(0b1); RETIRE_SUCCESS + } else { + if haveAtomics() then { + /* dispatch defined combinations to the default implementation, others to the extension hook. */ + /* for now, we assume that these extensions need misa.A set. */ + match (width, sizeof(xlen)) { + (WORD, _) => default_storecon(aq, rl, rs2, rs1, width, rd), + (DOUBLE, 64) => default_storecon(aq, rl, rs2, rs1, width, rd), + _ => ext_execute(STORECON(aq, rl, rs2, rs1, width, rd)) + } } else { handle_illegal(); RETIRE_FAIL diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail index 0a08853..a9ebd8f 100644 --- a/model/riscv_insts_base.sail +++ b/model/riscv_insts_base.sail @@ -291,28 +291,6 @@ 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_bits(size) != 0b11 | not_bool(is_unsigned) <-> imm @ rs1 @ bool_bits(is_unsigned) @ size_bits(size) @ rd @ 0b0000011 if size_bits(size) != 0b11 | not_bool(is_unsigned) -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 EXTZ(v) else EXTS(v) : xlenbits), - MemException(e) => MemException(e) -} - -val process_load : forall 'n, 0 < 'n <= xlen_bytes. (regidx, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> Retired effect {escape, rreg, wreg} -function process_load(rd, addr, value, is_unsigned) = - match extend_value(is_unsigned, value) { - MemValue(result) => { X(rd) = result; RETIRE_SUCCESS }, - MemException(e) => { handle_mem_exception(addr, 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] == true, - WORD => vaddr[0] == true | vaddr[1] == true, - DOUBLE => vaddr[0] == true | vaddr[1] == true | vaddr[2] == true - } - function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = { let offset : xlenbits = EXTS(imm); /* Get the address, X(rs1) + offset. @@ -750,4 +728,3 @@ function clause execute SFENCE_VMA(rs1, rs2) = { mapping clause assembly = SFENCE_VMA(rs1, rs2) <-> "sfence.vma" ^ spc() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) - diff --git a/model/riscv_insts_begin.sail b/model/riscv_insts_begin.sail index b007246..8e98271 100644 --- a/model/riscv_insts_begin.sail +++ b/model/riscv_insts_begin.sail @@ -17,3 +17,9 @@ scattered mapping encdec val encdec_compressed : ast <-> bits(16) scattered mapping encdec_compressed + +/* an ast not defined in the standard might be defined by an extension. + * this hook allows the extension to implement these ast. it has the + * same semantics as execute. + */ +val ext_execute : ast -> Retired effect {escape, wreg, rreg, wmv, wmvt, eamem, rmem, barr, exmem} diff --git a/model/riscv_insts_end.sail b/model/riscv_insts_end.sail index e52f19d..49d1e5d 100644 --- a/model/riscv_insts_end.sail +++ b/model/riscv_insts_end.sail @@ -22,12 +22,22 @@ mapping clause assembly = C_ILLEGAL(s) <-> "c.illegal" ^ spc() ^ hex_bits_16(s) /* ****************************************************************** */ +/* The default implementation for unknown or undefined ast values: + * treat them as illegal instructions. + */ + +function clause ext_execute (_) = { + handle_illegal(); + RETIRE_FAIL +} + /* End definitions */ end ast end execute end assembly end encdec end encdec_compressed +end ext_execute val cast print_insn : ast -> string function print_insn insn = assembly(insn) diff --git a/model/riscv_insts_helpers.sail b/model/riscv_insts_helpers.sail new file mode 100644 index 0000000..ef229f3 --- /dev/null +++ b/model/riscv_insts_helpers.sail @@ -0,0 +1,37 @@ +/* This file contains some helpers for instruction definition. They are collected + * here for use by instruction extensions. + */ + +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 EXTZ(v) else EXTS(v) : xlenbits), + MemException(e) => MemException(e) +} + +val process_load : forall 'n, 0 < 'n <= xlen_bytes. (regidx, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> Retired effect {escape, rreg, wreg} +function process_load(rd, addr, value, is_unsigned) = + match extend_value(is_unsigned, value) { + MemValue(result) => { X(rd) = result; RETIRE_SUCCESS }, + MemException(e) => { handle_mem_exception(addr, 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] == true, + WORD => vaddr[0] == true | vaddr[1] == true, + DOUBLE => vaddr[0] == true | vaddr[1] == true | vaddr[2] == true + } + +/* We could set load-reservations on physical or virtual addresses. + * For now we set them on virtual addresses, since it makes the + * sequential model of SC a bit simpler, at the cost of an explicit + * 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 effect {escape, rreg, wreg} +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 } + } |