summaryrefslogtreecommitdiff
path: root/riscv/riscv.sail
diff options
context:
space:
mode:
Diffstat (limited to 'riscv/riscv.sail')
-rw-r--r--riscv/riscv.sail156
1 files changed, 83 insertions, 73 deletions
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)
+ }
}
+ }
}
}
}
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 18:01:14 +0000