From df6eac371d270556012e46a0bb912e5dc51fad84 Mon Sep 17 00:00:00 2001 From: Tim Hutt Date: Wed, 6 Mar 2024 10:52:53 +0000 Subject: [PATCH] Replace atom with int This is the newer, less confusing (and documented!) syntax. Fixes #425. --- model/prelude.sail | 12 ++++---- model/prelude_mem.sail | 10 +++--- model/prelude_mem_metadata.sail | 4 +-- model/riscv_addr_checks_common.sail | 4 +-- model/riscv_mem.sail | 48 ++++++++++++++--------------- model/riscv_platform.sail | 20 ++++++------ model/riscv_pmp_control.sail | 2 +- model/riscv_types.sail | 4 +-- model/rvfi_dii.sail | 2 +- 9 files changed, 53 insertions(+), 53 deletions(-) diff --git a/model/prelude.sail b/model/prelude.sail index b1814b1d8..028af2126 100644 --- a/model/prelude.sail +++ b/model/prelude.sail @@ -66,7 +66,7 @@ overload min = {min_int} overload max = {max_int} -val pow2 = "pow2" : forall 'n. atom('n) -> atom(2 ^ 'n) +val pow2 = "pow2" : forall 'n. int('n) -> int(2 ^ 'n) val print = "print_endline" : string -> unit val print_string = "print_string" : (string, string) -> unit @@ -112,7 +112,7 @@ function bit_to_bool b = match b { bitzero => false } -val to_bits : forall 'l, 'l >= 0.(atom('l), int) -> bits('l) +val to_bits : forall 'l, 'l >= 0.(int('l), int) -> bits('l) function to_bits (l, n) = get_slice_int(l, n, 0) infix 4 <_s @@ -148,8 +148,8 @@ infix 7 << val "shift_bits_right" : forall 'n 'm. (bits('n), bits('m)) -> bits('n) val "shift_bits_left" : forall 'n 'm. (bits('n), bits('m)) -> bits('n) -val "shiftl" : forall 'm 'n, 'n >= 0. (bits('m), atom('n)) -> bits('m) -val "shiftr" : forall 'm 'n, 'n >= 0. (bits('m), atom('n)) -> bits('m) +val "shiftl" : forall 'm 'n, 'n >= 0. (bits('m), int('n)) -> bits('m) +val "shiftr" : forall 'm 'n, 'n >= 0. (bits('m), int('n)) -> bits('m) overload operator >> = {shift_bits_right, shiftr} overload operator << = {shift_bits_left, shiftl} @@ -175,11 +175,11 @@ val rotate_bits_left : forall 'n 'm, 'm >= 0. (bits('n), bits('m)) -> bits('n) function rotate_bits_left (v, n) = (v << n) | (v >> (to_bits(length(n), length(v)) - n)) -val rotater : forall 'm 'n, 'm >= 'n >= 0. (bits('m), atom('n)) -> bits('m) +val rotater : forall 'm 'n, 'm >= 'n >= 0. (bits('m), int('n)) -> bits('m) function rotater (v, n) = (v >> n) | (v << (length(v) - n)) -val rotatel : forall 'm 'n, 'm >= 'n >= 0. (bits('m), atom('n)) -> bits('m) +val rotatel : forall 'm 'n, 'm >= 'n >= 0. (bits('m), int('n)) -> bits('m) function rotatel (v, n) = (v << n) | (v >> (length(v) - n)) diff --git a/model/prelude_mem.sail b/model/prelude_mem.sail index f2067f680..c4f3d0710 100644 --- a/model/prelude_mem.sail +++ b/model/prelude_mem.sail @@ -27,7 +27,7 @@ capabilities and SIMD / vector instructions will also need more. */ type max_mem_access : Int = 16 -val write_ram = {lem: "write_ram", coq: "write_ram"} : forall 'n, 0 < 'n <= max_mem_access . (write_kind, xlenbits, atom('n), bits(8 * 'n), mem_meta) -> bool +val write_ram = {lem: "write_ram", coq: "write_ram"} : forall 'n, 0 < 'n <= max_mem_access . (write_kind, xlenbits, int('n), bits(8 * 'n), mem_meta) -> bool function write_ram(wk, addr, width, data, meta) = { /* Write out metadata only if the value write succeeds. * It is assumed for now that this write always succeeds; @@ -41,14 +41,14 @@ function write_ram(wk, addr, width, data, meta) = { ret } -val write_ram_ea : forall 'n, 0 < 'n <= max_mem_access . (write_kind, xlenbits, atom('n)) -> unit +val write_ram_ea : forall 'n, 0 < 'n <= max_mem_access . (write_kind, xlenbits, int('n)) -> unit function write_ram_ea(wk, addr, width) = __write_mem_ea(wk, sizeof(xlen), addr, width) -val read_ram = {lem: "read_ram", coq: "read_ram"} : forall 'n, 0 < 'n <= max_mem_access . (read_kind, xlenbits, atom('n), bool) -> (bits(8 * 'n), mem_meta) +val read_ram = {lem: "read_ram", coq: "read_ram"} : forall 'n, 0 < 'n <= max_mem_access . (read_kind, xlenbits, int('n), bool) -> (bits(8 * 'n), mem_meta) function read_ram(rk, addr, width, read_meta) = let meta = if read_meta then __ReadRAM_Meta(addr, width) else default_meta in (__read_mem(rk, sizeof(xlen), addr, width), meta) -val __TraceMemoryWrite : forall 'n 'm. (atom('n), bits('m), bits(8 * 'n)) -> unit -val __TraceMemoryRead : forall 'n 'm. (atom('n), bits('m), bits(8 * 'n)) -> unit +val __TraceMemoryWrite : forall 'n 'm. (int('n), bits('m), bits(8 * 'n)) -> unit +val __TraceMemoryRead : forall 'n 'm. (int('n), bits('m), bits(8 * 'n)) -> unit diff --git a/model/prelude_mem_metadata.sail b/model/prelude_mem_metadata.sail index 640a5c529..b8dd81b32 100644 --- a/model/prelude_mem_metadata.sail +++ b/model/prelude_mem_metadata.sail @@ -14,8 +14,8 @@ type mem_meta = unit let default_meta : mem_meta = () -val __WriteRAM_Meta : forall 'n. (xlenbits, atom('n), mem_meta) -> unit +val __WriteRAM_Meta : forall 'n. (xlenbits, int('n), mem_meta) -> unit function __WriteRAM_Meta(addr, width, meta) = () -val __ReadRAM_Meta : forall 'n. (xlenbits, atom('n)) -> mem_meta +val __ReadRAM_Meta : forall 'n. (xlenbits, int('n)) -> mem_meta function __ReadRAM_Meta(addr, width) = () diff --git a/model/riscv_addr_checks_common.sail b/model/riscv_addr_checks_common.sail index f76ac2839..b7a269842 100644 --- a/model/riscv_addr_checks_common.sail +++ b/model/riscv_addr_checks_common.sail @@ -40,7 +40,7 @@ union Ext_PhysAddr_Check = { * return Some(exception) to abort the read or None to allow it to proceed. The * check is performed after PMP checks and does not apply to MMIO memory. */ -val ext_check_phys_mem_read : forall 'n, 0 < 'n <= max_mem_access . (AccessType (ext_access_type), xlenbits, atom('n), bool, bool, bool, bool) -> Ext_PhysAddr_Check +val ext_check_phys_mem_read : forall 'n, 0 < 'n <= max_mem_access . (AccessType (ext_access_type), xlenbits, int('n), bool, bool, bool, bool) -> Ext_PhysAddr_Check /*! * Validate a write to physical memory. @@ -48,4 +48,4 @@ val ext_check_phys_mem_read : forall 'n, 0 < 'n <= max_mem_access . (AccessType * to abort the write or None to allow it to proceed. The check is performed * after PMP checks and does not apply to MMIO memory. */ -val ext_check_phys_mem_write : forall 'n, 0 < 'n <= max_mem_access . (write_kind, xlenbits, atom('n), bits(8 * 'n), mem_meta) -> Ext_PhysAddr_Check +val ext_check_phys_mem_write : forall 'n, 0 < 'n <= max_mem_access . (write_kind, xlenbits, int('n), bits(8 * 'n), mem_meta) -> Ext_PhysAddr_Check diff --git a/model/riscv_mem.sail b/model/riscv_mem.sail index e51283484..a5fd8f7d1 100644 --- a/model/riscv_mem.sail +++ b/model/riscv_mem.sail @@ -35,7 +35,7 @@ * per the platform memory map. */ -function is_aligned_addr forall 'n. (addr : xlenbits, width : atom('n)) -> bool = +function is_aligned_addr forall 'n. (addr : xlenbits, width : int('n)) -> bool = unsigned(addr) % width == 0 function read_kind_of_flags (aq : bool, rl : bool, res : bool) -> option(read_kind) = @@ -51,7 +51,7 @@ function read_kind_of_flags (aq : bool, rl : bool, res : bool) -> option(read_ki } // only used for actual memory regions, to avoid MMIO effects -function phys_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), paddr : xlenbits, width : atom('n), aq : bool, rl: bool, res : bool, meta : bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) = { +function phys_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), paddr : xlenbits, width : int('n), aq : bool, rl: bool, res : bool, meta : bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) = { let result = (match read_kind_of_flags(aq, rl, res) { Some(rk) => Some(read_ram(rk, paddr, width, meta)), None() => None() @@ -67,7 +67,7 @@ function phys_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext } /* dispatches to MMIO regions or physical memory regions depending on physical memory map */ -function checked_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), paddr : xlenbits, width : atom('n), aq : bool, rl : bool, res: bool, meta : bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) = +function checked_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), paddr : xlenbits, width : int('n), aq : bool, rl : bool, res: bool, meta : bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) = if within_mmio_readable(paddr, width) then MemoryOpResult_add_meta(mmio_read(t, paddr, width), default_meta) else if within_phys_mem(paddr, width) @@ -81,7 +81,7 @@ function checked_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType( } /* PMP checks if enabled */ -function pmp_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), p : Privilege, paddr : xlenbits, width : atom('n), aq : bool, rl : bool, res: bool, meta : bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) = +function pmp_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), p : Privilege, paddr : xlenbits, width : int('n), aq : bool, rl : bool, res: bool, meta : bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) = if sys_pmp_count() == 0 then checked_mem_read(t, paddr, width, aq, rl, res, meta) else { @@ -94,7 +94,7 @@ function pmp_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_ /* Atomic accesses can be done to MMIO regions, e.g. in kernel access to device registers. */ $ifdef RVFI_DII -val rvfi_read : forall 'n, 'n > 0. (xlenbits, atom('n), MemoryOpResult((bits(8 * 'n), mem_meta))) -> unit +val rvfi_read : forall 'n, 'n > 0. (xlenbits, int('n), MemoryOpResult((bits(8 * 'n), mem_meta))) -> unit function rvfi_read (addr, width, result) = { rvfi_mem_data[rvfi_mem_addr] = zero_extend(addr); rvfi_mem_data_present = true; @@ -108,21 +108,21 @@ function rvfi_read (addr, width, result) = { }; } $else -val rvfi_read : forall 'n, 'n > 0. (xlenbits, atom('n), MemoryOpResult((bits(8 * 'n), mem_meta))) -> unit +val rvfi_read : forall 'n, 'n > 0. (xlenbits, int('n), MemoryOpResult((bits(8 * 'n), mem_meta))) -> unit function rvfi_read (addr, width, result) = () $endif /* NOTE: The rreg effect is due to MMIO. */ $ifdef RVFI_DII -val mem_read : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) -val mem_read_priv : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), Privilege, xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) -val mem_read_meta : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool, bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) -val mem_read_priv_meta : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), Privilege, xlenbits, atom('n), bool, bool, bool, bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) +val mem_read : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, int('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) +val mem_read_priv : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), Privilege, xlenbits, int('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) +val mem_read_meta : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, int('n), bool, bool, bool, bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) +val mem_read_priv_meta : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), Privilege, xlenbits, int('n), bool, bool, bool, bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) $else -val mem_read : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) -val mem_read_priv : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), Privilege, xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) -val mem_read_meta : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool, bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) -val mem_read_priv_meta : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), Privilege, xlenbits, atom('n), bool, bool, bool, bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) +val mem_read : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, int('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) +val mem_read_priv : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), Privilege, xlenbits, int('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) +val mem_read_meta : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, int('n), bool, bool, bool, bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) +val mem_read_priv_meta : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), Privilege, xlenbits, int('n), bool, bool, bool, bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) $endif /* The most generic memory read operation */ @@ -150,7 +150,7 @@ function mem_read_priv (typ, priv, paddr, width, aq, rl, res) = function mem_read (typ, paddr, width, aq, rel, res) = mem_read_priv(typ, effectivePrivilege(typ, mstatus, cur_privilege), paddr, width, aq, rel, res) -val mem_write_ea : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(unit) +val mem_write_ea : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, int('n), bool, bool, bool) -> MemoryOpResult(unit) function mem_write_ea (addr, width, aq, rl, con) = { if (rl | con) & not(is_aligned_addr(addr, width)) @@ -168,7 +168,7 @@ function mem_write_ea (addr, width, aq, rl, con) = { } $ifdef RVFI_DII -val rvfi_write : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bits(8 * 'n), mem_meta, MemoryOpResult(bool)) -> unit +val rvfi_write : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, int('n), bits(8 * 'n), mem_meta, MemoryOpResult(bool)) -> unit function rvfi_write (addr, width, value, meta, result) = { rvfi_mem_data[rvfi_mem_addr] = zero_extend(addr); rvfi_mem_data_present = true; @@ -185,12 +185,12 @@ function rvfi_write (addr, width, value, meta, result) = { } } $else -val rvfi_write : forall 'n, 'n > 0. (xlenbits, atom('n), bits(8 * 'n), mem_meta, MemoryOpResult(bool)) -> unit +val rvfi_write : forall 'n, 'n > 0. (xlenbits, int('n), bits(8 * 'n), mem_meta, MemoryOpResult(bool)) -> unit function rvfi_write (addr, width, value, meta, result) = () $endif // only used for actual memory regions, to avoid MMIO effects -function phys_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk : write_kind, paddr : xlenbits, width : atom('n), data : bits(8 * 'n), meta : mem_meta) -> MemoryOpResult(bool) = { +function phys_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk : write_kind, paddr : xlenbits, width : int('n), data : bits(8 * 'n), meta : mem_meta) -> MemoryOpResult(bool) = { let result = MemValue(write_ram(wk, paddr, width, data, meta)); if get_config_print_mem() then print_mem("mem[" ^ BitStr(paddr) ^ "] <- " ^ BitStr(data)); @@ -198,7 +198,7 @@ function phys_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk : write_kind, } /* dispatches to MMIO regions or physical memory regions depending on physical memory map */ -function checked_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk : write_kind, paddr : xlenbits, width : atom('n), data: bits(8 * 'n), meta: mem_meta) -> MemoryOpResult(bool) = +function checked_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk : write_kind, paddr : xlenbits, width : int('n), data: bits(8 * 'n), meta: mem_meta) -> MemoryOpResult(bool) = if within_mmio_writable(paddr, width) then mmio_write(paddr, width, data) else if within_phys_mem(paddr, width) @@ -209,7 +209,7 @@ function checked_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk : write_kin else MemException(E_SAMO_Access_Fault()) /* PMP checks if enabled */ -function pmp_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk: write_kind, paddr : xlenbits, width : atom('n), data: bits(8 * 'n), typ: AccessType(ext_access_type), priv: Privilege, meta: mem_meta) -> MemoryOpResult(bool) = +function pmp_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk: write_kind, paddr : xlenbits, width : int('n), data: bits(8 * 'n), typ: AccessType(ext_access_type), priv: Privilege, meta: mem_meta) -> MemoryOpResult(bool) = if sys_pmp_count() == 0 then checked_mem_write(wk, paddr, width, data, meta) else { @@ -226,7 +226,7 @@ function pmp_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk: write_kind, pa * data. * NOTE: The wreg effect is due to MMIO, the rreg is due to checking mtime. */ -val mem_write_value_priv_meta : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bits(8 * 'n), AccessType(ext_access_type), Privilege, mem_meta, bool, bool, bool) -> MemoryOpResult(bool) +val mem_write_value_priv_meta : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, int('n), bits(8 * 'n), AccessType(ext_access_type), Privilege, mem_meta, bool, bool, bool) -> MemoryOpResult(bool) function mem_write_value_priv_meta (paddr, width, value, typ, priv, meta, aq, rl, con) = { if (rl | con) & not(is_aligned_addr(paddr, width)) then MemException(E_SAMO_Addr_Align()) @@ -249,12 +249,12 @@ function mem_write_value_priv_meta (paddr, width, value, typ, priv, meta, aq, rl } /* Memory write with explicit Privilege, implicit AccessType and metadata */ -val mem_write_value_priv : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bits(8 * 'n), Privilege, bool, bool, bool) -> MemoryOpResult(bool) +val mem_write_value_priv : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, int('n), bits(8 * 'n), Privilege, bool, bool, bool) -> MemoryOpResult(bool) function mem_write_value_priv (paddr, width, value, priv, aq, rl, con) = mem_write_value_priv_meta(paddr, width, value, Write(default_write_acc), priv, default_meta, aq, rl, con) /* Memory write with explicit metadata and AccessType, implicit and Privilege */ -val mem_write_value_meta : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bits(8 * 'n), ext_access_type, mem_meta, bool, bool, bool) -> MemoryOpResult(bool) +val mem_write_value_meta : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, int('n), bits(8 * 'n), ext_access_type, mem_meta, bool, bool, bool) -> MemoryOpResult(bool) function mem_write_value_meta (paddr, width, value, ext_acc, meta, aq, rl, con) = { let typ = Write(ext_acc); let ep = effectivePrivilege(typ, mstatus, cur_privilege); @@ -262,7 +262,7 @@ function mem_write_value_meta (paddr, width, value, ext_acc, meta, aq, rl, con) } /* Memory write with default AccessType, Privilege, and metadata */ -val mem_write_value : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bits(8 * 'n), bool, bool, bool) -> MemoryOpResult(bool) +val mem_write_value : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, int('n), bits(8 * 'n), bool, bool, bool) -> MemoryOpResult(bool) function mem_write_value (paddr, width, value, aq, rl, con) = { mem_write_value_meta(paddr, width, value, default_write_acc, default_meta, aq, rl, con) } diff --git a/model/riscv_platform.sail b/model/riscv_platform.sail index 9f38090a6..19e3d30ae 100644 --- a/model/riscv_platform.sail +++ b/model/riscv_platform.sail @@ -71,7 +71,7 @@ function phys_mem_segments() = /* Physical memory map predicates */ -function within_phys_mem forall 'n, 'n <= max_mem_access. (addr : xlenbits, width : atom('n)) -> bool = { +function within_phys_mem forall 'n, 'n <= max_mem_access. (addr : xlenbits, width : int('n)) -> bool = { /* To avoid overflow issues when physical memory extends to the end * of the addressable range, we need to perform address bound checks * on unsigned unbounded integers. @@ -99,7 +99,7 @@ function within_phys_mem forall 'n, 'n <= max_mem_access. (addr : xlenbits, widt } } -function within_clint forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : atom('n)) -> bool = { +function within_clint forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : int('n)) -> bool = { /* To avoid overflow issues when physical memory extends to the end * of the addressable range, we need to perform address bound checks * on unsigned unbounded integers. @@ -111,10 +111,10 @@ function within_clint forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, wi & (addr_int + sizeof('n)) <= (clint_base_int + clint_size_int) } -function within_htif_writable forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : atom('n)) -> bool = +function within_htif_writable forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : int('n)) -> bool = plat_htif_tohost() == addr | (plat_htif_tohost() + 4 == addr & width == 4) -function within_htif_readable forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : atom('n)) -> bool = +function within_htif_readable forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : int('n)) -> bool = plat_htif_tohost() == addr | (plat_htif_tohost() + 4 == addr & width == 4) /* CLINT (Core Local Interruptor), based on Spike. */ @@ -385,20 +385,20 @@ function htif_tick() = { /* Top-level MMIO dispatch */ $ifndef RVFI_DII -function within_mmio_readable forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : atom('n)) -> bool = +function within_mmio_readable forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : int('n)) -> bool = within_clint(addr, width) | (within_htif_readable(addr, width) & 1 <= 'n) $else -function within_mmio_readable forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : atom('n)) -> bool = false +function within_mmio_readable forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : int('n)) -> bool = false $endif $ifndef RVFI_DII -function within_mmio_writable forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : atom('n)) -> bool = +function within_mmio_writable forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : int('n)) -> bool = within_clint(addr, width) | (within_htif_writable(addr, width) & 'n <= 8) $else -function within_mmio_writable forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : atom('n)) -> bool = false +function within_mmio_writable forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : int('n)) -> bool = false $endif -function mmio_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), paddr : xlenbits, width : atom('n)) -> MemoryOpResult(bits(8 * 'n)) = +function mmio_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), paddr : xlenbits, width : int('n)) -> MemoryOpResult(bits(8 * 'n)) = if within_clint(paddr, width) then clint_load(t, paddr, width) else if within_htif_readable(paddr, width) & (1 <= 'n) @@ -409,7 +409,7 @@ function mmio_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_acc _ => MemException(E_SAMO_Access_Fault()) } -function mmio_write forall 'n, 0 <'n <= max_mem_access . (paddr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> MemoryOpResult(bool) = +function mmio_write forall 'n, 0 <'n <= max_mem_access . (paddr : xlenbits, width : int('n), data: bits(8 * 'n)) -> MemoryOpResult(bool) = if within_clint(paddr, width) then clint_store(paddr, width, data) else if within_htif_writable(paddr, width) & 'n <= 8 diff --git a/model/riscv_pmp_control.sail b/model/riscv_pmp_control.sail index 4242968d8..1e4cb77de 100644 --- a/model/riscv_pmp_control.sail +++ b/model/riscv_pmp_control.sail @@ -104,7 +104,7 @@ function accessToFault(acc : AccessType(ext_access_type)) -> ExceptionType = Execute() => E_Fetch_Access_Fault(), } -function pmpCheck forall 'n, 'n > 0. (addr: xlenbits, width: atom('n), acc: AccessType(ext_access_type), priv: Privilege) +function pmpCheck forall 'n, 'n > 0. (addr: xlenbits, width: int('n), acc: AccessType(ext_access_type), priv: Privilege) -> option(ExceptionType) = { let width : xlenbits = to_bits(sizeof(xlen), width); diff --git a/model/riscv_types.sail b/model/riscv_types.sail index d26f79b43..0e23d63d1 100644 --- a/model/riscv_types.sail +++ b/model/riscv_types.sail @@ -28,7 +28,7 @@ type csreg = bits(12) /* CSR addressing */ /* register file indexing */ -type regno ('n : Int), 0 <= 'n < 32 = atom('n) +type regno ('n : Int), 0 <= 'n < 32 = int('n) val regidx_to_regno : bits(5) -> {'n, 0 <= 'n < 32. regno('n)} function regidx_to_regno b = let 'r = unsigned(b) in r @@ -381,7 +381,7 @@ mapping size_mnemonic : word_width <-> string = { DOUBLE <-> "d" } -val word_width_bytes : word_width -> {'s, 's == 1 | 's == 2 | 's == 4 | 's == 8 . atom('s)} +val word_width_bytes : word_width -> {'s, 's == 1 | 's == 2 | 's == 4 | 's == 8 . int('s)} function word_width_bytes width = match width { BYTE => 1, HALF => 2, diff --git a/model/rvfi_dii.sail b/model/rvfi_dii.sail index 7ebc8a837..d1ad480df 100644 --- a/model/rvfi_dii.sail +++ b/model/rvfi_dii.sail @@ -298,7 +298,7 @@ function rvfi_get_mem_data () = { return rvfi_mem_data.bits; } -val rvfi_encode_width_mask : forall 'n, 0 < 'n <= 32. atom('n) -> bits(32) +val rvfi_encode_width_mask : forall 'n, 0 < 'n <= 32. int('n) -> bits(32) function rvfi_encode_width_mask(width) = (0xFFFFFFFF >> (32 - width))