From 4c77f62622c199f14e0bd6cdc6a6c427fe31b09e Mon Sep 17 00:00:00 2001 From: Tim Hutt Date: Fri, 11 Aug 2023 16:00:51 +0100 Subject: [PATCH] Remove effects Since Sail 0.15 (released Nov 2022), effects have had no effect. They now generate a deprecation warning. This commit removes all the effect annotations from the model, thus fixing the compiler warnings. --- model/prelude.sail | 2 +- model/prelude_mem.sail | 6 +- model/prelude_mem_metadata.sail | 4 +- model/riscv_csr_map.sail | 6 +- model/riscv_decode_ext.sail | 4 +- model/riscv_ext_regs.sail | 4 +- model/riscv_fdext_control.sail | 2 +- model/riscv_fdext_regs.sail | 40 ++++---- model/riscv_fetch.sail | 2 +- model/riscv_insts_aext.sail | 2 +- model/riscv_insts_base.sail | 2 +- model/riscv_insts_begin.sail | 6 +- model/riscv_insts_fext.sail | 10 +- model/riscv_mem.sail | 30 +++--- model/riscv_pc_access.sail | 8 +- model/riscv_platform.sail | 12 +-- model/riscv_pmp_regs.sail | 4 +- model/riscv_regs.sail | 8 +- model/riscv_softfloat_interface.sail | 134 +++++++++++++-------------- model/riscv_step_rvfi.sail | 2 +- model/riscv_sys_control.sail | 4 +- model/riscv_sys_exceptions.sail | 6 +- model/riscv_sys_regs.sail | 2 +- model/riscv_types.sail | 6 +- model/riscv_types_kext.sail | 2 +- model/riscv_vmem_rv32.sail | 8 +- model/riscv_vmem_rv64.sail | 8 +- model/riscv_vmem_sv32.sail | 10 +- model/riscv_vmem_sv39.sail | 10 +- model/riscv_vmem_sv48.sail | 10 +- model/riscv_vmem_tlb.sail | 2 +- model/rvfi_dii.sail | 22 ++--- 32 files changed, 189 insertions(+), 189 deletions(-) diff --git a/model/prelude.sail b/model/prelude.sail index e51bca213..bec76d645 100644 --- a/model/prelude.sail +++ b/model/prelude.sail @@ -87,7 +87,7 @@ val eq_anything = {ocaml: "(fun (x, y) -> x = y)", interpreter: "eq_anything", l overload operator == = {eq_string, eq_anything} -val "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg} +val "reg_deref" : forall ('a : Type). register('a) -> 'a /* sneaky deref with no effect necessary for bitfield writes */ val _reg_deref = "reg_deref" : forall ('a : Type). register('a) -> 'a diff --git a/model/prelude_mem.sail b/model/prelude_mem.sail index 1b27d495a..3bbf437ac 100644 --- a/model/prelude_mem.sail +++ b/model/prelude_mem.sail @@ -89,7 +89,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 effect {wmv, wmvt} +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 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; @@ -103,11 +103,11 @@ 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 effect {eamem} +val write_ram_ea : forall 'n, 0 < 'n <= max_mem_access . (write_kind, xlenbits, atom('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) effect {rmem, rmemt} +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) 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) diff --git a/model/prelude_mem_metadata.sail b/model/prelude_mem_metadata.sail index e714189c4..919cee374 100644 --- a/model/prelude_mem_metadata.sail +++ b/model/prelude_mem_metadata.sail @@ -76,8 +76,8 @@ type mem_meta = unit let default_meta : mem_meta = () -val __WriteRAM_Meta : forall 'n. (xlenbits, atom('n), mem_meta) -> unit effect {wmvt} +val __WriteRAM_Meta : forall 'n. (xlenbits, atom('n), mem_meta) -> unit function __WriteRAM_Meta(addr, width, meta) = () -val __ReadRAM_Meta : forall 'n. (xlenbits, atom('n)) -> mem_meta effect {rmem} +val __ReadRAM_Meta : forall 'n. (xlenbits, atom('n)) -> mem_meta function __ReadRAM_Meta(addr, width) = () diff --git a/model/riscv_csr_map.sail b/model/riscv_csr_map.sail index e3f8f5bb8..e3c1c20b9 100644 --- a/model/riscv_csr_map.sail +++ b/model/riscv_csr_map.sail @@ -180,13 +180,13 @@ overload to_str = {csr_name} /* returns whether a CSR is defined and accessible at a given address * and privilege */ -val ext_is_CSR_defined : (csreg, Privilege) -> bool effect {rreg} +val ext_is_CSR_defined : (csreg, Privilege) -> bool scattered function ext_is_CSR_defined /* returns the value of the CSR if it is defined */ -val ext_read_CSR : csreg -> option(xlenbits) effect {rreg} +val ext_read_CSR : csreg -> option(xlenbits) scattered function ext_read_CSR /* returns new value (after legalisation) if the CSR is defined */ -val ext_write_CSR : (csreg, xlenbits) -> option(xlenbits) effect {rreg, wreg, escape} +val ext_write_CSR : (csreg, xlenbits) -> option(xlenbits) scattered function ext_write_CSR diff --git a/model/riscv_decode_ext.sail b/model/riscv_decode_ext.sail index b6b4bb86c..b215109ea 100644 --- a/model/riscv_decode_ext.sail +++ b/model/riscv_decode_ext.sail @@ -73,8 +73,8 @@ hooks, the default implementation of which is provided below. */ -val ext_decode_compressed : bits(16) -> ast effect {rreg} +val ext_decode_compressed : bits(16) -> ast function ext_decode_compressed(bv) = encdec_compressed(bv) -val ext_decode : bits(32) -> ast effect {rreg} +val ext_decode : bits(32) -> ast function ext_decode(bv) = encdec(bv) diff --git a/model/riscv_ext_regs.sail b/model/riscv_ext_regs.sail index 1ff956efa..8568e6a39 100644 --- a/model/riscv_ext_regs.sail +++ b/model/riscv_ext_regs.sail @@ -72,7 +72,7 @@ * overridden by extensions. */ -val ext_init_regs : unit -> unit effect {wreg} +val ext_init_regs : unit -> unit function ext_init_regs () = () /*! @@ -80,7 +80,7 @@ This function is called after above when running rvfi and allows the model to be initialised differently (e.g. CHERI cap regs are initialised to omnipotent instead of null). */ -val ext_rvfi_init : unit -> unit effect {rreg, wreg} +val ext_rvfi_init : unit -> unit function ext_rvfi_init () = { x1 = x1 // to avoid hook being optimized out } diff --git a/model/riscv_fdext_control.sail b/model/riscv_fdext_control.sail index 768aede02..563d60088 100644 --- a/model/riscv_fdext_control.sail +++ b/model/riscv_fdext_control.sail @@ -77,7 +77,7 @@ /* **************************************************************** */ -/* val clause ext_is_CSR_defined : (csreg, Privilege) -> bool effect {rreg} */ +/* val clause ext_is_CSR_defined : (csreg, Privilege) -> bool */ function clause ext_is_CSR_defined (0x001, _) = haveFExt() | haveZfinx() function clause ext_is_CSR_defined (0x002, _) = haveFExt() | haveZfinx() diff --git a/model/riscv_fdext_regs.sail b/model/riscv_fdext_regs.sail index f2e0fb33c..6a40606cf 100644 --- a/model/riscv_fdext_regs.sail +++ b/model/riscv_fdext_regs.sail @@ -106,7 +106,7 @@ function nan_unbox_H regval = then regval [15..0] else canonical_NaN_H() -val nan_box_S : bits(32) -> flenbits effect {escape} +val nan_box_S : bits(32) -> flenbits function nan_box_S val_32b = { assert(sys_enable_fdext()); if (sizeof(flen) == 32) @@ -114,7 +114,7 @@ function nan_box_S val_32b = { else 0x_FFFF_FFFF @ val_32b } -val nan_unbox_S : flenbits -> bits(32) effect {escape} +val nan_unbox_S : flenbits -> bits(32) function nan_unbox_S regval = { assert(sys_enable_fdext()); if (sizeof(flen) == 32) @@ -174,7 +174,7 @@ function dirty_fd_context_if_present() -> unit = { if sys_enable_fdext() then dirty_fd_context() } -val rF : forall 'n, 0 <= 'n < 32. regno('n) -> flenbits effect {rreg, escape} +val rF : forall 'n, 0 <= 'n < 32. regno('n) -> flenbits function rF r = { assert(sys_enable_fdext()); let v : fregtype = @@ -216,7 +216,7 @@ function rF r = { fregval_from_freg(v) } -val wF : forall 'n, 0 <= 'n < 32. (regno('n), flenbits) -> unit effect {wreg, escape} +val wF : forall 'n, 0 <= 'n < 32. (regno('n), flenbits) -> unit function wF (r, in_v) = { assert(sys_enable_fdext()); let v = fregval_into_freg(in_v); @@ -272,42 +272,42 @@ function wF_bits(i: bits(5), data: flenbits) -> unit = { overload F = {rF_bits, wF_bits, rF, wF} -val rF_H : bits(5) -> bits(16) effect {escape, rreg} +val rF_H : bits(5) -> bits(16) function rF_H(i) = { assert(sizeof(flen) >= 16); assert(sys_enable_fdext() & not(sys_enable_zfinx())); nan_unbox(F(i)) } -val wF_H : (bits(5), bits(16)) -> unit effect {escape, wreg} +val wF_H : (bits(5), bits(16)) -> unit function wF_H(i, data) = { assert(sizeof(flen) >= 16); assert(sys_enable_fdext() & not(sys_enable_zfinx())); F(i) = nan_box(data) } -val rF_S : bits(5) -> bits(32) effect {escape, rreg} +val rF_S : bits(5) -> bits(32) function rF_S(i) = { assert(sizeof(flen) >= 32); assert(sys_enable_fdext() & not(sys_enable_zfinx())); nan_unbox(F(i)) } -val wF_S : (bits(5), bits(32)) -> unit effect {escape, wreg} +val wF_S : (bits(5), bits(32)) -> unit function wF_S(i, data) = { assert(sizeof(flen) >= 32); assert(sys_enable_fdext() & not(sys_enable_zfinx())); F(i) = nan_box(data) } -val rF_D : bits(5) -> bits(64) effect {escape, rreg} +val rF_D : bits(5) -> bits(64) function rF_D(i) = { assert(sizeof(flen) >= 64); assert(sys_enable_fdext() & not(sys_enable_zfinx())); F(i) } -val wF_D : (bits(5), bits(64)) -> unit effect {escape, wreg} +val wF_D : (bits(5), bits(64)) -> unit function wF_D(i, data) = { assert(sizeof(flen) >= 64); assert(sys_enable_fdext() & not(sys_enable_zfinx())); @@ -318,7 +318,7 @@ overload F_H = { rF_H, wF_H } overload F_S = { rF_S, wF_S } overload F_D = { rF_D, wF_D } -val rF_or_X_H : bits(5) -> bits(16) effect {escape, rreg} +val rF_or_X_H : bits(5) -> bits(16) function rF_or_X_H(i) = { assert(sizeof(flen) >= 16); assert(sys_enable_fdext() != sys_enable_zfinx()); @@ -327,7 +327,7 @@ function rF_or_X_H(i) = { else X(i)[15..0] } -val rF_or_X_S : bits(5) -> bits(32) effect {escape, rreg} +val rF_or_X_S : bits(5) -> bits(32) function rF_or_X_S(i) = { assert(sizeof(flen) >= 32); assert(sys_enable_fdext() != sys_enable_zfinx()); @@ -336,7 +336,7 @@ function rF_or_X_S(i) = { else X(i)[31..0] } -val rF_or_X_D : bits(5) -> bits(64) effect {escape, rreg} +val rF_or_X_D : bits(5) -> bits(64) function rF_or_X_D(i) = { assert(sizeof(flen) >= 64); assert(sys_enable_fdext() != sys_enable_zfinx()); @@ -350,7 +350,7 @@ function rF_or_X_D(i) = { } } -val wF_or_X_H : (bits(5), bits(16)) -> unit effect {escape, wreg} +val wF_or_X_H : (bits(5), bits(16)) -> unit function wF_or_X_H(i, data) = { assert(sizeof(flen) >= 16); assert(sys_enable_fdext() != sys_enable_zfinx()); @@ -359,7 +359,7 @@ function wF_or_X_H(i, data) = { else X(i) = sign_extend(data) } -val wF_or_X_S : (bits(5), bits(32)) -> unit effect {escape, wreg} +val wF_or_X_S : (bits(5), bits(32)) -> unit function wF_or_X_S(i, data) = { assert(sizeof(flen) >= 32); assert(sys_enable_fdext() != sys_enable_zfinx()); @@ -368,7 +368,7 @@ function wF_or_X_S(i, data) = { else X(i) = sign_extend(data) } -val wF_or_X_D : (bits(5), bits(64)) -> unit effect {escape, wreg} +val wF_or_X_D : (bits(5), bits(64)) -> unit function wF_or_X_D(i, data) = { assert (sizeof(flen) >= 64); assert(sys_enable_fdext() != sys_enable_zfinx()); @@ -474,7 +474,7 @@ mapping freg_or_reg_name = { reg if sys_enable_zfinx() <-> reg_name(reg) if sys_enable_zfinx() } -val init_fdext_regs : unit -> unit effect {wreg} +val init_fdext_regs : unit -> unit function init_fdext_regs () = { f0 = zero_freg; f1 = zero_freg; @@ -524,7 +524,7 @@ bitfield Fcsr : bits(32) = { register fcsr : Fcsr -val ext_write_fcsr : (bits(3), bits(5)) -> unit effect {rreg, wreg, escape} +val ext_write_fcsr : (bits(3), bits(5)) -> unit function ext_write_fcsr (frm, fflags) = { fcsr->FRM() = frm; /* Note: frm can be an illegal value, 101, 110, 111 */ fcsr->FFLAGS() = fflags; @@ -533,7 +533,7 @@ function ext_write_fcsr (frm, fflags) = { } /* called for softfloat paths (softfloat flags are consistent) */ -val write_fflags : (bits(5)) -> unit effect {rreg, wreg, escape} +val write_fflags : (bits(5)) -> unit function write_fflags(fflags) = { if fcsr.FFLAGS() != fflags then dirty_fd_context_if_present(); @@ -541,7 +541,7 @@ function write_fflags(fflags) = { } /* called for non-softfloat paths (softfloat flags need updating) */ -val accrue_fflags : (bits(5)) -> unit effect {rreg, wreg, escape} +val accrue_fflags : (bits(5)) -> unit function accrue_fflags(flags) = { let f = fcsr.FFLAGS() | flags; if fcsr.FFLAGS() != f diff --git a/model/riscv_fetch.sail b/model/riscv_fetch.sail index 7a083a772..4c54ccc9b 100644 --- a/model/riscv_fetch.sail +++ b/model/riscv_fetch.sail @@ -74,7 +74,7 @@ function isRVC(h : half) -> bool = not(h[1 .. 0] == 0b11) -val fetch : unit -> FetchResult effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg} +val fetch : unit -> FetchResult function fetch() -> FetchResult = /* fetch PC check for extensions: extensions return a transformed PC to fetch, * but any exceptions use the untransformed PC. diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail index b1bfcef88..6915f28d3 100644 --- a/model/riscv_insts_aext.sail +++ b/model/riscv_insts_aext.sail @@ -115,7 +115,7 @@ mapping clause encdec = LOADRES(aq, rl, rs1, size, rd) if amo_width_valid(size) * call to load_reservation in LR and cancel_reservation in SC. */ -val process_loadres : forall 'n, 0 < 'n <= xlen_bytes. (regidx, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> Retired effect {escape, rreg, wreg} +val process_loadres : forall 'n, 0 < 'n <= xlen_bytes. (regidx, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> Retired function process_loadres(rd, addr, value, is_unsigned) = match extend_value(is_unsigned, value) { MemValue(result) => { load_reservation(addr); X(rd) = result; RETIRE_SUCCESS }, diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail index d68e7a34f..b5e699e70 100644 --- a/model/riscv_insts_base.sail +++ b/model/riscv_insts_base.sail @@ -368,7 +368,7 @@ function extend_value(is_unsigned, value) = match (value) { MemException(e) => MemException(e) } -val process_load : forall 'n, 0 < 'n <= xlen_bytes. (regidx, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> Retired effect {escape, rreg, wreg} +val process_load : forall 'n, 0 < 'n <= xlen_bytes. (regidx, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> Retired function process_load(rd, vaddr, value, is_unsigned) = match extend_value(is_unsigned, value) { MemValue(result) => { X(rd) = result; RETIRE_SUCCESS }, diff --git a/model/riscv_insts_begin.sail b/model/riscv_insts_begin.sail index fae285cc5..dd7865f8c 100644 --- a/model/riscv_insts_begin.sail +++ b/model/riscv_insts_begin.sail @@ -76,16 +76,16 @@ scattered union ast /* returns whether an instruction was retired, used for computing minstret */ -val execute : ast -> Retired effect {escape, wreg, rreg, wmv, wmvt, eamem, rmem, rmemt, barr, exmem, undef} +val execute : ast -> Retired scattered function execute val assembly : ast <-> string scattered mapping assembly -val encdec : ast <-> bits(32) effect {rreg} +val encdec : ast <-> bits(32) scattered mapping encdec -val encdec_compressed : ast <-> bits(16) effect {rreg} +val encdec_compressed : ast <-> bits(16) scattered mapping encdec_compressed /* diff --git a/model/riscv_insts_fext.sail b/model/riscv_insts_fext.sail index e60b96b5d..67f34a7d6 100644 --- a/model/riscv_insts_fext.sail +++ b/model/riscv_insts_fext.sail @@ -108,7 +108,7 @@ mapping frm_mnemonic : rounding_mode <-> string = { val valid_rounding_mode : bits(3) -> bool function valid_rounding_mode rm = (rm != 0b101 & rm != 0b110) -val select_instr_or_fcsr_rm : rounding_mode -> option(rounding_mode) effect {rreg} +val select_instr_or_fcsr_rm : rounding_mode -> option(rounding_mode) function select_instr_or_fcsr_rm instr_rm = if (instr_rm == RM_DYN) then { @@ -345,7 +345,7 @@ mapping clause encdec = LOAD_FP(imm, rs1, rd, DOUBLE) if haveDExt() /* Execution semantics ================================ */ val process_fload64 : (regidx, xlenbits, MemoryOpResult(bits(64))) - -> Retired effect {escape, rreg, wreg} + -> Retired function process_fload64(rd, addr, value) = if sizeof(flen) == 64 then match value { @@ -358,7 +358,7 @@ function process_fload64(rd, addr, value) = } val process_fload32 : (regidx, xlenbits, MemoryOpResult(bits(32))) - -> Retired effect {escape, rreg, wreg} + -> Retired function process_fload32(rd, addr, value) = match value { MemValue(result) => { F(rd) = nan_box(result); RETIRE_SUCCESS }, @@ -366,7 +366,7 @@ function process_fload32(rd, addr, value) = } val process_fload16 : (regidx, xlenbits, MemoryOpResult(bits(16))) - -> Retired effect {escape, rreg, wreg} + -> Retired function process_fload16(rd, addr, value) = match value { MemValue(result) => { F(rd) = nan_box(result); RETIRE_SUCCESS }, @@ -430,7 +430,7 @@ mapping clause encdec = STORE_FP(imm7 @ imm5, rs2, rs1, DOUBLE) /* Execution semantics ================================ */ -val process_fstore : (xlenbits, MemoryOpResult(bool)) -> Retired effect {escape, rreg, wreg} +val process_fstore : (xlenbits, MemoryOpResult(bool)) -> Retired function process_fstore(vaddr, value) = match value { MemValue(true) => { RETIRE_SUCCESS }, diff --git a/model/riscv_mem.sail b/model/riscv_mem.sail index 147258908..0f36deef5 100644 --- a/model/riscv_mem.sail +++ b/model/riscv_mem.sail @@ -156,7 +156,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 effect {wreg} +val rvfi_read : forall 'n, 'n > 0. (xlenbits, atom('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; @@ -176,15 +176,15 @@ $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)) effect {wreg, rmem, rmemt, rreg, escape} -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)) effect {wreg, rmem, rmemt, rreg, escape} -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)) effect {wreg, rmem, rmemt, rreg, escape} -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)) effect {wreg, rmem, rmemt, rreg, escape} +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)) $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)) effect {rmem, rmemt, rreg, escape} -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)) effect {rmem, rmemt, rreg, escape} -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)) effect {rmem, rmemt, rreg, escape} -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)) effect {rmem, rmemt, rreg, escape} +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)) $endif /* The most generic memory read operation */ @@ -212,7 +212,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) effect {eamem, escape} +val mem_write_ea : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(unit) function mem_write_ea (addr, width, aq, rl, con) = { if (rl | con) & not(is_aligned_addr(addr, width)) @@ -230,7 +230,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 effect {wreg} +val rvfi_write : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('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; @@ -288,7 +288,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) effect {wmv, wmvt, rreg, wreg, escape} +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) 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()) @@ -311,12 +311,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) effect {wmv, wmvt, rreg, wreg, escape} +val mem_write_value_priv : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('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) effect {wmv, wmvt, rreg, wreg, escape} +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) 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); @@ -324,7 +324,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) effect {wmv, wmvt, rreg, wreg, escape} +val mem_write_value : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('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_pc_access.sail b/model/riscv_pc_access.sail index 9c3c742f5..dee566a2f 100644 --- a/model/riscv_pc_access.sail +++ b/model/riscv_pc_access.sail @@ -76,18 +76,18 @@ The value in the PC register is the absolute virtual address of the instruction to fetch. */ -val get_arch_pc : unit -> xlenbits effect {rreg} +val get_arch_pc : unit -> xlenbits function get_arch_pc() = PC -val get_next_pc : unit -> xlenbits effect {rreg} +val get_next_pc : unit -> xlenbits function get_next_pc() = nextPC -val set_next_pc : xlenbits -> unit effect {wreg} +val set_next_pc : xlenbits -> unit function set_next_pc(pc) = { nextPC = pc } -val tick_pc : unit -> unit effect {rreg, wreg} +val tick_pc : unit -> unit function tick_pc() = { PC = nextPC } diff --git a/model/riscv_platform.sail b/model/riscv_platform.sail index 6194b8f9c..579a118b6 100644 --- a/model/riscv_platform.sail +++ b/model/riscv_platform.sail @@ -212,7 +212,7 @@ let MTIMECMP_BASE_HI : xlenbits = zero_extend(0x04004) let MTIME_BASE : xlenbits = zero_extend(0x0bff8) let MTIME_BASE_HI : xlenbits = zero_extend(0x0bffc) -val clint_load : forall 'n, 'n > 0. (AccessType(ext_access_type), xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rreg} +val clint_load : forall 'n, 'n > 0. (AccessType(ext_access_type), xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n)) function clint_load(t, addr, width) = { let addr = addr - plat_clint_base (); /* FIXME: For now, only allow exact aligned access. */ @@ -284,7 +284,7 @@ function clint_dispatch() -> unit = { } /* The rreg effect is due to checking mtime. */ -val clint_store: forall 'n, 'n > 0. (xlenbits, int('n), bits(8 * 'n)) -> MemoryOpResult(bool) effect {rreg,wreg} +val clint_store: forall 'n, 'n > 0. (xlenbits, int('n), bits(8 * 'n)) -> MemoryOpResult(bool) function clint_store(addr, width, data) = { let addr = addr - plat_clint_base (); if addr == MSIP_BASE & ('n == 8 | 'n == 4) then { @@ -318,7 +318,7 @@ function clint_store(addr, width, data) = { } } -val tick_clock : unit -> unit effect {rreg, wreg} +val tick_clock : unit -> unit function tick_clock() = { if mcountinhibit.CY() == 0b0 then mcycle = mcycle + 1; @@ -367,7 +367,7 @@ function reset_htif () -> unit = { * dispatched the address. */ -val htif_load : forall 'n, 'n > 0. (AccessType(ext_access_type), xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rreg} +val htif_load : forall 'n, 'n > 0. (AccessType(ext_access_type), xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n)) function htif_load(t, paddr, width) = { if get_config_print_platform() then print_platform("htif[" ^ BitStr(paddr) ^ "] -> " ^ BitStr(htif_tohost)); @@ -386,7 +386,7 @@ function htif_load(t, paddr, width) = { } /* The rreg,wreg effects are an artifact of using 'register' to implement device state. */ -val htif_store: forall 'n, 0 < 'n <= 8. (xlenbits, int('n), bits(8 * 'n)) -> MemoryOpResult(bool) effect {rreg,wreg} +val htif_store: forall 'n, 0 < 'n <= 8. (xlenbits, int('n), bits(8 * 'n)) -> MemoryOpResult(bool) function htif_store(paddr, width, data) = { if get_config_print_platform() then print_platform("htif[" ^ BitStr(paddr) ^ "] <- " ^ BitStr(data)); @@ -444,7 +444,7 @@ function htif_store(paddr, width, data) = { MemValue(true) } -val htif_tick : unit -> unit effect {rreg, wreg} +val htif_tick : unit -> unit function htif_tick() = { if get_config_print_platform() then print_platform("htif::tick " ^ BitStr(htif_tohost)); diff --git a/model/riscv_pmp_regs.sail b/model/riscv_pmp_regs.sail index d02200669..9b6355ca6 100644 --- a/model/riscv_pmp_regs.sail +++ b/model/riscv_pmp_regs.sail @@ -140,7 +140,7 @@ register pmpaddr15 : xlenbits /* Packing and unpacking pmpcfg regs for xlen-width accesses */ -val pmpReadCfgReg : forall 'n, 0 <= 'n < 4 . (atom('n)) -> xlenbits effect {rreg} +val pmpReadCfgReg : forall 'n, 0 <= 'n < 4 . (atom('n)) -> xlenbits function pmpReadCfgReg(n) = { if sizeof(xlen) == 32 then match n { @@ -168,7 +168,7 @@ function pmpWriteCfg(cfg: Pmpcfg_ent, v: bits(8)) -> Pmpcfg_ent = if pmpLocked(cfg) then cfg else Mk_Pmpcfg_ent(v & 0x9f) // Bits 5 and 6 are zero. -val pmpWriteCfgReg : forall 'n, 0 <= 'n < 4 . (atom('n), xlenbits) -> unit effect {rreg, wreg} +val pmpWriteCfgReg : forall 'n, 0 <= 'n < 4 . (atom('n), xlenbits) -> unit function pmpWriteCfgReg(n, v) = { if sizeof(xlen) == 32 then match n { diff --git a/model/riscv_regs.sail b/model/riscv_regs.sail index ec4a2c63e..15e7613f0 100644 --- a/model/riscv_regs.sail +++ b/model/riscv_regs.sail @@ -110,7 +110,7 @@ register x29 : regtype register x30 : regtype register x31 : regtype -val rX : forall 'n, 0 <= 'n < 32. regno('n) -> xlenbits effect {rreg, escape} +val rX : forall 'n, 0 <= 'n < 32. regno('n) -> xlenbits function rX r = { let v : regtype = match r { @@ -152,7 +152,7 @@ function rX r = { } $ifdef RVFI_DII -val rvfi_wX : forall 'n, 0 <= 'n < 32. (regno('n), xlenbits) -> unit effect {wreg} +val rvfi_wX : forall 'n, 0 <= 'n < 32. (regno('n), xlenbits) -> unit function rvfi_wX (r,v) = { rvfi_int_data->rvfi_rd_wdata() = zero_extend(v); rvfi_int_data->rvfi_rd_addr() = to_bits(8,r); @@ -163,7 +163,7 @@ val rvfi_wX : forall 'n, 0 <= 'n < 32. (regno('n), xlenbits) -> unit function rvfi_wX (r,v) = () $endif -val wX : forall 'n, 0 <= 'n < 32. (regno('n), xlenbits) -> unit effect {wreg, escape} +val wX : forall 'n, 0 <= 'n < 32. (regno('n), xlenbits) -> unit function wX (r, in_v) = { let v = regval_into_reg(in_v); match r { @@ -308,7 +308,7 @@ mapping creg_name : bits(3) <-> string = { 0b111 <-> "a5" } -val init_base_regs : unit -> unit effect {wreg} +val init_base_regs : unit -> unit function init_base_regs () = { x1 = zero_reg; x2 = zero_reg; diff --git a/model/riscv_softfloat_interface.sail b/model/riscv_softfloat_interface.sail index 3be28c8c0..b98c44465 100644 --- a/model/riscv_softfloat_interface.sail +++ b/model/riscv_softfloat_interface.sail @@ -107,7 +107,7 @@ register float_result : bits(64) register float_fflags : bits(64) /* updater to keep the flags in sync with fcsr.fflags */ -val update_softfloat_fflags : bits(5) -> unit effect {wreg} +val update_softfloat_fflags : bits(5) -> unit function update_softfloat_fflags(flags) = { float_fflags = sail_zero_extend(flags, 64); } @@ -116,84 +116,84 @@ function update_softfloat_fflags(flags) = { /* ADD/SUB/MUL/DIV */ val extern_f16Add = {c: "softfloat_f16add", ocaml: "Softfloat.f16_add", lem: "softfloat_f16_add"} : (bits_rm, bits_H, bits_H) -> unit -val riscv_f16Add : (bits_rm, bits_H, bits_H) -> (bits_fflags, bits_H) effect {rreg} +val riscv_f16Add : (bits_rm, bits_H, bits_H) -> (bits_fflags, bits_H) function riscv_f16Add (rm, v1, v2) = { extern_f16Add(rm, v1, v2); (float_fflags[4 .. 0], float_result[15 .. 0]) } val extern_f16Sub = {c: "softfloat_f16sub", ocaml: "Softfloat.f16_sub", lem: "softfloat_f16_sub"} : (bits_rm, bits_H, bits_H) -> unit -val riscv_f16Sub : (bits_rm, bits_H, bits_H) -> (bits_fflags, bits_H) effect {rreg} +val riscv_f16Sub : (bits_rm, bits_H, bits_H) -> (bits_fflags, bits_H) function riscv_f16Sub (rm, v1, v2) = { extern_f16Sub(rm, v1, v2); (float_fflags[4 .. 0], float_result[15 .. 0]) } val extern_f16Mul = {c: "softfloat_f16mul", ocaml: "Softfloat.f16_mul", lem: "softfloat_f16_mul"} : (bits_rm, bits_H, bits_H) -> unit -val riscv_f16Mul : (bits_rm, bits_H, bits_H) -> (bits_fflags, bits_H) effect {rreg} +val riscv_f16Mul : (bits_rm, bits_H, bits_H) -> (bits_fflags, bits_H) function riscv_f16Mul (rm, v1, v2) = { extern_f16Mul(rm, v1, v2); (float_fflags[4 .. 0], float_result[15 .. 0]) } val extern_f16Div = {c: "softfloat_f16div", ocaml: "Softfloat.f16_div", lem: "softfloat_f16_div"} : (bits_rm, bits_H, bits_H) -> unit -val riscv_f16Div : (bits_rm, bits_H, bits_H) -> (bits_fflags, bits_H) effect {rreg} +val riscv_f16Div : (bits_rm, bits_H, bits_H) -> (bits_fflags, bits_H) function riscv_f16Div (rm, v1, v2) = { extern_f16Div(rm, v1, v2); (float_fflags[4 .. 0], float_result[15 .. 0]) } val extern_f32Add = {c: "softfloat_f32add", ocaml: "Softfloat.f32_add", lem: "softfloat_f32_add"} : (bits_rm, bits_S, bits_S) -> unit -val riscv_f32Add : (bits_rm, bits_S, bits_S) -> (bits_fflags, bits_S) effect {rreg} +val riscv_f32Add : (bits_rm, bits_S, bits_S) -> (bits_fflags, bits_S) function riscv_f32Add (rm, v1, v2) = { extern_f32Add(rm, v1, v2); (float_fflags[4 .. 0], float_result[31 .. 0]) } val extern_f32Sub = {c: "softfloat_f32sub", ocaml: "Softfloat.f32_sub", lem: "softfloat_f32_sub"} : (bits_rm, bits_S, bits_S) -> unit -val riscv_f32Sub : (bits_rm, bits_S, bits_S) -> (bits_fflags, bits_S) effect {rreg} +val riscv_f32Sub : (bits_rm, bits_S, bits_S) -> (bits_fflags, bits_S) function riscv_f32Sub (rm, v1, v2) = { extern_f32Sub(rm, v1, v2); (float_fflags[4 .. 0], float_result[31 .. 0]) } val extern_f32Mul = {c: "softfloat_f32mul", ocaml: "Softfloat.f32_mul", lem: "softfloat_f32_mul"} : (bits_rm, bits_S, bits_S) -> unit -val riscv_f32Mul : (bits_rm, bits_S, bits_S) -> (bits_fflags, bits_S) effect {rreg} +val riscv_f32Mul : (bits_rm, bits_S, bits_S) -> (bits_fflags, bits_S) function riscv_f32Mul (rm, v1, v2) = { extern_f32Mul(rm, v1, v2); (float_fflags[4 .. 0], float_result[31 .. 0]) } val extern_f32Div = {c: "softfloat_f32div", ocaml: "Softfloat.f32_div", lem: "softfloat_f32_div"} : (bits_rm, bits_S, bits_S) -> unit -val riscv_f32Div : (bits_rm, bits_S, bits_S) -> (bits_fflags, bits_S) effect {rreg} +val riscv_f32Div : (bits_rm, bits_S, bits_S) -> (bits_fflags, bits_S) function riscv_f32Div (rm, v1, v2) = { extern_f32Div(rm, v1, v2); (float_fflags[4 .. 0], float_result[31 .. 0]) } val extern_f64Add = {c: "softfloat_f64add", ocaml: "Softfloat.f64_add", lem: "softfloat_f64_add"} : (bits_rm, bits_D, bits_D) -> unit -val riscv_f64Add : (bits_rm, bits_D, bits_D) -> (bits_fflags, bits_D) effect {rreg} +val riscv_f64Add : (bits_rm, bits_D, bits_D) -> (bits_fflags, bits_D) function riscv_f64Add (rm, v1, v2) = { extern_f64Add(rm, v1, v2); (float_fflags[4 .. 0], float_result) } val extern_f64Sub = {c: "softfloat_f64sub", ocaml: "Softfloat.f64_sub", lem: "softfloat_f64_sub"} : (bits_rm, bits_D, bits_D) -> unit -val riscv_f64Sub : (bits_rm, bits_D, bits_D) -> (bits_fflags, bits_D) effect {rreg} +val riscv_f64Sub : (bits_rm, bits_D, bits_D) -> (bits_fflags, bits_D) function riscv_f64Sub (rm, v1, v2) = { extern_f64Sub(rm, v1, v2); (float_fflags[4 .. 0], float_result) } val extern_f64Mul = {c: "softfloat_f64mul", ocaml: "Softfloat.f64_mul", lem: "softfloat_f64_mul"} : (bits_rm, bits_D, bits_D) -> unit -val riscv_f64Mul : (bits_rm, bits_D, bits_D) -> (bits_fflags, bits_D) effect {rreg} +val riscv_f64Mul : (bits_rm, bits_D, bits_D) -> (bits_fflags, bits_D) function riscv_f64Mul (rm, v1, v2) = { extern_f64Mul(rm, v1, v2); (float_fflags[4 .. 0], float_result) } val extern_f64Div = {c: "softfloat_f64div", ocaml: "Softfloat.f64_div", lem: "softfloat_f64_div"} : (bits_rm, bits_D, bits_D) -> unit -val riscv_f64Div : (bits_rm, bits_D, bits_D) -> (bits_fflags, bits_D) effect {rreg} +val riscv_f64Div : (bits_rm, bits_D, bits_D) -> (bits_fflags, bits_D) function riscv_f64Div (rm, v1, v2) = { extern_f64Div(rm, v1, v2); (float_fflags[4 .. 0], float_result) @@ -203,21 +203,21 @@ function riscv_f64Div (rm, v1, v2) = { /* MULTIPLY-ADD */ val extern_f16MulAdd = {c: "softfloat_f16muladd", ocaml: "Softfloat.f16_muladd", lem: "softfloat_f16_muladd"} : (bits_rm, bits_H, bits_H, bits_H) -> unit -val riscv_f16MulAdd : (bits_rm, bits_H, bits_H, bits_H) -> (bits_fflags, bits_H) effect {rreg} +val riscv_f16MulAdd : (bits_rm, bits_H, bits_H, bits_H) -> (bits_fflags, bits_H) function riscv_f16MulAdd (rm, v1, v2, v3) = { extern_f16MulAdd(rm, v1, v2, v3); (float_fflags[4 .. 0], float_result[15 .. 0]) } val extern_f32MulAdd = {c: "softfloat_f32muladd", ocaml: "Softfloat.f32_muladd", lem: "softfloat_f32_muladd"} : (bits_rm, bits_S, bits_S, bits_S) -> unit -val riscv_f32MulAdd : (bits_rm, bits_S, bits_S, bits_S) -> (bits_fflags, bits_S) effect {rreg} +val riscv_f32MulAdd : (bits_rm, bits_S, bits_S, bits_S) -> (bits_fflags, bits_S) function riscv_f32MulAdd (rm, v1, v2, v3) = { extern_f32MulAdd(rm, v1, v2, v3); (float_fflags[4 .. 0], float_result[31 .. 0]) } val extern_f64MulAdd = {c: "softfloat_f64muladd", ocaml: "Softfloat.f64_muladd", lem: "softfloat_f64_muladd"} : (bits_rm, bits_D, bits_D, bits_D) -> unit -val riscv_f64MulAdd : (bits_rm, bits_D, bits_D, bits_D) -> (bits_fflags, bits_D) effect {rreg} +val riscv_f64MulAdd : (bits_rm, bits_D, bits_D, bits_D) -> (bits_fflags, bits_D) function riscv_f64MulAdd (rm, v1, v2, v3) = { extern_f64MulAdd(rm, v1, v2, v3); (float_fflags[4 .. 0], float_result) @@ -227,21 +227,21 @@ function riscv_f64MulAdd (rm, v1, v2, v3) = { /* SQUARE ROOT */ val extern_f16Sqrt = {c: "softfloat_f16sqrt", ocaml: "Softfloat.f16_sqrt", lem: "softfloat_f16_sqrt"} : (bits_rm, bits_H) -> unit -val riscv_f16Sqrt : (bits_rm, bits_H) -> (bits_fflags, bits_H) effect {rreg} +val riscv_f16Sqrt : (bits_rm, bits_H) -> (bits_fflags, bits_H) function riscv_f16Sqrt (rm, v) = { extern_f16Sqrt(rm, v); (float_fflags[4 .. 0], float_result[15 .. 0]) } val extern_f32Sqrt = {c: "softfloat_f32sqrt", ocaml: "Softfloat.f32_sqrt", lem: "softfloat_f32_sqrt"} : (bits_rm, bits_S) -> unit -val riscv_f32Sqrt : (bits_rm, bits_S) -> (bits_fflags, bits_S) effect {rreg} +val riscv_f32Sqrt : (bits_rm, bits_S) -> (bits_fflags, bits_S) function riscv_f32Sqrt (rm, v) = { extern_f32Sqrt(rm, v); (float_fflags[4 .. 0], float_result[31 .. 0]) } val extern_f64Sqrt = {c: "softfloat_f64sqrt", ocaml: "Softfloat.f64_sqrt", lem: "softfloat_f64_sqrt"} : (bits_rm, bits_D) -> unit -val riscv_f64Sqrt : (bits_rm, bits_D) -> (bits_fflags, bits_D) effect {rreg} +val riscv_f64Sqrt : (bits_rm, bits_D) -> (bits_fflags, bits_D) function riscv_f64Sqrt (rm, v) = { extern_f64Sqrt(rm, v); (float_fflags[4 .. 0], float_result) @@ -251,210 +251,210 @@ function riscv_f64Sqrt (rm, v) = { /* CONVERSIONS */ val extern_f16ToI32 = {c: "softfloat_f16toi32", ocaml: "Softfloat.f16_to_i32", lem: "softfloat_f16_to_i32"} : (bits_rm, bits_H) -> unit -val riscv_f16ToI32 : (bits_rm, bits_H) -> (bits_fflags, bits_W) effect {rreg} +val riscv_f16ToI32 : (bits_rm, bits_H) -> (bits_fflags, bits_W) function riscv_f16ToI32 (rm, v) = { extern_f16ToI32(rm, v); (float_fflags[4 .. 0], float_result[31 .. 0]) } val extern_f16ToUi32 = {c: "softfloat_f16toui32", ocaml: "Softfloat.f16_to_ui32", lem: "softfloat_f16_to_ui32"} : (bits_rm, bits_H) -> unit -val riscv_f16ToUi32 : (bits_rm, bits_H) -> (bits_fflags, bits_WU) effect {rreg} +val riscv_f16ToUi32 : (bits_rm, bits_H) -> (bits_fflags, bits_WU) function riscv_f16ToUi32 (rm, v) = { extern_f16ToUi32(rm, v); (float_fflags[4 .. 0], float_result[31 .. 0]) } val extern_i32ToF16 = {c: "softfloat_i32tof16", ocaml: "Softfloat.i32_to_f16", lem: "softfloat_i32_to_f16"} : (bits_rm, bits_W) -> unit -val riscv_i32ToF16 : (bits_rm, bits_W) -> (bits_fflags, bits_H) effect {rreg} +val riscv_i32ToF16 : (bits_rm, bits_W) -> (bits_fflags, bits_H) function riscv_i32ToF16 (rm, v) = { extern_i32ToF16(rm, v); (float_fflags[4 .. 0], float_result[15 .. 0]) } val extern_ui32ToF16 = {c: "softfloat_ui32tof16", ocaml: "Softfloat.ui32_to_f16", lem: "softfloat_ui32_to_f16"} : (bits_rm, bits_WU) -> unit -val riscv_ui32ToF16 : (bits_rm, bits_WU) -> (bits_fflags, bits_H) effect {rreg} +val riscv_ui32ToF16 : (bits_rm, bits_WU) -> (bits_fflags, bits_H) function riscv_ui32ToF16 (rm, v) = { extern_ui32ToF16(rm, v); (float_fflags[4 .. 0], float_result[15 .. 0]) } val extern_f16ToI64 = {c: "softfloat_f16toi64", ocaml: "Softfloat.f16_to_i64", lem: "softfloat_f16_to_i64"} : (bits_rm, bits_H) -> unit -val riscv_f16ToI64 : (bits_rm, bits_H) -> (bits_fflags, bits_L) effect {rreg} +val riscv_f16ToI64 : (bits_rm, bits_H) -> (bits_fflags, bits_L) function riscv_f16ToI64 (rm, v) = { extern_f16ToI64(rm, v); (float_fflags[4 .. 0], float_result) } val extern_f16ToUi64 = {c: "softfloat_f16toui64", ocaml: "Softfloat.f16_to_ui64", lem: "softfloat_f16_to_ui64"} : (bits_rm, bits_H) -> unit -val riscv_f16ToUi64 : (bits_rm, bits_H) -> (bits_fflags, bits_LU) effect {rreg} +val riscv_f16ToUi64 : (bits_rm, bits_H) -> (bits_fflags, bits_LU) function riscv_f16ToUi64 (rm, v) = { extern_f16ToUi64(rm, v); (float_fflags[4 .. 0], float_result) } val extern_i64ToF16 = {c: "softfloat_i64tof16", ocaml: "Softfloat.i64_to_f16", lem: "softfloat_i64_to_f16"} : (bits_rm, bits_L) -> unit -val riscv_i64ToF16 : (bits_rm, bits_L) -> (bits_fflags, bits_H) effect {rreg} +val riscv_i64ToF16 : (bits_rm, bits_L) -> (bits_fflags, bits_H) function riscv_i64ToF16 (rm, v) = { extern_i64ToF16(rm, v); (float_fflags[4 .. 0], float_result[15 .. 0]) } val extern_ui64ToF16 = {c: "softfloat_ui64tof16", ocaml: "Softfloat.ui64_to_f16", lem: "softfloat_ui64_to_f16"} : (bits_rm, bits_L) -> unit -val riscv_ui64ToF16 : (bits_rm, bits_LU) -> (bits_fflags, bits_H) effect {rreg} +val riscv_ui64ToF16 : (bits_rm, bits_LU) -> (bits_fflags, bits_H) function riscv_ui64ToF16 (rm, v) = { extern_ui64ToF16(rm, v); (float_fflags[4 .. 0], float_result[15 .. 0]) } val extern_f32ToI32 = {c: "softfloat_f32toi32", ocaml: "Softfloat.f32_to_i32", lem: "softfloat_f32_to_i32"} : (bits_rm, bits_S) -> unit -val riscv_f32ToI32 : (bits_rm, bits_S) -> (bits_fflags, bits_W) effect {rreg} +val riscv_f32ToI32 : (bits_rm, bits_S) -> (bits_fflags, bits_W) function riscv_f32ToI32 (rm, v) = { extern_f32ToI32(rm, v); (float_fflags[4 .. 0], float_result[31 .. 0]) } val extern_f32ToUi32 = {c: "softfloat_f32toui32", ocaml: "Softfloat.f32_to_ui32", lem: "softfloat_f32_to_ui32"} : (bits_rm, bits_S) -> unit -val riscv_f32ToUi32 : (bits_rm, bits_S) -> (bits_fflags, bits_WU) effect {rreg} +val riscv_f32ToUi32 : (bits_rm, bits_S) -> (bits_fflags, bits_WU) function riscv_f32ToUi32 (rm, v) = { extern_f32ToUi32(rm, v); (float_fflags[4 .. 0], float_result[31 .. 0]) } val extern_i32ToF32 = {c: "softfloat_i32tof32", ocaml: "Softfloat.i32_to_f32", lem: "softfloat_i32_to_f32"} : (bits_rm, bits_W) -> unit -val riscv_i32ToF32 : (bits_rm, bits_W) -> (bits_fflags, bits_S) effect {rreg} +val riscv_i32ToF32 : (bits_rm, bits_W) -> (bits_fflags, bits_S) function riscv_i32ToF32 (rm, v) = { extern_i32ToF32(rm, v); (float_fflags[4 .. 0], float_result[31 .. 0]) } val extern_ui32ToF32 = {c: "softfloat_ui32tof32", ocaml: "Softfloat.ui32_to_f32", lem: "softfloat_ui32_to_f32"} : (bits_rm, bits_WU) -> unit -val riscv_ui32ToF32 : (bits_rm, bits_WU) -> (bits_fflags, bits_S) effect {rreg} +val riscv_ui32ToF32 : (bits_rm, bits_WU) -> (bits_fflags, bits_S) function riscv_ui32ToF32 (rm, v) = { extern_ui32ToF32(rm, v); (float_fflags[4 .. 0], float_result[31 .. 0]) } val extern_f32ToI64 = {c: "softfloat_f32toi64", ocaml: "Softfloat.f32_to_i64", lem: "softfloat_f32_to_i64"} : (bits_rm, bits_S) -> unit -val riscv_f32ToI64 : (bits_rm, bits_S) -> (bits_fflags, bits_L) effect {rreg} +val riscv_f32ToI64 : (bits_rm, bits_S) -> (bits_fflags, bits_L) function riscv_f32ToI64 (rm, v) = { extern_f32ToI64(rm, v); (float_fflags[4 .. 0], float_result) } val extern_f32ToUi64 = {c: "softfloat_f32toui64", ocaml: "Softfloat.f32_to_ui64", lem: "softfloat_f32_to_ui64"} : (bits_rm, bits_S) -> unit -val riscv_f32ToUi64 : (bits_rm, bits_S) -> (bits_fflags, bits_LU) effect {rreg} +val riscv_f32ToUi64 : (bits_rm, bits_S) -> (bits_fflags, bits_LU) function riscv_f32ToUi64 (rm, v) = { extern_f32ToUi64(rm, v); (float_fflags[4 .. 0], float_result) } val extern_i64ToF32 = {c: "softfloat_i64tof32", ocaml: "Softfloat.i64_to_f32", lem: "softfloat_i64_to_f32"} : (bits_rm, bits_L) -> unit -val riscv_i64ToF32 : (bits_rm, bits_L) -> (bits_fflags, bits_S) effect {rreg} +val riscv_i64ToF32 : (bits_rm, bits_L) -> (bits_fflags, bits_S) function riscv_i64ToF32 (rm, v) = { extern_i64ToF32(rm, v); (float_fflags[4 .. 0], float_result[31 .. 0]) } val extern_ui64ToF32 = {c: "softfloat_ui64tof32", ocaml: "Softfloat.ui64_to_f32", lem: "softfloat_ui64_to_f32"} : (bits_rm, bits_L) -> unit -val riscv_ui64ToF32 : (bits_rm, bits_LU) -> (bits_fflags, bits_S) effect {rreg} +val riscv_ui64ToF32 : (bits_rm, bits_LU) -> (bits_fflags, bits_S) function riscv_ui64ToF32 (rm, v) = { extern_ui64ToF32(rm, v); (float_fflags[4 .. 0], float_result[31 .. 0]) } val extern_f64ToI32 = {c: "softfloat_f64toi32", ocaml: "Softfloat.f64_to_i32", lem: "softfloat_f64_to_i32"} : (bits_rm, bits_D) -> unit -val riscv_f64ToI32 : (bits_rm, bits_D) -> (bits_fflags, bits_W) effect {rreg} +val riscv_f64ToI32 : (bits_rm, bits_D) -> (bits_fflags, bits_W) function riscv_f64ToI32 (rm, v) = { extern_f64ToI32(rm, v); (float_fflags[4 .. 0], float_result[31 .. 0]) } val extern_f64ToUi32 = {c: "softfloat_f64toui32", ocaml: "Softfloat.f64_to_ui32", lem: "softfloat_f64_to_ui32"} : (bits_rm, bits_D) -> unit -val riscv_f64ToUi32 : (bits_rm, bits_D) -> (bits_fflags, bits_WU) effect {rreg} +val riscv_f64ToUi32 : (bits_rm, bits_D) -> (bits_fflags, bits_WU) function riscv_f64ToUi32 (rm, v) = { extern_f64ToUi32(rm, v); (float_fflags[4 .. 0], float_result[31 .. 0]) } val extern_i32ToF64 = {c: "softfloat_i32tof64", ocaml: "Softfloat.i32_to_f64", lem: "softfloat_i32_to_f64"} : (bits_rm, bits_W) -> unit -val riscv_i32ToF64 : (bits_rm, bits_W) -> (bits_fflags, bits_D) effect {rreg} +val riscv_i32ToF64 : (bits_rm, bits_W) -> (bits_fflags, bits_D) function riscv_i32ToF64 (rm, v) = { extern_i32ToF64(rm, v); (float_fflags[4 .. 0], float_result) } val extern_ui32ToF64 = {c: "softfloat_ui32tof64", ocaml: "Softfloat.ui32_to_f64", lem: "softfloat_ui32_to_f64"} : (bits_rm, bits_WU) -> unit -val riscv_ui32ToF64 : (bits_rm, bits_WU) -> (bits_fflags, bits_D) effect {rreg} +val riscv_ui32ToF64 : (bits_rm, bits_WU) -> (bits_fflags, bits_D) function riscv_ui32ToF64 (rm, v) = { extern_ui32ToF64(rm, v); (float_fflags[4 .. 0], float_result) } val extern_f64ToI64 = {c: "softfloat_f64toi64", ocaml: "Softfloat.f64_to_i64", lem: "softfloat_f64_to_i64"} : (bits_rm, bits_D) -> unit -val riscv_f64ToI64 : (bits_rm, bits_D) -> (bits_fflags, bits_L) effect {rreg} +val riscv_f64ToI64 : (bits_rm, bits_D) -> (bits_fflags, bits_L) function riscv_f64ToI64 (rm, v) = { extern_f64ToI64(rm, v); (float_fflags[4 .. 0], float_result) } val extern_f64ToUi64 = {c: "softfloat_f64toui64", ocaml: "Softfloat.f64_to_ui64", lem: "softfloat_f64_to_ui64"} : (bits_rm, bits_D) -> unit -val riscv_f64ToUi64 : (bits_rm, bits_D) -> (bits_fflags, bits_LU) effect {rreg} +val riscv_f64ToUi64 : (bits_rm, bits_D) -> (bits_fflags, bits_LU) function riscv_f64ToUi64 (rm, v) = { extern_f64ToUi64(rm, v); (float_fflags[4 .. 0], float_result) } val extern_i64ToF64 = {c: "softfloat_i64tof64", ocaml: "Softfloat.i64_to_f64", lem: "softfloat_i64_to_f64"} : (bits_rm, bits_L) -> unit -val riscv_i64ToF64 : (bits_rm, bits_L) -> (bits_fflags, bits_D) effect {rreg} +val riscv_i64ToF64 : (bits_rm, bits_L) -> (bits_fflags, bits_D) function riscv_i64ToF64 (rm, v) = { extern_i64ToF64(rm, v); (float_fflags[4 .. 0], float_result) } val extern_ui64ToF64 = {c: "softfloat_ui64tof64", ocaml: "Softfloat.ui64_to_f64", lem: "softfloat_ui64_to_f64"} : (bits_rm, bits_LU) -> unit -val riscv_ui64ToF64 : (bits_rm, bits_LU) -> (bits_fflags, bits_D) effect {rreg} +val riscv_ui64ToF64 : (bits_rm, bits_LU) -> (bits_fflags, bits_D) function riscv_ui64ToF64 (rm, v) = { extern_ui64ToF64(rm, v); (float_fflags[4 .. 0], float_result) } val extern_f16ToF32 = {c: "softfloat_f16tof32", ocaml: "Softfloat.f16_to_f32", lem: "softfloat_f16_to_f32"} : (bits_rm, bits_H) -> unit -val riscv_f16ToF32 : (bits_rm, bits_H) -> (bits_fflags, bits_S) effect {rreg} +val riscv_f16ToF32 : (bits_rm, bits_H) -> (bits_fflags, bits_S) function riscv_f16ToF32 (rm, v) = { extern_f16ToF32(rm, v); (float_fflags[4 .. 0], float_result[31 .. 0]) } val extern_f16ToF64 = {c: "softfloat_f16tof64", ocaml: "Softfloat.f16_to_f64", lem: "softfloat_f16_to_f64"} : (bits_rm, bits_H) -> unit -val riscv_f16ToF64 : (bits_rm, bits_H) -> (bits_fflags, bits_D) effect {rreg} +val riscv_f16ToF64 : (bits_rm, bits_H) -> (bits_fflags, bits_D) function riscv_f16ToF64 (rm, v) = { extern_f16ToF64(rm, v); (float_fflags[4 .. 0], float_result) } val extern_f32ToF64 = {c: "softfloat_f32tof64", ocaml: "Softfloat.f32_to_f64", lem: "softfloat_f32_to_f64"} : (bits_rm, bits_S) -> unit -val riscv_f32ToF64 : (bits_rm, bits_S) -> (bits_fflags, bits_D) effect {rreg} +val riscv_f32ToF64 : (bits_rm, bits_S) -> (bits_fflags, bits_D) function riscv_f32ToF64 (rm, v) = { extern_f32ToF64(rm, v); (float_fflags[4 .. 0], float_result) } val extern_f32ToF16 = {c: "softfloat_f32tof16", ocaml: "Softfloat.f32_to_f16", lem: "softfloat_f32_to_f16"} : (bits_rm, bits_S) -> unit -val riscv_f32ToF16 : (bits_rm, bits_S) -> (bits_fflags, bits_H) effect {rreg} +val riscv_f32ToF16 : (bits_rm, bits_S) -> (bits_fflags, bits_H) function riscv_f32ToF16 (rm, v) = { extern_f32ToF16(rm, v); (float_fflags[4 .. 0], float_result[15 .. 0]) } val extern_f64ToF16 = {c: "softfloat_f64tof16", ocaml: "Softfloat.f64_to_f16", lem: "softfloat_f64_to_f16"} : (bits_rm, bits_D) -> unit -val riscv_f64ToF16 : (bits_rm, bits_D) -> (bits_fflags, bits_H) effect {rreg} +val riscv_f64ToF16 : (bits_rm, bits_D) -> (bits_fflags, bits_H) function riscv_f64ToF16 (rm, v) = { extern_f64ToF16(rm, v); (float_fflags[4 .. 0], float_result[15 .. 0]) } val extern_f64ToF32 = {c: "softfloat_f64tof32", ocaml: "Softfloat.f64_to_f32", lem: "softfloat_f64_to_f32"} : (bits_rm, bits_D) -> unit -val riscv_f64ToF32 : (bits_rm, bits_D) -> (bits_fflags, bits_S) effect {rreg} +val riscv_f64ToF32 : (bits_rm, bits_D) -> (bits_fflags, bits_S) function riscv_f64ToF32 (rm, v) = { extern_f64ToF32(rm, v); (float_fflags[4 .. 0], float_result[31 .. 0]) @@ -464,126 +464,126 @@ function riscv_f64ToF32 (rm, v) = { /* COMPARISONS */ val extern_f16Lt = {c: "softfloat_f16lt", ocaml: "Softfloat.f16_lt", lem: "softfloat_f16_lt"} : (bits_H, bits_H) -> unit -val riscv_f16Lt : (bits_H, bits_H) -> (bits_fflags, bool) effect {rreg} +val riscv_f16Lt : (bits_H, bits_H) -> (bits_fflags, bool) function riscv_f16Lt (v1, v2) = { extern_f16Lt(v1, v2); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } val extern_f16Lt_quiet = {c: "softfloat_f16lt_quiet", ocaml: "Softfloat.f16_lt_quiet", lem: "softfloat_f16_lt_quiet"} : (bits_H, bits_H) -> unit -val riscv_f16Lt_quiet : (bits_H, bits_H) -> (bits_fflags, bool) effect {rreg} +val riscv_f16Lt_quiet : (bits_H, bits_H) -> (bits_fflags, bool) function riscv_f16Lt_quiet (v1, v2) = { extern_f16Lt_quiet(v1, v2); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } val extern_f16Le = {c: "softfloat_f16le", ocaml: "Softfloat.f16_le", lem: "softfloat_f16_le"} : (bits_H, bits_H) -> unit -val riscv_f16Le : (bits_H, bits_H) -> (bits_fflags, bool) effect {rreg} +val riscv_f16Le : (bits_H, bits_H) -> (bits_fflags, bool) function riscv_f16Le (v1, v2) = { extern_f16Le(v1, v2); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } val extern_f16Le_quiet = {c: "softfloat_f16le_quiet", ocaml: "Softfloat.f16_le_quiet", lem: "softfloat_f16_le_quiet"} : (bits_H, bits_H) -> unit -val riscv_f16Le_quiet : (bits_H, bits_H) -> (bits_fflags, bool) effect {rreg} +val riscv_f16Le_quiet : (bits_H, bits_H) -> (bits_fflags, bool) function riscv_f16Le_quiet (v1, v2) = { extern_f16Le_quiet(v1, v2); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } val extern_f16Eq = {c: "softfloat_f16eq", ocaml: "Softfloat.f16_eq", lem: "softfloat_f16_eq"} : (bits_H, bits_H) -> unit -val riscv_f16Eq : (bits_H, bits_H) -> (bits_fflags, bool) effect {rreg} +val riscv_f16Eq : (bits_H, bits_H) -> (bits_fflags, bool) function riscv_f16Eq (v1, v2) = { extern_f16Eq(v1, v2); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } val extern_f32Lt = {c: "softfloat_f32lt", ocaml: "Softfloat.f32_lt", lem: "softfloat_f32_lt"} : (bits_S, bits_S) -> unit -val riscv_f32Lt : (bits_S, bits_S) -> (bits_fflags, bool) effect {rreg} +val riscv_f32Lt : (bits_S, bits_S) -> (bits_fflags, bool) function riscv_f32Lt (v1, v2) = { extern_f32Lt(v1, v2); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } val extern_f32Lt_quiet = {c: "softfloat_f32lt_quiet", ocaml: "Softfloat.f32_lt_quiet", lem: "softfloat_f32_lt_quiet"} : (bits_S, bits_S) -> unit -val riscv_f32Lt_quiet : (bits_S, bits_S) -> (bits_fflags, bool) effect {rreg} +val riscv_f32Lt_quiet : (bits_S, bits_S) -> (bits_fflags, bool) function riscv_f32Lt_quiet (v1, v2) = { extern_f32Lt_quiet(v1, v2); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } val extern_f32Le = {c: "softfloat_f32le", ocaml: "Softfloat.f32_le", lem: "softfloat_f32_le"} : (bits_S, bits_S) -> unit -val riscv_f32Le : (bits_S, bits_S) -> (bits_fflags, bool) effect {rreg} +val riscv_f32Le : (bits_S, bits_S) -> (bits_fflags, bool) function riscv_f32Le (v1, v2) = { extern_f32Le(v1, v2); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } val extern_f32Le_quiet = {c: "softfloat_f32le_quiet", ocaml: "Softfloat.f32_le_quiet", lem: "softfloat_f32_le_quiet"} : (bits_S, bits_S) -> unit -val riscv_f32Le_quiet : (bits_S, bits_S) -> (bits_fflags, bool) effect {rreg} +val riscv_f32Le_quiet : (bits_S, bits_S) -> (bits_fflags, bool) function riscv_f32Le_quiet (v1, v2) = { extern_f32Le_quiet(v1, v2); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } val extern_f32Eq = {c: "softfloat_f32eq", ocaml: "Softfloat.f32_eq", lem: "softfloat_f32_eq"} : (bits_S, bits_S) -> unit -val riscv_f32Eq : (bits_S, bits_S) -> (bits_fflags, bool) effect {rreg} +val riscv_f32Eq : (bits_S, bits_S) -> (bits_fflags, bool) function riscv_f32Eq (v1, v2) = { extern_f32Eq(v1, v2); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } val extern_f64Lt = {c: "softfloat_f64lt", ocaml: "Softfloat.f64_lt", lem: "softfloat_f64_lt"} : (bits_D, bits_D) -> unit -val riscv_f64Lt : (bits_D, bits_D) -> (bits_fflags, bool) effect {rreg} +val riscv_f64Lt : (bits_D, bits_D) -> (bits_fflags, bool) function riscv_f64Lt (v1, v2) = { extern_f64Lt(v1, v2); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } val extern_f64Lt_quiet = {c: "softfloat_f64lt_quiet", ocaml: "Softfloat.f64_lt_quiet", lem: "softfloat_f64_lt_quiet"} : (bits_D, bits_D) -> unit -val riscv_f64Lt_quiet : (bits_D, bits_D) -> (bits_fflags, bool) effect {rreg} +val riscv_f64Lt_quiet : (bits_D, bits_D) -> (bits_fflags, bool) function riscv_f64Lt_quiet (v1, v2) = { extern_f64Lt_quiet(v1, v2); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } val extern_f64Le = {c: "softfloat_f64le", ocaml: "Softfloat.f64_le", lem: "softfloat_f64_le"} : (bits_D, bits_D) -> unit -val riscv_f64Le : (bits_D, bits_D) -> (bits_fflags, bool) effect {rreg} +val riscv_f64Le : (bits_D, bits_D) -> (bits_fflags, bool) function riscv_f64Le (v1, v2) = { extern_f64Le(v1, v2); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } val extern_f64Le_quiet = {c: "softfloat_f64le_quiet", ocaml: "Softfloat.f64_le_quiet", lem: "softfloat_f64_le_quiet"} : (bits_D, bits_D) -> unit -val riscv_f64Le_quiet : (bits_D, bits_D) -> (bits_fflags, bool) effect {rreg} +val riscv_f64Le_quiet : (bits_D, bits_D) -> (bits_fflags, bool) function riscv_f64Le_quiet (v1, v2) = { extern_f64Le_quiet(v1, v2); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } val extern_f64Eq = {c: "softfloat_f64eq", ocaml: "Softfloat.f64_eq", lem: "softfloat_f64_eq"} : (bits_D, bits_D) -> unit -val riscv_f64Eq : (bits_D, bits_D) -> (bits_fflags, bool) effect {rreg} +val riscv_f64Eq : (bits_D, bits_D) -> (bits_fflags, bool) function riscv_f64Eq (v1, v2) = { extern_f64Eq(v1, v2); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } val extern_f16roundToInt = {c: "softfloat_f16roundToInt", ocaml: "Softfloat.f16_round_to_int", lem: "softfloat_f16_round_to_int"} : (bits_rm, bits_H, bool) -> unit -val riscv_f16roundToInt : (bits_rm, bits_H, bool) -> (bits_fflags, bits_H) effect {rreg} +val riscv_f16roundToInt : (bits_rm, bits_H, bool) -> (bits_fflags, bits_H) function riscv_f16roundToInt (rm, v, exact) = { extern_f16roundToInt(rm, v, exact); (float_fflags[4 .. 0], float_result[15 .. 0]) } val extern_f32roundToInt = {c: "softfloat_f32roundToInt", ocaml: "Softfloat.f32_round_to_int", lem: "softfloat_f32_round_to_int"} : (bits_rm, bits_S, bool) -> unit -val riscv_f32roundToInt : (bits_rm, bits_S, bool) -> (bits_fflags, bits_S) effect {rreg} +val riscv_f32roundToInt : (bits_rm, bits_S, bool) -> (bits_fflags, bits_S) function riscv_f32roundToInt (rm, v, exact) = { extern_f32roundToInt(rm, v, exact); (float_fflags[4 .. 0], float_result[31 .. 0]) } val extern_f64roundToInt = {c: "softfloat_f64roundToInt", ocaml: "Softfloat.f64_round_to_int", lem: "softfloat_f64_round_to_int"} : (bits_rm, bits_D, bool) -> unit -val riscv_f64roundToInt : (bits_rm, bits_D, bool) -> (bits_fflags, bits_D) effect {rreg} +val riscv_f64roundToInt : (bits_rm, bits_D, bool) -> (bits_fflags, bits_D) function riscv_f64roundToInt (rm, v, exact) = { extern_f64roundToInt(rm, v, exact); (float_fflags[4 .. 0], float_result) diff --git a/model/riscv_step_rvfi.sail b/model/riscv_step_rvfi.sail index c266e6b87..d23a679d7 100644 --- a/model/riscv_step_rvfi.sail +++ b/model/riscv_step_rvfi.sail @@ -79,7 +79,7 @@ function ext_post_step_hook() -> unit = { rvfi_pc_data->rvfi_pc_wdata() = zero_extend(get_arch_pc()) } -val ext_init : unit -> unit effect {wreg} +val ext_init : unit -> unit function ext_init() = { init_base_regs(); init_fdext_regs(); diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index b8540538c..cf0a488cc 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -228,7 +228,7 @@ function check_CSR(csr : csreg, p : Privilege, isWrite : bool) -> bool = * where cancellation can be performed. */ -val speculate_conditional = {ocaml: "Platform.speculate_conditional", interpreter: "excl_res", c: "speculate_conditional", lem: "speculate_conditional_success"} : unit -> bool effect {exmem} +val speculate_conditional = {ocaml: "Platform.speculate_conditional", interpreter: "excl_res", c: "speculate_conditional", lem: "speculate_conditional_success"} : unit -> bool val load_reservation = {ocaml: "Platform.load_reservation", interpreter: "Platform.load_reservation", c: "load_reservation", lem: "load_reservation"} : xlenbits -> unit val match_reservation = {ocaml: "Platform.match_reservation", interpreter: "Platform.match_reservation", lem: "match_reservation", c: "match_reservation"} : xlenbits -> bool @@ -377,7 +377,7 @@ function tval(excinfo : option(xlenbits)) -> xlenbits = { } $ifdef RVFI_DII -val rvfi_trap : unit -> unit effect {wreg} +val rvfi_trap : unit -> unit // TODO: record rvfi_trap_data function rvfi_trap () = rvfi_inst_data->rvfi_trap() = 0x01 diff --git a/model/riscv_sys_exceptions.sail b/model/riscv_sys_exceptions.sail index a4fc8f06b..14cc05cfd 100644 --- a/model/riscv_sys_exceptions.sail +++ b/model/riscv_sys_exceptions.sail @@ -99,7 +99,7 @@ function prepare_trap_vector(p : Privilege, cause : Mcause) -> xlenbits = { * prepare_xret_target: used to get the value for control transfer to the xret target */ -val get_xret_target : Privilege -> xlenbits effect {rreg} +val get_xret_target : Privilege -> xlenbits function get_xret_target(p) = match p { Machine => mepc, @@ -107,7 +107,7 @@ function get_xret_target(p) = User => uepc } -val set_xret_target : (Privilege, xlenbits) -> xlenbits effect {rreg, wreg} +val set_xret_target : (Privilege, xlenbits) -> xlenbits function set_xret_target(p, value) = { let target = legalize_xepc(value); match p { @@ -118,7 +118,7 @@ function set_xret_target(p, value) = { target } -val prepare_xret_target : (Privilege) -> xlenbits effect {rreg, wreg} +val prepare_xret_target : (Privilege) -> xlenbits function prepare_xret_target(p) = get_xret_target(p) diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 251df5a65..47744698d 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -154,7 +154,7 @@ val sys_enable_next = {c: "sys_enable_next", ocaml: "Platform.enable_next", _: " /* This function allows an extension to veto a write to Misa if it would violate an alignment restriction on unsetting C. If it returns true the write will have no effect. */ -val ext_veto_disable_C : unit -> bool effect {rreg} +val ext_veto_disable_C : unit -> bool function legalize_misa(m : Misa, v : xlenbits) -> Misa = { let v = Mk_Misa(v); diff --git a/model/riscv_types.sail b/model/riscv_types.sail index 728c1d26c..b9402864b 100644 --- a/model/riscv_types.sail +++ b/model/riscv_types.sail @@ -138,10 +138,10 @@ union exception = { Error_internal_error : unit } -val not_implemented : forall ('a : Type). string -> 'a effect {escape} +val not_implemented : forall ('a : Type). string -> 'a function not_implemented message = throw(Error_not_implemented(message)) -val internal_error : forall ('a : Type). (string, int, string) -> 'a effect {escape} +val internal_error : forall ('a : Type). (string, int, string) -> 'a function internal_error(file, line, s) = { assert (false, file ^ ":" ^ string_of_int(line) ^ ": " ^ s); throw Error_internal_error() @@ -464,7 +464,7 @@ function word_width_bytes width = match width { * should be unreachable. See https://github.com/riscv/sail-riscv/issues/194 * and https://github.com/riscv/sail-riscv/pull/197 . */ -val report_invalid_width : forall ('a : Type). (string, int, word_width, string) -> 'a effect {escape} +val report_invalid_width : forall ('a : Type). (string, int, word_width, string) -> 'a function report_invalid_width(f , l, w, k) -> 'a = { /* * Ideally we would call internal_error here but this triggers a Sail bug, diff --git a/model/riscv_types_kext.sail b/model/riscv_types_kext.sail index ef03d9b79..9f9892f8b 100644 --- a/model/riscv_types_kext.sail +++ b/model/riscv_types_kext.sail @@ -144,7 +144,7 @@ function aes_mixcolumn_inv(x) = { do not decode to the AES64KS1I instruction. The 0xA case is used specifically for the AES-256 KeySchedule, and this function is never called in that case. */ -val aes_decode_rcon : bits(4) -> bits(32) effect {escape} +val aes_decode_rcon : bits(4) -> bits(32) function aes_decode_rcon(r) = { assert(r <_u 0xA); match r { diff --git a/model/riscv_vmem_rv32.sail b/model/riscv_vmem_rv32.sail index ba2933250..3478be4da 100644 --- a/model/riscv_vmem_rv32.sail +++ b/model/riscv_vmem_rv32.sail @@ -79,7 +79,7 @@ function legalize_satp(a : Architecture, o : xlenbits, v : xlenbits) -> xlenbits /* Compute the address translation mode. */ -val translationMode : (Privilege) -> SATPMode effect {rreg, escape} +val translationMode : (Privilege) -> SATPMode function translationMode(priv) = { if priv == Machine then Sbare else { @@ -96,7 +96,7 @@ function translationMode(priv) = { /* Top-level address translation dispatcher */ -val translateAddr_priv : (xlenbits, AccessType(ext_access_type), Privilege) -> TR_Result(xlenbits, ExceptionType) effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg} +val translateAddr_priv : (xlenbits, AccessType(ext_access_type), Privilege) -> TR_Result(xlenbits, ExceptionType) function translateAddr_priv(vAddr, ac, effPriv) = { let mxr : bool = mstatus.MXR() == 0b1; let do_sum : bool = mstatus.SUM() == 0b1; @@ -118,11 +118,11 @@ function translateAddr_priv(vAddr, ac, effPriv) = { } } -val translateAddr : (xlenbits, AccessType(ext_access_type)) -> TR_Result(xlenbits, ExceptionType) effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg} +val translateAddr : (xlenbits, AccessType(ext_access_type)) -> TR_Result(xlenbits, ExceptionType) function translateAddr(vAddr, ac) = translateAddr_priv(vAddr, ac, effectivePrivilege(ac, mstatus, cur_privilege)) -val flush_TLB : (option(xlenbits), option(xlenbits)) -> unit effect {rreg, wreg} +val flush_TLB : (option(xlenbits), option(xlenbits)) -> unit function flush_TLB(asid_xlen, addr_xlen) -> unit = { let asid : option(asid32) = match (asid_xlen) { diff --git a/model/riscv_vmem_rv64.sail b/model/riscv_vmem_rv64.sail index 10b2067d6..18d099192 100644 --- a/model/riscv_vmem_rv64.sail +++ b/model/riscv_vmem_rv64.sail @@ -93,7 +93,7 @@ function isValidSv48Addr(vAddr : xlenbits) -> bool = { /* Compute the address translation mode. */ -val translationMode : (Privilege) -> SATPMode effect {rreg, escape} +val translationMode : (Privilege) -> SATPMode function translationMode(priv) = { if priv == Machine then Sbare else { @@ -117,7 +117,7 @@ function translationMode(priv) = { /* Top-level address translation dispatcher */ -val translateAddr_priv : (xlenbits, AccessType(ext_access_type), Privilege) -> TR_Result(xlenbits, ExceptionType) effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg} +val translateAddr_priv : (xlenbits, AccessType(ext_access_type), Privilege) -> TR_Result(xlenbits, ExceptionType) function translateAddr_priv(vAddr, ac, effPriv) = { let mxr : bool = mstatus.MXR() == 0b1; let do_sum : bool = mstatus.SUM() == 0b1; @@ -149,11 +149,11 @@ function translateAddr_priv(vAddr, ac, effPriv) = { } } -val translateAddr : (xlenbits, AccessType(ext_access_type)) -> TR_Result(xlenbits, ExceptionType) effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg} +val translateAddr : (xlenbits, AccessType(ext_access_type)) -> TR_Result(xlenbits, ExceptionType) function translateAddr(vAddr, ac) = translateAddr_priv(vAddr, ac, effectivePrivilege(ac, mstatus, cur_privilege)) -val flush_TLB : (option(xlenbits), option(xlenbits)) -> unit effect {rreg, wreg} +val flush_TLB : (option(xlenbits), option(xlenbits)) -> unit function flush_TLB(asid_xlen, addr_xlen) -> unit = { /* Flush both Sv39 and Sv48 TLBs. */ let (addr39, addr48) : (option(vaddr39), option(vaddr48)) = diff --git a/model/riscv_vmem_sv32.sail b/model/riscv_vmem_sv32.sail index e8365c323..72def151a 100644 --- a/model/riscv_vmem_sv32.sail +++ b/model/riscv_vmem_sv32.sail @@ -76,7 +76,7 @@ function to_phys_addr(a : paddr32) -> xlenbits = a[31..0] -val walk32 : (vaddr32, AccessType(ext_access_type), Privilege, bool, bool, paddr32, nat, bool, ext_ptw) -> PTW_Result(paddr32, SV32_PTE) effect {rmem, rmemt, rreg, escape} +val walk32 : (vaddr32, AccessType(ext_access_type), Privilege, bool, bool, paddr32, nat, bool, ext_ptw) -> PTW_Result(paddr32, SV32_PTE) function walk32(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { let va = Mk_SV32_Vaddr(vaddr); let pt_ofs : paddr32 = shiftl(zero_extend(shiftr(va.VPNi(), (level * SV32_LEVEL_BITS))[(SV32_LEVEL_BITS - 1) .. 0]), @@ -158,14 +158,14 @@ function walk32(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { type TLB32_Entry = TLB_Entry(9, 32, 34, 32) register tlb32 : option(TLB32_Entry) -val lookup_TLB32 : (asid32, vaddr32) -> option((nat, TLB32_Entry)) effect {rreg} +val lookup_TLB32 : (asid32, vaddr32) -> option((nat, TLB32_Entry)) function lookup_TLB32(asid, vaddr) = match tlb32 { None() => None(), Some(e) => if match_TLB_Entry(e, asid, vaddr) then Some((0, e)) else None() } -val add_to_TLB32 : (asid32, vaddr32, paddr32, SV32_PTE, paddr32, nat, bool) -> unit effect {wreg, rreg} +val add_to_TLB32 : (asid32, vaddr32, paddr32, SV32_PTE, paddr32, nat, bool) -> unit function add_to_TLB32(asid, vAddr, pAddr, pte, pteAddr, level, global) = { let ent : TLB32_Entry = make_TLB_Entry(asid, global, vAddr, pAddr, pte.bits(), level, pteAddr, SV32_LEVEL_BITS); tlb32 = Some(ent) @@ -174,7 +174,7 @@ function add_to_TLB32(asid, vAddr, pAddr, pte, pteAddr, level, global) = { function write_TLB32(idx : nat, ent : TLB32_Entry) -> unit = tlb32 = Some(ent) -val flush_TLB32 : (option(asid32), option(vaddr32)) -> unit effect {rreg, wreg} +val flush_TLB32 : (option(asid32), option(vaddr32)) -> unit function flush_TLB32(asid, addr) = match (tlb32) { None() => (), @@ -185,7 +185,7 @@ function flush_TLB32(asid, addr) = /* address translation */ -val translate32 : (asid32, paddr32, vaddr32, AccessType(ext_access_type), Privilege, bool, bool, nat, ext_ptw) -> TR_Result(paddr32, PTW_Error) effect {rreg, wreg, wmv, wmvt, escape, rmem, rmemt} +val translate32 : (asid32, paddr32, vaddr32, AccessType(ext_access_type), Privilege, bool, bool, nat, ext_ptw) -> TR_Result(paddr32, PTW_Error) function translate32(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = { match lookup_TLB32(asid, vAddr) { Some(idx, ent) => { diff --git a/model/riscv_vmem_sv39.sail b/model/riscv_vmem_sv39.sail index 384b6ece3..25378a8dc 100644 --- a/model/riscv_vmem_sv39.sail +++ b/model/riscv_vmem_sv39.sail @@ -70,7 +70,7 @@ /* Sv39 address translation for RV64. */ -val walk39 : (vaddr39, AccessType(ext_access_type), Privilege, bool, bool, paddr64, nat, bool, ext_ptw) -> PTW_Result(paddr64, SV39_PTE) effect {rmem, rmemt, rreg, escape} +val walk39 : (vaddr39, AccessType(ext_access_type), Privilege, bool, bool, paddr64, nat, bool, ext_ptw) -> PTW_Result(paddr64, SV39_PTE) function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { let va = Mk_SV39_Vaddr(vaddr); let pt_ofs : paddr64 = shiftl(zero_extend(shiftr(va.VPNi(), (level * SV39_LEVEL_BITS))[(SV39_LEVEL_BITS - 1) .. 0]), @@ -152,14 +152,14 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { type TLB39_Entry = TLB_Entry(16, 39, 56, 64) register tlb39 : option(TLB39_Entry) -val lookup_TLB39 : (asid64, vaddr39) -> option((nat, TLB39_Entry)) effect {rreg} +val lookup_TLB39 : (asid64, vaddr39) -> option((nat, TLB39_Entry)) function lookup_TLB39(asid, vaddr) = match tlb39 { None() => None(), Some(e) => if match_TLB_Entry(e, asid, vaddr) then Some((0, e)) else None() } -val add_to_TLB39 : (asid64, vaddr39, paddr64, SV39_PTE, paddr64, nat, bool) -> unit effect {wreg, rreg} +val add_to_TLB39 : (asid64, vaddr39, paddr64, SV39_PTE, paddr64, nat, bool) -> unit function add_to_TLB39(asid, vAddr, pAddr, pte, pteAddr, level, global) = { let ent : TLB39_Entry = make_TLB_Entry(asid, global, vAddr, pAddr, pte.bits(), level, pteAddr, SV39_LEVEL_BITS); tlb39 = Some(ent) @@ -168,7 +168,7 @@ function add_to_TLB39(asid, vAddr, pAddr, pte, pteAddr, level, global) = { function write_TLB39(idx : nat, ent : TLB39_Entry) -> unit = tlb39 = Some(ent) -val flush_TLB39 : (option(asid64), option(vaddr39)) -> unit effect {rreg, wreg} +val flush_TLB39 : (option(asid64), option(vaddr39)) -> unit function flush_TLB39(asid, addr) = match (tlb39) { None() => (), @@ -179,7 +179,7 @@ function flush_TLB39(asid, addr) = /* address translation */ -val translate39 : (asid64, paddr64, vaddr39, AccessType(ext_access_type), Privilege, bool, bool, nat, ext_ptw) -> TR_Result(paddr64, PTW_Error) effect {rreg, wreg, wmv, wmvt, escape, rmem, rmemt} +val translate39 : (asid64, paddr64, vaddr39, AccessType(ext_access_type), Privilege, bool, bool, nat, ext_ptw) -> TR_Result(paddr64, PTW_Error) function translate39(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = { match lookup_TLB39(asid, vAddr) { Some(idx, ent) => { diff --git a/model/riscv_vmem_sv48.sail b/model/riscv_vmem_sv48.sail index 729a70177..64c7a542a 100644 --- a/model/riscv_vmem_sv48.sail +++ b/model/riscv_vmem_sv48.sail @@ -70,7 +70,7 @@ /* Sv48 address translation for RV64. */ -val walk48 : (vaddr48, AccessType(ext_access_type), Privilege, bool, bool, paddr64, nat, bool, ext_ptw) -> PTW_Result(paddr64, SV48_PTE) effect {rmem, rmemt, rreg, escape} +val walk48 : (vaddr48, AccessType(ext_access_type), Privilege, bool, bool, paddr64, nat, bool, ext_ptw) -> PTW_Result(paddr64, SV48_PTE) function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { let va = Mk_SV48_Vaddr(vaddr); let pt_ofs : paddr64 = shiftl(zero_extend(shiftr(va.VPNi(), (level * SV48_LEVEL_BITS))[(SV48_LEVEL_BITS - 1) .. 0]), @@ -152,14 +152,14 @@ function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { type TLB48_Entry = TLB_Entry(16, 48, 56, 64) register tlb48 : option(TLB48_Entry) -val lookup_TLB48 : (asid64, vaddr48) -> option((nat, TLB48_Entry)) effect {rreg} +val lookup_TLB48 : (asid64, vaddr48) -> option((nat, TLB48_Entry)) function lookup_TLB48(asid, vaddr) = match tlb48 { None() => None(), Some(e) => if match_TLB_Entry(e, asid, vaddr) then Some((0, e)) else None() } -val add_to_TLB48 : (asid64, vaddr48, paddr64, SV48_PTE, paddr64, nat, bool) -> unit effect {wreg, rreg} +val add_to_TLB48 : (asid64, vaddr48, paddr64, SV48_PTE, paddr64, nat, bool) -> unit function add_to_TLB48(asid, vAddr, pAddr, pte, pteAddr, level, global) = { let ent : TLB48_Entry = make_TLB_Entry(asid, global, vAddr, pAddr, pte.bits(), level, pteAddr, SV48_LEVEL_BITS); tlb48 = Some(ent) @@ -168,7 +168,7 @@ function add_to_TLB48(asid, vAddr, pAddr, pte, pteAddr, level, global) = { function write_TLB48(idx : nat, ent : TLB48_Entry) -> unit = tlb48 = Some(ent) -val flush_TLB48 : (option(asid64), option(vaddr48)) -> unit effect {rreg, wreg} +val flush_TLB48 : (option(asid64), option(vaddr48)) -> unit function flush_TLB48(asid, addr) = match (tlb48) { None() => (), @@ -179,7 +179,7 @@ function flush_TLB48(asid, addr) = /* address translation */ -val translate48 : (asid64, paddr64, vaddr48, AccessType(ext_access_type), Privilege, bool, bool, nat, ext_ptw) -> TR_Result(paddr64, PTW_Error) effect {rreg, wreg, wmv, wmvt, escape, rmem, rmemt} +val translate48 : (asid64, paddr64, vaddr48, AccessType(ext_access_type), Privilege, bool, bool, nat, ext_ptw) -> TR_Result(paddr64, PTW_Error) function translate48(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = { match walk48(vAddr, ac, priv, mxr, do_sum, ptb, level, false, ext_ptw) { PTW_Failure(f, ext_ptw) => TR_Failure(f, ext_ptw), diff --git a/model/riscv_vmem_tlb.sail b/model/riscv_vmem_tlb.sail index ae24815f0..27b63ba37 100644 --- a/model/riscv_vmem_tlb.sail +++ b/model/riscv_vmem_tlb.sail @@ -85,7 +85,7 @@ struct TLB_Entry('asidlen: Int, 'valen: Int, 'palen: Int, 'ptelen: Int) = { val make_TLB_Entry : forall 'asidlen 'valen 'palen 'ptelen, 'valen > 0. (bits('asidlen), bool, bits('valen), bits('palen), bits('ptelen), nat, bits('palen), nat) - -> TLB_Entry('asidlen, 'valen, 'palen, 'ptelen) effect {rreg} + -> TLB_Entry('asidlen, 'valen, 'palen, 'ptelen) function make_TLB_Entry(asid, global, vAddr, pAddr, pte, level, pteAddr, levelBitSize) = { let shift : nat = PAGESIZE_BITS + (level * levelBitSize); /* fixme hack: use a better idiom for masks */ diff --git a/model/rvfi_dii.sail b/model/rvfi_dii.sail index 5c87465b6..e1007bb03 100644 --- a/model/rvfi_dii.sail +++ b/model/rvfi_dii.sail @@ -86,16 +86,16 @@ bitfield RVFI_DII_Instruction_Packet : bits(64) = { register rvfi_instruction : RVFI_DII_Instruction_Packet -val rvfi_set_instr_packet : bits(64) -> unit effect {wreg} +val rvfi_set_instr_packet : bits(64) -> unit function rvfi_set_instr_packet(p) = rvfi_instruction = Mk_RVFI_DII_Instruction_Packet(p) -val rvfi_get_cmd : unit -> bits(8) effect {rreg} +val rvfi_get_cmd : unit -> bits(8) function rvfi_get_cmd () = rvfi_instruction.rvfi_cmd() -val rvfi_get_insn : unit -> bits(32) effect {rreg} +val rvfi_get_insn : unit -> bits(32) function rvfi_get_insn () = rvfi_instruction.rvfi_insn() @@ -261,7 +261,7 @@ register rvfi_mem_data : RVFI_DII_Execution_Packet_Ext_MemAccess register rvfi_mem_data_present : bool // Reset the trace -val rvfi_zero_exec_packet : unit -> unit effect {wreg} +val rvfi_zero_exec_packet : unit -> unit function rvfi_zero_exec_packet () = { rvfi_inst_data = Mk_RVFI_DII_Execution_Packet_InstMetaData(zero_extend(0b0)); @@ -278,7 +278,7 @@ function rvfi_zero_exec_packet () = { // FIXME: most of these will no longer be necessary once we use the c2 sail backend. -val rvfi_halt_exec_packet : unit -> unit effect {wreg} +val rvfi_halt_exec_packet : unit -> unit function rvfi_halt_exec_packet () = rvfi_inst_data->rvfi_halt() = 0x01 @@ -294,7 +294,7 @@ function rvfi_get_v2_support_packet () = { return rvfi_exec.bits(); } -val rvfi_get_exec_packet_v1 : unit -> bits(704) effect {rreg} +val rvfi_get_exec_packet_v1 : unit -> bits(704) function rvfi_get_exec_packet_v1 () = { let v1_packet = Mk_RVFI_DII_Execution_Packet_V1(zero_extend(0b0)); // Convert the v2 packet to a v1 packet @@ -323,7 +323,7 @@ function rvfi_get_exec_packet_v1 () = { return v1_packet.bits(); } -val rvfi_get_v2_trace_size : unit -> bits(64) effect {rreg} +val rvfi_get_v2_trace_size : unit -> bits(64) function rvfi_get_v2_trace_size () = { let trace_size : bits(64) = to_bits(64, 512); let trace_size = if (rvfi_int_data_present) then trace_size + 320 else trace_size; @@ -331,7 +331,7 @@ function rvfi_get_v2_trace_size () = { return trace_size >> 3; // we have to return bytes not bits } -val rvfi_get_exec_packet_v2 : unit -> bits(512) effect {rreg} +val rvfi_get_exec_packet_v2 : unit -> bits(512) function rvfi_get_exec_packet_v2 () = { // TODO: add the other data // TODO: find a way to return a variable-length bitvector @@ -348,13 +348,13 @@ function rvfi_get_exec_packet_v2 () = { return packet.bits(); } -val rvfi_get_int_data : unit -> bits(320) effect {rreg} +val rvfi_get_int_data : unit -> bits(320) function rvfi_get_int_data () = { assert(rvfi_int_data_present, "reading uninitialized data"); return rvfi_int_data.bits(); } -val rvfi_get_mem_data : unit -> bits(704) effect {rreg} +val rvfi_get_mem_data : unit -> bits(704) function rvfi_get_mem_data () = { assert(rvfi_mem_data_present, "reading uninitialized data"); return rvfi_mem_data.bits(); @@ -365,7 +365,7 @@ val rvfi_encode_width_mask : forall 'n, 0 < 'n <= 32. atom('n) -> bits(32) function rvfi_encode_width_mask(width) = (0xFFFFFFFF >> (32 - width)) -val print_rvfi_exec : unit -> unit effect {rreg} +val print_rvfi_exec : unit -> unit function print_rvfi_exec () = { print_bits("rvfi_intr : ", rvfi_inst_data.rvfi_intr());