diff options
Diffstat (limited to 'riscv')
| -rw-r--r-- | riscv/prelude.sail | 7 | ||||
| -rw-r--r-- | riscv/riscv.sail | 156 | ||||
| -rw-r--r-- | riscv/riscv_mem.sail | 62 | ||||
| -rw-r--r-- | riscv/riscv_sys.sail | 7 |
4 files changed, 127 insertions, 105 deletions
diff --git a/riscv/prelude.sail b/riscv/prelude.sail index 24e856e7..d667573e 100644 --- a/riscv/prelude.sail +++ b/riscv/prelude.sail @@ -286,8 +286,11 @@ overload max = {max_nat, max_int} val __WriteRAM = "write_ram" : forall 'n 'm. (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> unit effect {wmv} -val __RISCV_write : forall 'n. (bits(64), atom('n), bits(8 * 'n)) -> unit effect {wmv} -function __RISCV_write (addr, width, data) = __WriteRAM(64, width, 0x0000_0000_0000_0000, addr, data) +val __RISCV_write : forall 'n. (bits(64), atom('n), bits(8 * 'n)) -> bool effect {wmv} +function __RISCV_write (addr, width, data) = { + __WriteRAM(64, width, 0x0000_0000_0000_0000, addr, data); + true +} val __TraceMemoryWrite : forall 'n 'm. (atom('n), bits('m), bits(8 * 'n)) -> unit diff --git a/riscv/riscv.sail b/riscv/riscv.sail index 550ccfee..9c61e65f 100644 --- a/riscv/riscv.sail +++ b/riscv/riscv.sail @@ -224,28 +224,21 @@ function extend_value(is_unsigned, value) = match (value) { MemException(e) => MemException(e) } -val process_load : forall 'n, 0 < 'n <= 8. (regbits, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> option(xlenbits) effect {escape, rreg, wreg} +val process_load : forall 'n, 0 < 'n <= 8. (regbits, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> unit effect {escape, rreg, wreg} function process_load(rd, addr, value, is_unsigned) = match (extend_value(is_unsigned, value)) { - MemValue(result) => { X(rd) = result; - Some(result) }, - MemException(e) => - { let t : sync_exception = struct { trap = e, - excinfo = Some(addr) } in - nextPC = handle_exception_ctl(cur_privilege, CTL_TRAP(t), PC); - None() - } + MemValue(result) => X(rd) = result, + MemException(e) => handle_mem_exception(addr, e) } function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = let addr : xlenbits = X(rs1) + EXTS(imm) in - let _ : option(xlenbits) = match width { + match width { BYTE => process_load(rd, addr, mem_read(addr, 1, aq, rl, false), is_unsigned), HALF => process_load(rd, addr, mem_read(addr, 2, aq, rl, false), is_unsigned), WORD => process_load(rd, addr, mem_read(addr, 4, aq, rl, false), is_unsigned), DOUBLE => process_load(rd, addr, mem_read(addr, 8, aq, rl, false), is_unsigned) - } in - () + } /* FIXME: aq/rl are getting dropped */ function clause print_insn (LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = @@ -270,19 +263,27 @@ function clause decode imm7 : bits(7) @ rs2 : regbits @ rs1 : regbits @ 0b010 @ function clause decode imm7 : bits(7) @ rs2 : regbits @ rs1 : regbits @ 0b011 @ imm5 : bits(5) @ 0b0100011 = Some(STORE(imm7 @ imm5, rs2, rs1, DOUBLE, false, false)) function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = - let addr : xlenbits = X(rs1) + EXTS(imm) in { - match width { - BYTE => mem_write_ea(addr, 1, aq, rl, false), - HALF => mem_write_ea(addr, 2, aq, rl, false), - WORD => mem_write_ea(addr, 4, aq, rl, false), - DOUBLE => mem_write_ea(addr, 8, aq, rl, false) - }; - let rs2_val = X(rs2) in - match width { - BYTE => mem_write_value(addr, 1, rs2_val[7..0], aq, rl, false), - HALF => mem_write_value(addr, 2, rs2_val[15..0], aq, rl, false), - WORD => mem_write_value(addr, 4, rs2_val[31..0], aq, rl, false), - DOUBLE => mem_write_value(addr, 8, rs2_val, aq, rl, false) + let addr : xlenbits = X(rs1) + EXTS(imm) in + let eares : MemoryOpResult(unit) = match width { + BYTE => mem_write_ea(addr, 1, aq, rl, false), + HALF => mem_write_ea(addr, 2, aq, rl, false), + WORD => mem_write_ea(addr, 4, aq, rl, false), + DOUBLE => mem_write_ea(addr, 8, aq, rl, false) + } in + match (eares) { + MemException(e) => handle_mem_exception(addr, e), + MemValue(_) => { + let rs2_val = X(rs2) in + let res : MemoryOpResult(unit) = match width { + BYTE => mem_write_value(addr, 1, rs2_val[7..0], aq, rl, false), + HALF => mem_write_value(addr, 2, rs2_val[15..0], aq, rl, false), + WORD => mem_write_value(addr, 4, rs2_val[31..0], aq, rl, false), + DOUBLE => mem_write_value(addr, 8, rs2_val, aq, rl, false) + } in + match (res) { + MemValue(_) => (), + MemException(e) => handle_mem_exception(addr, e) + } } } @@ -566,12 +567,11 @@ val process_loadres : forall 'n, 0 < 'n <= 8. (regbits, xlenbits, MemoryOpResult function clause execute(LOADRES(aq, rl, rs1, width, rd)) = let addr : xlenbits = X(rs1) in - let _ : option(xlenbits) = match width { + match width { WORD => process_load(rd, addr, mem_read(addr, 4, aq, rl, true), false), DOUBLE => process_load(rd, addr, mem_read(addr, 8, aq, rl, true), false), _ => internal_error("LOADRES expected WORD or DOUBLE") - } in - () + } /* FIXME */ function clause print_insn (LOADRES(aq, rl, rs1, width, rd)) = @@ -595,18 +595,27 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = { if status == 0b1 then () else { addr : xlenbits = X(rs1); - match width { + let eares : MemoryOpResult(unit) = match width { WORD => mem_write_ea(addr, 4, aq, rl, true), DOUBLE => mem_write_ea(addr, 8, aq, rl, true), _ => internal_error("STORECON expected word or double") }; - rs2_val = X(rs2); - match width { - WORD => mem_write_value(addr, 4, rs2_val[31..0], aq, rl, true), - DOUBLE => mem_write_value(addr, 8, rs2_val, aq, rl, true), - _ => internal_error("STORECON expected word or double") - }; - }; + match (eares) { + MemException(e) => handle_mem_exception(addr, e), + MemValue(_) => { + rs2_val = X(rs2); + let res : MemoryOpResult(unit) = match width { + WORD => mem_write_value(addr, 4, rs2_val[31..0], aq, rl, true), + DOUBLE => mem_write_value(addr, 8, rs2_val, aq, rl, true), + _ => internal_error("STORECON expected word or double") + } in + match (res) { + MemValue(_) => (), + MemException(e) => handle_mem_exception(addr, e) + } + } + } + } } /* FIXME */ @@ -644,48 +653,49 @@ function clause decode 0b11100 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0 function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = { addr : xlenbits = X(rs1); - match width { + let eares : MemoryOpResult(unit) = match width { WORD => mem_write_ea(addr, 4, aq & rl, rl, true), DOUBLE => mem_write_ea(addr, 8, aq & rl, rl, true), _ => internal_error ("AMO expected WORD or DOUBLE") }; - - /* FIXME: this is incorrect! It could update rd even if the - mem_write below fails. This will be fixed once we support - mem_write actually failing, and then do the write before the - register update. - */ - value : option(xlenbits) = - match width { - WORD => process_load(rd, addr, mem_read(addr, 4, aq, aq & rl, true), false), - DOUBLE => process_load(rd, addr, mem_read(addr, 8, aq, aq & rl, true), false), - _ => internal_error ("AMO expected WORD or DOUBLE") - }; - - match (value) { - None() => (), - Some(loaded) => { - rs2_val : xlenbits = X(rs2); - result : xlenbits = - match op { - AMOSWAP => rs2_val, - AMOADD => rs2_val + loaded, - AMOXOR => rs2_val ^ loaded, - AMOAND => rs2_val & loaded, - AMOOR => rs2_val | loaded, - - /* Have to convert number to vector here. Check this */ - AMOMIN => vector64(min(signed(rs2_val), signed(loaded))), - AMOMAX => vector64(max(signed(rs2_val), signed(loaded))), - AMOMINU => vector64(min(unsigned(rs2_val), unsigned(loaded))), - AMOMAXU => vector64(max(unsigned(rs2_val), unsigned(loaded))) - }; - - match width { - WORD => mem_write_value(addr, 4, result[31..0], aq & rl, rl, true), - DOUBLE => mem_write_value(addr, 8, result, aq & rl, rl, true), - _ => internal_error("AMO expected WORD or DOUBLE") + match (eares) { + MemException(e) => handle_mem_exception(addr, e), + MemValue(_) => { + let rval : MemoryOpResult(xlenbits) = match width { + WORD => extend_value(false, mem_read(addr, 4, aq, aq & rl, true)), + DOUBLE => extend_value(false, mem_read(addr, 8, aq, aq & rl, true)), + _ => internal_error ("AMO expected WORD or DOUBLE") + }; + match (rval) { + MemException(e) => handle_mem_exception(addr, e), + MemValue(loaded) => { + rs2_val : xlenbits = X(rs2); + result : xlenbits = + match op { + AMOSWAP => rs2_val, + AMOADD => rs2_val + loaded, + AMOXOR => rs2_val ^ loaded, + AMOAND => rs2_val & loaded, + AMOOR => rs2_val | loaded, + + /* Have to convert number to vector here. Check this */ + AMOMIN => vector64(min(signed(rs2_val), signed(loaded))), + AMOMAX => vector64(max(signed(rs2_val), signed(loaded))), + AMOMINU => vector64(min(unsigned(rs2_val), unsigned(loaded))), + AMOMAXU => vector64(max(unsigned(rs2_val), unsigned(loaded))) + }; + + let wval : MemoryOpResult(unit) = match width { + WORD => mem_write_value(addr, 4, result[31..0], aq & rl, rl, true), + DOUBLE => mem_write_value(addr, 8, result, aq & rl, rl, true), + _ => internal_error("AMO expected WORD or DOUBLE") + }; + match (wval) { + MemValue(_) => X(rd) = loaded, + MemException(e) => handle_mem_exception(addr, e) + } } + } } } } diff --git a/riscv/riscv_mem.sail b/riscv/riscv_mem.sail index 87d7e41a..67c35bce 100644 --- a/riscv/riscv_mem.sail +++ b/riscv/riscv_mem.sail @@ -1,9 +1,5 @@ /* memory */ -/* TODO: remove this when unused */ -function check_alignment (addr : xlenbits, width : atom('n)) -> forall 'n. unit = - if unsigned(addr) % width != 0 then throw Error_misaligned_access() else () - union MemoryOpResult ('a : Type) = { MemValue : 'a, MemException: ExceptionType @@ -63,43 +59,49 @@ val MEMea_conditional_release = {ocaml: "memea", lem: "MEMea_conditional_release val MEMea_conditional_strong_release = {ocaml: "memea", lem: "MEMea_conditional_strong_release"} : forall 'n. (xlenbits, atom('n)) -> unit effect {eamem} -val mem_write_ea : forall 'n. (xlenbits, atom('n), bool, bool, bool) -> unit effect {eamem, escape} +val mem_write_ea : forall 'n. (xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(unit) effect {eamem, escape} function mem_write_ea (addr, width, aq, rl, con) = { - if rl | con then check_alignment(addr, width); - - match (aq, rl, con) { - (false, false, false) => MEMea(addr, width), - (false, true, false) => MEMea_release(addr, width), - (false, false, true) => MEMea_conditional(addr, width), - (false, true , true) => MEMea_conditional_release(addr, width), + if (rl | con) & (~ (is_aligned_addr(addr, width))) + then MemException(E_SAMO_Addr_Align) + else match (aq, rl, con) { + (false, false, false) => MemValue(MEMea(addr, width)), + (false, true, false) => MemValue(MEMea_release(addr, width)), + (false, false, true) => MemValue(MEMea_conditional(addr, width)), + (false, true , true) => MemValue(MEMea_conditional_release(addr, width)), (true, false, false) => throw(Error_not_implemented("store.aq")), - (true, true, false) => MEMea_strong_release(addr, width), + (true, true, false) => MemValue(MEMea_strong_release(addr, width)), (true, false, true) => throw(Error_not_implemented("sc.aq")), - (true, true , true) => MEMea_conditional_strong_release(addr, width) + (true, true , true) => MemValue(MEMea_conditional_strong_release(addr, width)) } } -val MEMval : forall 'n. (xlenbits, atom('n), bits(8 * 'n)) -> unit effect {wmv} -val MEMval_release : forall 'n. (xlenbits, atom('n), bits(8 * 'n)) -> unit effect {wmv} -val MEMval_strong_release : forall 'n. (xlenbits, atom('n), bits(8 * 'n)) -> unit effect {wmv} -val MEMval_conditional : forall 'n. (xlenbits, atom('n), bits(8 * 'n)) -> unit effect {wmv} -val MEMval_conditional_release : forall 'n. (xlenbits, atom('n), bits(8 * 'n)) -> unit effect {wmv} -val MEMval_conditional_strong_release : forall 'n. (xlenbits, atom('n), bits(8 * 'n)) -> unit effect {wmv} +function checked_mem_write(addr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> forall 'n. MemoryOpResult(unit) = + if (__RISCV_write(addr, width, data)) + then MemValue(()) + else MemException(E_SAMO_Access_Fault) -function MEMval (addr, width, data) = __RISCV_write(addr, width, data) -function MEMval_release (addr, width, data) = __RISCV_write(addr, width, data) -function MEMval_strong_release (addr, width, data) = __RISCV_write(addr, width, data) -function MEMval_conditional (addr, width, data) = __RISCV_write(addr, width, data) -function MEMval_conditional_release (addr, width, data) = __RISCV_write(addr, width, data) -function MEMval_conditional_strong_release (addr, width, data) = __RISCV_write(addr, width, data) +val MEMval : forall 'n. (xlenbits, atom('n), bits(8 * 'n)) -> MemoryOpResult(unit) effect {wmv} +val MEMval_release : forall 'n. (xlenbits, atom('n), bits(8 * 'n)) -> MemoryOpResult(unit) effect {wmv} +val MEMval_strong_release : forall 'n. (xlenbits, atom('n), bits(8 * 'n)) -> MemoryOpResult(unit) effect {wmv} +val MEMval_conditional : forall 'n. (xlenbits, atom('n), bits(8 * 'n)) -> MemoryOpResult(unit) effect {wmv} +val MEMval_conditional_release : forall 'n. (xlenbits, atom('n), bits(8 * 'n)) -> MemoryOpResult(unit) effect {wmv} +val MEMval_conditional_strong_release : forall 'n. (xlenbits, atom('n), bits(8 * 'n)) -> MemoryOpResult(unit) effect {wmv} -val mem_write_value : forall 'n. (xlenbits, atom('n), bits(8 * 'n), bool, bool, bool) -> unit effect {wmv, escape} +function MEMval (addr, width, data) = checked_mem_write(addr, width, data) +function MEMval_release (addr, width, data) = checked_mem_write(addr, width, data) +function MEMval_strong_release (addr, width, data) = checked_mem_write(addr, width, data) +function MEMval_conditional (addr, width, data) = checked_mem_write(addr, width, data) +function MEMval_conditional_release (addr, width, data) = checked_mem_write(addr, width, data) +function MEMval_conditional_strong_release (addr, width, data) = checked_mem_write(addr, width, data) -function mem_write_value (addr, width, value, aq, rl, con) = { - if rl | con then check_alignment(addr, width); - match (aq, rl, con) { +val mem_write_value : forall 'n. (xlenbits, atom('n), bits(8 * 'n), bool, bool, bool) -> MemoryOpResult(unit) effect {wmv, escape} + +function mem_write_value (addr, width, value, aq, rl, con) = { + if (rl | con) & (~ (is_aligned_addr(addr, width))) + then MemException(E_SAMO_Addr_Align) + else match (aq, rl, con) { (false, false, false) => MEMval(addr, width, value), (false, true, false) => MEMval_release(addr, width, value), (false, false, true) => MEMval_conditional(addr, width, value), diff --git a/riscv/riscv_sys.sail b/riscv/riscv_sys.sail index fbba53af..ab15604b 100644 --- a/riscv/riscv_sys.sail +++ b/riscv/riscv_sys.sail @@ -675,6 +675,13 @@ function handle_exception_ctl(cur_priv : Privilege, ctl : ctl_result, } } +function handle_mem_exception(addr : xlenbits, e : ExceptionType) -> unit = { + let t : sync_exception = struct { trap = e, + excinfo = Some(addr) } in + nextPC = handle_exception_ctl(cur_privilege, CTL_TRAP(t), PC) +} + + function init_sys() -> unit = { cur_privilege = Machine; |