summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--riscv/riscv_mem.sail20
-rw-r--r--riscv/riscv_platform.sail28
-rw-r--r--riscv/riscv_types.sail53
3 files changed, 65 insertions, 36 deletions
diff --git a/riscv/riscv_mem.sail b/riscv/riscv_mem.sail
index 1c914eca..788ef594 100644
--- a/riscv/riscv_mem.sail
+++ b/riscv/riscv_mem.sail
@@ -8,14 +8,16 @@ function phys_mem_read(t : ReadType, addr : xlenbits, width : atom('n)) -> foral
match (t, __RISCV_read(addr, width)) {
(Instruction, None()) => MemException(E_Fetch_Access_Fault),
(Data, None()) => MemException(E_Load_Access_Fault),
- (_, Some(v)) => MemValue(v)
+ (_, Some(v)) => { print("mem[" ^ t ^ "," ^ BitStr(addr) ^ "] -> " ^ BitStr(v));
+ MemValue(v) }
}
function checked_mem_read(t : ReadType, addr : xlenbits, width : atom('n)) -> forall 'n. MemoryOpResult(bits(8 * 'n)) =
- if within_phys_mem(addr, width)
+ /* treat MMIO regions as not executable for now. TODO: this should actually come from PMP/PMA. */
+ if t == Data & within_mmio_readable(addr, width)
+ then mmio_read(addr, width)
+ else if within_phys_mem(addr, width)
then phys_mem_read(t, addr, width)
- else if t == Data /* treat MMIO regions as not executable for now. TODO: this should actually come from PMP/PMA. */
- then mmio_load(addr, width)
else MemException(E_Load_Access_Fault)
/* FIXME: We assume atomic accesses are only done to memory-backed regions. MMIO is not modeled. */
@@ -83,15 +85,19 @@ function mem_write_ea (addr, width, aq, rl, con) = {
}
// only used for actual memory regions, to avoid MMIO effects
-function phys_mem_write(addr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> forall 'n. MemoryOpResult(unit) =
+function phys_mem_write(addr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> forall 'n. MemoryOpResult(unit) = {
+ print("mem[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data));
if __RISCV_write(addr, width, data)
then MemValue(())
else MemException(E_SAMO_Access_Fault)
+}
function checked_mem_write(addr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> forall 'n, 'n > 0. MemoryOpResult(unit) =
- if within_phys_mem(addr, width)
+ 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)
- else mmio_write(addr, width, data)
+ else MemException(E_SAMO_Access_Fault)
/* FIXME: We assume atomic accesses are only done to memory-backed regions. MMIO is not modeled. */
diff --git a/riscv/riscv_platform.sail b/riscv/riscv_platform.sail
index 761aeebd..405f79dd 100644
--- a/riscv/riscv_platform.sail
+++ b/riscv/riscv_platform.sail
@@ -78,16 +78,26 @@ val clint_load : forall 'n. (xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n))
function clint_load(addr, width) = {
/* FIXME: For now, only allow exact aligned access. */
if addr == MSIP_BASE & ('n == 8 | 'n == 4)
- then MemValue(zero_extend(mip.MSI(), sizeof(8 * 'n)))
+ then {
+ print("clint[" ^ BitStr(addr) ^ "] -> " ^ BitStr(mip.MSI()));
+ MemValue(zero_extend(mip.MSI(), sizeof(8 * 'n)))
+ }
else if addr == MTIMECMP_BASE & ('n == 8)
- then MemValue(zero_extend(mtimecmp, 64)) /* FIXME: Redundant zero_extend currently required by Lem backend */
+ then {
+ print("clint[" ^ BitStr(addr) ^ "] -> " ^ BitStr(mtimecmp));
+ MemValue(zero_extend(mtimecmp, 64)) /* FIXME: Redundant zero_extend currently required by Lem backend */
+ }
else if addr == MTIME_BASE & ('n == 8)
- then MemValue(zero_extend(mtime, 64))
+ then {
+ print("clint[" ^ BitStr(addr) ^ "] -> " ^ BitStr(mtime));
+ MemValue(zero_extend(mtime, 64))
+ }
else MemException(E_Load_Access_Fault)
}
val clint_store: forall 'n, 'n > 0. (xlenbits, int('n), bits(8 * 'n)) -> MemoryOpResult(unit) effect {wreg}
function clint_store(addr, width, data) = {
+ print("clint[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data));
if addr == MSIP_BASE & ('n == 8 | 'n == 4) then {
mip->MSI() = data[0] == 0b1;
MemValue(())
@@ -125,6 +135,7 @@ function htif_store(addr, width, data) = {
let cmd = Mk_htif_cmd(cbits);
match cmd.device() {
0x00 => { /* syscall-proxy */
+ print("htif-syscall-proxy[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data));
if cmd.payload()[0] == 0b1
then {
htif_done = true;
@@ -133,20 +144,27 @@ function htif_store(addr, width, data) = {
else ()
},
0x01 => { /* terminal */
+ print("htif-term[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data));
match cmd.cmd() {
0x00 => /* TODO: terminal input handling */ (),
0x01 => plat_term_write(cmd.payload()[7..0]),
c => print("Unknown term cmd: " ^ BitStr(c))
}
},
- d => print("Unknown htif device:" ^ BitStr(d))
+ d => print("htif-????[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data))
};
MemValue(())
}
/* Top-level MMIO dispatch */
-function mmio_load(addr : xlenbits, width : atom('n)) -> forall 'n. MemoryOpResult(bits(8 * 'n)) =
+function within_mmio_readable(addr : xlenbits, width : atom('n)) -> forall 'n. bool =
+ within_clint(addr, width) | (within_htif_readable(addr, width) & 1 <= 'n)
+
+function within_mmio_writable(addr : xlenbits, width : atom('n)) -> forall 'n. bool =
+ within_clint(addr, width) | (within_htif_writable(addr, width) & 'n <= 8)
+
+function mmio_read(addr : xlenbits, width : atom('n)) -> forall 'n. MemoryOpResult(bits(8 * 'n)) =
if within_clint(addr, width)
then clint_load(addr, width)
else if within_htif_readable(addr, width) & (1 <= 'n)
diff --git a/riscv/riscv_types.sail b/riscv/riscv_types.sail
index 5a71c737..1a79670b 100644
--- a/riscv/riscv_types.sail
+++ b/riscv/riscv_types.sail
@@ -97,21 +97,20 @@ type amo = bits(1)
/* base architecture definitions */
enum Architecture = {RV32, RV64, RV128}
type arch_xlen = bits(2)
-function architecture(a : arch_xlen) -> option(Architecture) = {
+function architecture(a : arch_xlen) -> option(Architecture) =
match (a) {
0b01 => Some(RV32),
0b10 => Some(RV64),
0b11 => Some(RV128),
_ => None()
}
-}
-function arch_to_bits(a : Architecture) -> arch_xlen = {
+
+function arch_to_bits(a : Architecture) -> arch_xlen =
match (a) {
RV32 => 0b01,
RV64 => 0b10,
RV128 => 0b11
}
-}
/* privilege levels */
@@ -119,35 +118,48 @@ type priv_level = bits(2)
enum Privilege = {User, Supervisor, Machine}
val cast privLevel_to_bits : Privilege -> priv_level
-function privLevel_to_bits (p) = {
+function privLevel_to_bits (p) =
match (p) {
User => 0b00,
Supervisor => 0b01,
Machine => 0b11
}
-}
val cast privLevel_of_bits : priv_level -> Privilege
-function privLevel_of_bits (p) = {
+function privLevel_of_bits (p) =
match (p) {
0b00 => User,
0b01 => Supervisor,
0b11 => Machine
}
-}
val cast privLevel_to_str : Privilege -> string
-function privLevel_to_str (p) = {
+function privLevel_to_str (p) =
match (p) {
User => "U",
Supervisor => "S",
Machine => "M"
}
-}
/* access types */
+
enum AccessType = {Read, Write, ReadWrite, Execute}
+val cast accessType_to_str : AccessType -> string
+function accessType_to_str (a) =
+ match (a) {
+ Read => "R",
+ Write => "W",
+ ReadWrite => "RW",
+ Execute => "X"
+ }
+
enum ReadType = {Instruction, Data}
+val cast readType_to_str : ReadType -> string
+function readType_to_str (r) =
+ match (r) {
+ Instruction => "I",
+ Data => "D"
+ }
/* architectural exception and interrupt definitions */
@@ -173,7 +185,7 @@ enum ExceptionType = {
}
val cast exceptionType_to_bits : ExceptionType -> exc_code
-function exceptionType_to_bits(e) = {
+function exceptionType_to_bits(e) =
match (e) {
E_Fetch_Addr_Align => 0x0,
E_Fetch_Access_Fault => 0x1,
@@ -192,10 +204,9 @@ function exceptionType_to_bits(e) = {
E_Reserved_14 => 0xe,
E_SAMO_Page_Fault => 0xf
}
-}
val cast exceptionType_to_str : ExceptionType -> string
-function exceptionType_to_str(e) = {
+function exceptionType_to_str(e) =
match (e) {
E_Fetch_Addr_Align => "fisaligned-fetch",
E_Fetch_Access_Fault => "fetch-access-fault",
@@ -214,7 +225,6 @@ function exceptionType_to_str(e) = {
E_Reserved_14 => "reserved-1",
E_SAMO_Page_Fault => "store/amo-page-fault"
}
-}
enum InterruptType = {
I_U_Software,
@@ -229,7 +239,7 @@ enum InterruptType = {
}
val cast interruptType_to_bits : InterruptType -> exc_code
-function interruptType_to_bits (i) = {
+function interruptType_to_bits (i) =
match (i) {
I_U_Software => 0x0,
I_S_Software => 0x1,
@@ -241,19 +251,17 @@ function interruptType_to_bits (i) = {
I_S_External => 0x9,
I_M_External => 0xb
}
-}
type tv_mode = bits(2)
enum TrapVectorMode = {TV_Direct, TV_Vector, TV_Reserved}
val cast trapVectorMode_of_bits : tv_mode -> TrapVectorMode
-function trapVectorMode_of_bits (m) = {
+function trapVectorMode_of_bits (m) =
match (m) {
0b00 => TV_Direct,
0b01 => TV_Vector,
_ => TV_Reserved
}
-}
/* other exceptions */
@@ -277,38 +285,35 @@ type ext_status = bits(2)
enum ExtStatus = {Off, Initial, Clean, Dirty}
val cast extStatus_to_bits : ExtStatus -> ext_status
-function extStatus_to_bits(e) = {
+function extStatus_to_bits(e) =
match (e) {
Off => 0b00,
Initial => 0b01,
Clean => 0b10,
Dirty => 0b11
}
-}
val cast extStatus_of_bits : ext_status -> ExtStatus
-function extStatus_of_bits(e) = {
+function extStatus_of_bits(e) =
match (e) {
0b00 => Off,
0b01 => Initial,
0b10 => Clean,
0b11 => Dirty
}
-}
/* supervisor-level address translation modes */
type satp_mode = bits(4)
enum SATPMode = {Sbare, Sv32, Sv39}
-function satpMode_of_bits(a : Architecture, m : satp_mode) -> option(SATPMode) = {
+function satpMode_of_bits(a : Architecture, m : satp_mode) -> option(SATPMode) =
match (a, m) {
(_, 0x0) => Some(Sbare),
(RV32, 0x1) => Some(Sv32),
(RV64, 0x8) => Some(Sv39),
(_, _) => None()
}
-}
/* CSR access control bits (from CSR addresses) */
type csrRW = bits(2) /* read/write */
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-14 16:07:17 +0000