aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--handwritten_support/riscv_extras.lem22
-rw-r--r--model/prelude.sail33
-rw-r--r--model/riscv_mem.sail51
-rw-r--r--model/riscv_vmem.sail4
4 files changed, 49 insertions, 61 deletions
diff --git a/handwritten_support/riscv_extras.lem b/handwritten_support/riscv_extras.lem
index c1a52c9..ed572be 100644
--- a/handwritten_support/riscv_extras.lem
+++ b/handwritten_support/riscv_extras.lem
@@ -49,15 +49,19 @@ let MEMr_reserved addrsize size hexRAM addr = read_mem Read_RISCV
let MEMr_reserved_acquire addrsize size hexRAM addr = read_mem Read_RISCV_reserved_acquire addr size
let MEMr_reserved_strong_acquire addrsize size hexRAM addr = read_mem Read_RISCV_reserved_strong_acquire addr size
-val write_ram : forall 'rv 'a 'b 'e. Size 'a, Size 'b =>
- integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e
-let write_ram addrsize size hexRAM address value =
- write_mem_val value
-
-val read_ram : forall 'rv 'a 'b 'e. Size 'a, Size 'b =>
- integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e
-let read_ram addrsize size hexRAM address =
- read_mem Read_plain address size
+val MEMw : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e
+val MEMw_release : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e
+val MEMw_strong_release : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e
+val MEMw_conditional : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e
+val MEMw_conditional_release : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e
+val MEMw_conditional_strong_release : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e
+
+let MEMw addrsize size hexRAM addr = write_mem Write_plain addr size
+let MEMw_release addrsize size hexRAM addr = write_mem Write_RISCV_release addr size
+let MEMw_strong_release addrsize size hexRAM addr = write_mem Write_RISCV_strong_release addr size
+let MEMw_conditional addrsize size hexRAM addr = write_mem Write_RISCV_conditional addr size
+let MEMw_conditional_release addrsize size hexRAM addr = write_mem Write_RISCV_conditional_release addr size
+let MEMw_conditional_strong_release addrsize size hexRAM addr = write_mem Write_RISCV_conditional_strong_release addr size
val load_reservation : forall 'a. Size 'a => bitvector 'a -> unit
let load_reservation addr = ()
diff --git a/model/prelude.sail b/model/prelude.sail
index 4f5b98a..91efcc0 100644
--- a/model/prelude.sail
+++ b/model/prelude.sail
@@ -268,13 +268,36 @@ overload min = {min_nat, min_int}
overload max = {max_nat, max_int}
-val __WriteRAM = "write_ram" : forall 'n 'm.
+val __WriteRAM = {lem: "MEMw", _: "write_ram"} : forall 'n 'm.
(atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv}
-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)
-}
+val __WriteRAM_release = {lem: "MEMw_release", _: "write_ram"} : forall 'n 'm.
+ (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv}
+
+val __WriteRAM_strong_release = {lem: "MEMw_strong_release", _: "write_ram"} : forall 'n 'm.
+ (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv}
+
+val __WriteRAM_conditional = {lem: "MEMw_conditional", _: "write_ram"} : forall 'n 'm.
+ (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv}
+
+val __WriteRAM_conditional_release = {lem: "MEMw_conditional_release", _: "write_ram"} : forall 'n 'm.
+ (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv}
+
+val __WriteRAM_conditional_strong_release = {lem: "MEMw_conditional_strong_release", _: "write_ram"} : forall 'n 'm.
+ (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv}
+
+val __RISCV_write : forall 'n. (bits(64), atom('n), bits(8 * 'n), bool, bool, bool) -> bool effect {wmv}
+function __RISCV_write (addr, width, data, aq, rl, con) =
+ match (aq, rl, con) {
+ (false, false, false) => __WriteRAM(64, width, 0x0000_0000_0000_0000, addr, data),
+ (false, true, false) => __WriteRAM_release(64, width, 0x0000_0000_0000_0000, addr, data),
+ (false, false, true) => __WriteRAM_conditional(64, width, 0x0000_0000_0000_0000, addr, data),
+ (false, true, true) => __WriteRAM_conditional_release(64, width, 0x0000_0000_0000_0000, addr, data),
+ (true, true, false) => __WriteRAM_strong_release(64, width, 0x0000_0000_0000_0000, addr, data),
+ (true, true, true) => __WriteRAM_conditional_strong_release(64, width, 0x0000_0000_0000_0000, addr, data),
+ (true, false, false) => false,
+ (true, false, true) => false
+ }
val __TraceMemoryWrite : forall 'n 'm.
(atom('n), bits('m), bits(8 * 'n)) -> unit
diff --git a/model/riscv_mem.sail b/model/riscv_mem.sail
index 0b3e550..3549e80 100644
--- a/model/riscv_mem.sail
+++ b/model/riscv_mem.sail
@@ -26,20 +26,6 @@ function checked_mem_read forall 'n, 'n > 0. (t : ReadType, addr : xlenbits, wid
/* Atomic accesses can be done to MMIO regions, e.g. in kernel access to device registers. */
-val MEMr : forall 'n, 'n > 0. (xlenbits, atom('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rreg}
-val MEMr_acquire : forall 'n, 'n > 0. (xlenbits, atom('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rreg}
-val MEMr_strong_acquire : forall 'n, 'n > 0. (xlenbits, atom('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rreg}
-val MEMr_reserved : forall 'n, 'n > 0. (xlenbits, atom('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rreg}
-val MEMr_reserved_acquire : forall 'n, 'n > 0. (xlenbits, atom('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rreg}
-val MEMr_reserved_strong_acquire : forall 'n, 'n > 0. (xlenbits, atom('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rreg}
-
-function MEMr (addr, width) = checked_mem_read(Data, addr, width, false, false, false)
-function MEMr_acquire (addr, width) = checked_mem_read(Data, addr, width, true, false, false)
-function MEMr_strong_acquire (addr, width) = checked_mem_read(Data, addr, width, true, true, false)
-function MEMr_reserved (addr, width) = checked_mem_read(Data, addr, width, false, false, true)
-function MEMr_reserved_acquire (addr, width) = checked_mem_read(Data, addr, width, true, false, true)
-function MEMr_reserved_strong_acquire (addr, width) = checked_mem_read(Data, addr, width, true, true, true)
-
$ifdef RVFI_DII
val rvfi_read : forall 'n, 'n > 0. (xlenbits, atom('n), MemoryOpResult(bits(8 * 'n))) -> unit effect {wreg}
function rvfi_read (addr, width, result) = {
@@ -71,14 +57,9 @@ function mem_read (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, false, false) => checked_mem_read(Data, addr, width, false, false, false),
- (true, false, false) => MEMr_acquire(addr, width),
- (false, false, true) => MEMr_reserved(addr, width),
- (true, false, true) => MEMr_reserved_acquire(addr, width),
(false, true, false) => throw(Error_not_implemented("load.rl")),
- (true, true, false) => MEMr_strong_acquire(addr, width),
(false, true, true) => throw(Error_not_implemented("lr.rl")),
- (true, true, true) => MEMr_reserved_strong_acquire(addr, width)
+ (_, _, _) => checked_mem_read(Data, addr, width, aq, rl, res)
};
rvfi_read(addr, width, result);
result
@@ -115,36 +96,21 @@ function mem_write_ea (addr, width, aq, rl, con) = {
}
// only used for actual memory regions, to avoid MMIO effects
-function phys_mem_write forall 'n. (addr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> MemoryOpResult(bool) = {
+function phys_mem_write forall 'n. (addr : xlenbits, width : atom('n), data: bits(8 * 'n), aq : bool, rl : bool, con : bool) -> MemoryOpResult(bool) = {
print_mem("mem[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data));
- MemValue(__RISCV_write(addr, width, data))
+ MemValue(__RISCV_write(addr, width, data, aq, rl, con))
}
// dispatches to MMIO regions or physical memory regions depending on physical memory map
-function checked_mem_write forall 'n, 'n > 0. (addr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> MemoryOpResult(bool) =
+function checked_mem_write forall 'n, 'n > 0. (addr : xlenbits, width : atom('n), data: bits(8 * 'n), aq : bool, rl : bool, con : bool) -> MemoryOpResult(bool) =
if within_mmio_writable(addr, width)
then mmio_write(addr, width, data)
else if within_phys_mem(addr, width)
- then phys_mem_write(addr, width, data)
+ then phys_mem_write(addr, width, data, aq, rl, con)
else MemException(E_SAMO_Access_Fault)
/* Atomic accesses can be done to MMIO regions, e.g. in kernel access to device registers. */
-val MEMval : forall 'n, 'n > 0. (xlenbits, atom('n), bits(8 * 'n)) -> MemoryOpResult(bool) effect {wmv, rreg, wreg}
-val MEMval_release : forall 'n, 'n > 0. (xlenbits, atom('n), bits(8 * 'n)) -> MemoryOpResult(bool) effect {wmv, rreg, wreg}
-val MEMval_strong_release : forall 'n, 'n > 0. (xlenbits, atom('n), bits(8 * 'n)) -> MemoryOpResult(bool) effect {wmv, rreg, wreg}
-val MEMval_conditional : forall 'n, 'n > 0. (xlenbits, atom('n), bits(8 * 'n)) -> MemoryOpResult(bool) effect {wmv, rreg, wreg}
-val MEMval_conditional_release : forall 'n, 'n > 0. (xlenbits, atom('n), bits(8 * 'n)) -> MemoryOpResult(bool) effect {wmv, rreg, wreg}
-val MEMval_conditional_strong_release : forall 'n, 'n > 0. (xlenbits, atom('n), bits(8 * 'n)) -> MemoryOpResult(bool) effect {wmv, rreg, wreg}
-
-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)
-
-
$ifdef RVFI_DII
val rvfi_write : forall 'n, 'n > 0. (xlenbits, atom('n), bits(8 * 'n)) -> unit effect {wreg}
function rvfi_write (addr, width, value) = {
@@ -167,14 +133,9 @@ 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) => checked_mem_write(addr, width, value),
- (false, true, false) => MEMval_release(addr, width, value),
- (false, false, true) => MEMval_conditional(addr, width, value),
- (false, true, true) => MEMval_conditional_release(addr, width, value),
(true, false, false) => throw(Error_not_implemented("store.aq")),
- (true, true, false) => MEMval_strong_release(addr, width, value),
(true, false, true) => throw(Error_not_implemented("sc.aq")),
- (true, true, true) => MEMval_conditional_strong_release(addr, width, value)
+ (_, _, _) => checked_mem_write(addr, width, value, aq, rl, con)
}
}
diff --git a/model/riscv_vmem.sail b/model/riscv_vmem.sail
index b617d29..ef56108 100644
--- a/model/riscv_vmem.sail
+++ b/model/riscv_vmem.sail
@@ -313,7 +313,7 @@ function translate39(vAddr, ac, priv, mxr, do_sum, level) = {
n_ent.pte = update_BITS(ent.pte, pbits.bits());
writeTLB39(idx, n_ent);
/* update page table */
- match checked_mem_write(EXTZ(ent.pteAddr), 8, ent.pte.bits()) {
+ match checked_mem_write(EXTZ(ent.pteAddr), 8, ent.pte.bits(), false, false, false) {
MemValue(_) => (),
MemException(e) => internal_error("invalid physical address in TLB")
};
@@ -339,7 +339,7 @@ function translate39(vAddr, ac, priv, mxr, do_sum, level) = {
TR39_Failure(PTW_PTE_Update)
} else {
w_pte : SV39_PTE = update_BITS(pte, pbits.bits());
- match checked_mem_write(EXTZ(pteAddr), 8, w_pte.bits()) {
+ match checked_mem_write(EXTZ(pteAddr), 8, w_pte.bits(), false, false, false) {
MemValue(_) => {
addToTLB39(asid, vAddr, pAddr, w_pte, pteAddr, level, global);
TR39_Address(pAddr)
generated by cgit v1.1 at 2024-11-16 17:55:53 +0000