diff options
Diffstat (limited to 'os-boot/os-boot-patch.diff')
-rw-r--r-- | os-boot/os-boot-patch.diff | 71 |
1 files changed, 39 insertions, 32 deletions
diff --git a/os-boot/os-boot-patch.diff b/os-boot/os-boot-patch.diff index 03d0c30..f4f1a52 100644 --- a/os-boot/os-boot-patch.diff +++ b/os-boot/os-boot-patch.diff @@ -1,42 +1,49 @@ -diff --git a/model/prelude_mem.sail b/model/prelude_mem.sail -index 8e483f8..8c68192 100644 ---- a/model/prelude_mem.sail -+++ b/model/prelude_mem.sail -@@ -29,8 +29,8 @@ function __RISCV_write (addr, width, data, aq, rl, con) = - (false, true, true) => __WriteRAM_conditional_release(sizeof(xlen), width, EXTZ(0x0), addr, data), - (true, true, false) => __WriteRAM_strong_release(sizeof(xlen), width, EXTZ(0x0), addr, data), - (true, true, true) => __WriteRAM_conditional_strong_release(sizeof(xlen), width, EXTZ(0x0), addr, data), -- (true, false, false) => false, -- (true, false, true) => false -+ (true, false, false) => __WriteRAM(sizeof(xlen), width, EXTZ(0x0), addr, data),//false -+ (true, false, true) => __WriteRAM(sizeof(xlen), width, EXTZ(0x0), addr, data) //false - } - - val __TraceMemoryWrite : forall 'n 'm. diff --git a/model/riscv_mem.sail b/model/riscv_mem.sail -index 3549e80..1d77e6b 100644 +index 256d6de4..45640229 100644 --- a/model/riscv_mem.sail +++ b/model/riscv_mem.sail -@@ -88,9 +88,9 @@ function mem_write_ea (addr, width, aq, rl, con) = { - (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)), +@@ -28,8 +28,8 @@ function phys_mem_read forall 'n, 'n > 0. (t : AccessType, addr : xlenbits, widt + (false, false, true) => Some(read_ram(Read_RISCV_reserved, addr, width)), + (true, false, true) => Some(read_ram(Read_RISCV_reserved_acquire, addr, width)), + (true, true, true) => Some(read_ram(Read_RISCV_reserved_strong_acquire, addr, width)), +- (false, true, false) => None(), /* should these be instead throwing error_not_implemented as below? */ +- (false, true, true) => None() ++ (false, true, false) => Some(read_ram(Read_plain, addr, width)), ++ (false, true, true) => Some(read_ram(Read_plain, addr, width)) + }) : option(bits(8 * 'n)); + match (t, result) { + (Execute, None()) => MemException(E_Fetch_Access_Fault), +@@ -91,8 +91,8 @@ function mem_read (typ, addr, width, aq, rl, res) = { + if (aq | res) & (~ (is_aligned_addr(addr, width))) + then MemException(E_Load_Addr_Align) + else match (aq, rl, res) { +- (false, true, false) => throw(Error_not_implemented("load.rl")), +- (false, true, true) => throw(Error_not_implemented("lr.rl")), ++ (false, true, false) => pmp_mem_read(typ, addr, width, aq, rl, res), ++ (false, true, true) => pmp_mem_read(typ, addr, width, aq, rl, res), + (_, _, _) => pmp_mem_read(typ, addr, width, aq, rl, res) + }; + rvfi_read(addr, width, result); +@@ -109,9 +109,9 @@ function mem_write_ea (addr, width, aq, rl, con) = { + (false, true, false) => MemValue(write_ram_ea(Write_RISCV_release, addr, width)), + (false, false, true) => MemValue(write_ram_ea(Write_RISCV_conditional, addr, width)), + (false, true , true) => MemValue(write_ram_ea(Write_RISCV_conditional_release, addr, width)), - (true, false, false) => throw(Error_not_implemented("store.aq")), -+ (true, false, false) => MemValue(MEMea(addr, width)),//throw(Error_not_implemented("store.aq")), - (true, true, false) => MemValue(MEMea_strong_release(addr, width)), ++ (true, false, false) => MemValue(write_ram_ea(Write_plain, addr, width)), + (true, true, false) => MemValue(write_ram_ea(Write_RISCV_strong_release, addr, width)), - (true, false, true) => throw(Error_not_implemented("sc.aq")), -+ (true, false, true) => MemValue(MEMea(addr, width)),//throw(Error_not_implemented("sc.aq")), - (true, true , true) => MemValue(MEMea_conditional_strong_release(addr, width)) ++ (true, false, true) => MemValue(write_ram_ea(Write_plain, addr, width)), + (true, true , true) => MemValue(write_ram_ea(Write_RISCV_conditional_strong_release, addr, width)) } } -@@ -133,8 +133,8 @@ 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) { +@@ -176,8 +176,8 @@ function mem_write_value_meta (addr, width, value, meta, aq, rl, con) = { + (true, true, false) => pmp_mem_write(Write_RISCV_strong_release, addr, width, value, meta), + (true, true , true) => pmp_mem_write(Write_RISCV_conditional_strong_release, addr, width, value, meta), + // throw an illegal instruction here? - (true, false, false) => throw(Error_not_implemented("store.aq")), -- (true, false, true) => throw(Error_not_implemented("sc.aq")), -+ (true, false, false) => checked_mem_write(addr, width, value, aq, rl, con),//throw(Error_not_implemented("store.aq")), -+ (true, false, true) => checked_mem_write(addr, width, value, aq, rl, con),//throw(Error_not_implemented("sc.aq")), - (_, _, _) => checked_mem_write(addr, width, value, aq, rl, con) +- (true, false, true) => throw(Error_not_implemented("sc.aq")) ++ (true, false, false) => pmp_mem_write(Write_plain, addr, width, value, meta), ++ (true, false, true) => pmp_mem_write(Write_plain, addr, width, value, meta) } } + |