diff options
Diffstat (limited to 'model')
38 files changed, 4094 insertions, 137 deletions
diff --git a/model/prelude_mem.sail b/model/prelude_mem.sail index b8d47d0..85d141b 100644 --- a/model/prelude_mem.sail +++ b/model/prelude_mem.sail @@ -17,15 +17,16 @@ would be even better if it could be <= 8 bytes so that data can also be a 64-bit int but CHERI needs 128-bit accesses for capabilities and SIMD / vector instructions will also need more. */ - type max_mem_access : Int = 16 +type max_mem_access : Int = 16 -val 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 effect {wmv, wmvt} 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; * there is currently no return value. - * FIXME: We should convert the external API to consume - * the value along with the metadata to ensure atomicity. + * FIXME: We should convert the external API for all backends + * (not just for Lem) to consume the value along with the + * metadata to ensure atomicity. */ let ret : bool = __write_mem(wk, sizeof(xlen), addr, width, data); if ret then __WriteRAM_Meta(addr, width, meta); @@ -36,10 +37,10 @@ val write_ram_ea : forall 'n, 0 < 'n <= max_mem_access . (write_kind, xlenbits, function write_ram_ea(wk, addr, width) = __write_mem_ea(wk, sizeof(xlen), addr, width) -/* FIXME: Make this also return the metadata, which will also require external API changes. */ -val read_ram : forall 'n, 0 < 'n <= max_mem_access . (read_kind, xlenbits, atom('n)) -> bits(8 * 'n) effect {rmem} -function read_ram(rk, addr, width) = - __read_mem(rk, 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} +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 diff --git a/model/riscv_csr_ext.sail b/model/riscv_csr_ext.sail index 8c0cc17..9220534 100644 --- a/model/riscv_csr_ext.sail +++ b/model/riscv_csr_ext.sail @@ -1,8 +1,12 @@ -/* numeric fallback XXX apparent sail bug prevents this from compiling for C */ -//mapping clause csr_name_map = reg <-> "UNKNOWN CSR: " ^ hex_bits_12(reg) +mapping clause csr_name_map = reg <-> hex_bits_12(reg) end csr_name_map +/* XXX due to an apparent Sail bug the definition of this function must appear + after the last csr_name_map clause and not by the val spec as it was + previously. */ +function csr_name(csr) = csr_name_map(csr) + function clause ext_is_CSR_defined(_, _) = false end ext_is_CSR_defined diff --git a/model/riscv_csr_map.sail b/model/riscv_csr_map.sail index 7ec161b..ba52da6 100644 --- a/model/riscv_csr_map.sail +++ b/model/riscv_csr_map.sail @@ -93,7 +93,6 @@ mapping clause csr_name_map = 0x7a2 <-> "tdata2" mapping clause csr_name_map = 0x7a3 <-> "tdata3" val csr_name : csreg -> string -function csr_name(csr) = csr_name_map(csr) overload to_str = {csr_name} /* Extensions may want to add additional CSR registers to the CSR address map. diff --git a/model/riscv_duopod.sail b/model/riscv_duopod.sail index 395a332..b811824 100644 --- a/model/riscv_duopod.sail +++ b/model/riscv_duopod.sail @@ -1,4 +1,6 @@ -// This file depends on the xlen definitions in riscv_xlen.sail. + +$include "prelude.sail" +$include "riscv_xlen64.sail" type regbits = bits(5) @@ -23,7 +25,7 @@ function rX(r) = val wX : (regbits, xlenbits) -> unit effect {wreg} -function wX (r, v) = +function wX(r, v) = if r != 0b00000 then { Xs[unsigned(r)] = v; } diff --git a/model/riscv_ext_regs.sail b/model/riscv_ext_regs.sail index 9ff83b3..d9674f7 100644 --- a/model/riscv_ext_regs.sail +++ b/model/riscv_ext_regs.sail @@ -10,5 +10,22 @@ 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 {wreg} -function ext_rvfi_init () = () +val ext_rvfi_init : unit -> unit effect {rreg, wreg} +function ext_rvfi_init () = { + x1 = x1 // to avoid hook being optimized out +} + + +/*! +THIS(csrno, priv, isWrite) allows an extension to block access to csrno, +at Privilege level priv. It should return true if the access is allowed. +*/ +val ext_check_CSR : (bits(12), Privilege, bool) -> bool +function ext_check_CSR (csrno, p, isWrite) = true + +/*! +THIS is called if ext_check_CSR returns false. It should +cause an appropriate RISCV exception. + */ +val ext_check_CSR_fail : unit->unit +function ext_check_CSR_fail () = () diff --git a/model/riscv_fdext_control.sail b/model/riscv_fdext_control.sail new file mode 100644 index 0000000..7155699 --- /dev/null +++ b/model/riscv_fdext_control.sail @@ -0,0 +1,24 @@ +/* **************************************************************** */ +/* Floating point register file and accessors for F, D extensions */ +/* Floating point CSR and accessors */ +/* **************************************************************** */ + +/* Original version written by Rishiyur S. Nikhil, Sept-Oct 2019 */ + +/* **************************************************************** */ + +/* val clause ext_is_CSR_defined : (csreg, Privilege) -> bool effect {rreg} */ + +function clause ext_is_CSR_defined (0x001, _) = haveFExt() | haveDExt() +function clause ext_is_CSR_defined (0x002, _) = haveFExt() | haveDExt() +function clause ext_is_CSR_defined (0x003, _) = haveFExt() | haveDExt() + +function clause ext_read_CSR (0x001) = Some (EXTZ (fcsr.FFLAGS())) +function clause ext_read_CSR (0x002) = Some (EXTZ (fcsr.FRM())) +function clause ext_read_CSR (0x003) = Some (EXTZ (fcsr.bits())) + +function clause ext_write_CSR (0x001, value) = write_fcsr (fcsr.FRM(), value [4..0]) +function clause ext_write_CSR (0x002, value) = write_fcsr (value [2..0], fcsr.FFLAGS()) +function clause ext_write_CSR (0x003, value) = write_fcsr (value [7..5], value [4..0]) + +/* **************************************************************** */ diff --git a/model/riscv_fdext_regs.sail b/model/riscv_fdext_regs.sail new file mode 100644 index 0000000..59efd22 --- /dev/null +++ b/model/riscv_fdext_regs.sail @@ -0,0 +1,294 @@ +/* **************************************************************** */ +/* Floating point register file and accessors for F, D extensions */ +/* Floating point CSR and accessors */ +/* **************************************************************** */ + +/* Original version written by Rishiyur S. Nikhil, Sept-Oct 2019 */ + +/* **************************************************************** */ +/* Floating point register file */ + +register fs : vector(32, dec, fregtype) + +register f0 : fregtype +register f1 : fregtype +register f2 : fregtype +register f3 : fregtype +register f4 : fregtype +register f5 : fregtype +register f6 : fregtype +register f7 : fregtype +register f8 : fregtype +register f9 : fregtype +register f10 : fregtype +register f11 : fregtype +register f12 : fregtype +register f13 : fregtype +register f14 : fregtype +register f15 : fregtype +register f16 : fregtype +register f17 : fregtype +register f18 : fregtype +register f19 : fregtype +register f20 : fregtype +register f21 : fregtype +register f22 : fregtype +register f23 : fregtype +register f24 : fregtype +register f25 : fregtype +register f26 : fregtype +register f27 : fregtype +register f28 : fregtype +register f29 : fregtype +register f30 : fregtype +register f31 : fregtype + +function dirty_fd_context() -> unit = { + mstatus->FS() = extStatus_to_bits(Dirty); + mstatus->SD() = 0b1 +} + +val rF : forall 'n, 0 <= 'n < 32. regno('n) -> flenbits effect {rreg, escape} +function rF r = { + let v : fregtype = + match r { + 0 => f0, + 1 => f1, + 2 => f2, + 3 => f3, + 4 => f4, + 5 => f5, + 6 => f6, + 7 => f7, + 8 => f8, + 9 => f9, + 10 => f10, + 11 => f11, + 12 => f12, + 13 => f13, + 14 => f14, + 15 => f15, + 16 => f16, + 17 => f17, + 18 => f18, + 19 => f19, + 20 => f20, + 21 => f21, + 22 => f22, + 23 => f23, + 24 => f24, + 25 => f25, + 26 => f26, + 27 => f27, + 28 => f28, + 29 => f29, + 30 => f30, + 31 => f31, + _ => {assert(false, "invalid floating point register number"); zero_freg} + }; + fregval_from_freg(v) +} + +val wF : forall 'n, 0 <= 'n < 32. (regno('n), flenbits) -> unit effect {wreg, escape} +function wF (r, in_v) = { + let v = fregval_into_freg(in_v); + match r { + 0 => f0 = v, + 1 => f1 = v, + 2 => f2 = v, + 3 => f3 = v, + 4 => f4 = v, + 5 => f5 = v, + 6 => f6 = v, + 7 => f7 = v, + 8 => f8 = v, + 9 => f9 = v, + 10 => f10 = v, + 11 => f11 = v, + 12 => f12 = v, + 13 => f13 = v, + 14 => f14 = v, + 15 => f15 = v, + 16 => f16 = v, + 17 => f17 = v, + 18 => f18 = v, + 19 => f19 = v, + 20 => f20 = v, + 21 => f21 = v, + 22 => f22 = v, + 23 => f23 = v, + 24 => f24 = v, + 25 => f25 = v, + 26 => f26 = v, + 27 => f27 = v, + 28 => f28 = v, + 29 => f29 = v, + 30 => f30 = v, + 31 => f31 = v, + _ => assert(false, "invalid floating point register number") + }; + + dirty_fd_context(); + + if get_config_print_reg() + then + /* TODO: will only print bits; should we print in floating point format? */ + print_reg("f" ^ string_of_int(r) ^ " <- " ^ FRegStr(v)); +} + +function rF_bits(i: bits(5)) -> flenbits = rF(unsigned(i)) + +function wF_bits(i: bits(5), data: flenbits) -> unit = { + wF(unsigned(i)) = data +} + +overload F = {rF_bits, wF_bits, rF, wF} + +/* register names */ + +val freg_name_abi : regidx <-> string + +mapping freg_name_abi = { + 0b00000 <-> "ft0", + 0b00001 <-> "ft1", + 0b00010 <-> "ft2", + 0b00011 <-> "ft3", + 0b00100 <-> "ft4", + 0b00101 <-> "ft5", + 0b00110 <-> "ft6", + 0b00111 <-> "ft7", + 0b01000 <-> "fs0", + 0b01001 <-> "fs1", + 0b01010 <-> "fa0", + 0b01011 <-> "fa1", + 0b01100 <-> "fa2", + 0b01101 <-> "fa3", + 0b01110 <-> "fa4", + 0b01111 <-> "fa5", + 0b10000 <-> "fa6", + 0b10001 <-> "fa7", + 0b10010 <-> "fs2", + 0b10011 <-> "fs3", + 0b10100 <-> "fs4", + 0b10101 <-> "fs5", + 0b10110 <-> "fs6", + 0b10111 <-> "fs7", + 0b11000 <-> "fs8", + 0b11001 <-> "fs9", + 0b11010 <-> "fs10", + 0b11011 <-> "fs11", + 0b11100 <-> "ft8", + 0b11101 <-> "ft9", + 0b11110 <-> "ft10", + 0b11111 <-> "ft11" +} + +overload to_str = {freg_name_abi} + +/* mappings for assembly */ + +val freg_name : bits(5) <-> string +mapping freg_name = { + 0b00000 <-> "ft0", + 0b00001 <-> "ft1", + 0b00010 <-> "ft2", + 0b00011 <-> "ft3", + 0b00100 <-> "ft4", + 0b00101 <-> "ft5", + 0b00110 <-> "ft6", + 0b00111 <-> "ft7", + 0b01000 <-> "fs0", + 0b01001 <-> "fs1", + 0b01010 <-> "fa0", + 0b01011 <-> "fa1", + 0b01100 <-> "fa2", + 0b01101 <-> "fa3", + 0b01110 <-> "fa4", + 0b01111 <-> "fa5", + 0b10000 <-> "fa6", + 0b10001 <-> "fa7", + 0b10010 <-> "fs2", + 0b10011 <-> "fs3", + 0b10100 <-> "fs4", + 0b10101 <-> "fs5", + 0b10110 <-> "fs6", + 0b10111 <-> "fs7", + 0b11000 <-> "fs8", + 0b11001 <-> "fs9", + 0b11010 <-> "fs10", + 0b11011 <-> "fs11", + 0b11100 <-> "ft8", + 0b11101 <-> "ft9", + 0b11110 <-> "ft10", + 0b11111 <-> "ft11" +} + +val init_fdext_regs : unit -> unit effect {wreg} +function init_fdext_regs () = { + f0 = zero_freg; + f1 = zero_freg; + f2 = zero_freg; + f3 = zero_freg; + f4 = zero_freg; + f5 = zero_freg; + f6 = zero_freg; + f7 = zero_freg; + f8 = zero_freg; + f9 = zero_freg; + f10 = zero_freg; + f11 = zero_freg; + f12 = zero_freg; + f13 = zero_freg; + f14 = zero_freg; + f15 = zero_freg; + f16 = zero_freg; + f17 = zero_freg; + f18 = zero_freg; + f19 = zero_freg; + f20 = zero_freg; + f21 = zero_freg; + f22 = zero_freg; + f23 = zero_freg; + f24 = zero_freg; + f25 = zero_freg; + f26 = zero_freg; + f27 = zero_freg; + f28 = zero_freg; + f29 = zero_freg; + f30 = zero_freg; + f31 = zero_freg +} + +/* **************************************************************** */ +/* Floating Point CSR */ +/* fflags address 0x001 same as fcrs [4..0] */ +/* frm address 0x002 same as fcrs [7..5] */ +/* fcsr address 0x003 */ + + +bitfield Fcsr : bits(32) = { + FRM : 7 .. 5, + FFLAGS : 4 .. 0, +} + +register fcsr : Fcsr + +val write_fcsr : (bits(3), bits(5)) -> option(xlenbits) effect {rreg, wreg} +function write_fcsr (frm, fflags) = { + fcsr->FRM() = frm; /* Note: frm can be an illegal value, 101, 110, 111 */ + fcsr->FFLAGS() = fflags; + dirty_fd_context(); + Some (EXTZ (fcsr.bits())) +} + +val write_fflags : (bits(5)) -> unit effect {rreg, wreg} +function write_fflags(fflags) = { + fcsr->FFLAGS() = fflags; + dirty_fd_context(); +} + +val write_frm : (bits(3)) -> unit effect {rreg, wreg} +function write_frm(frm) = { + fcsr->FRM() = frm; + dirty_fd_context(); +} diff --git a/model/riscv_fetch.sail b/model/riscv_fetch.sail index 64aff4b..cdda96e 100644 --- a/model/riscv_fetch.sail +++ b/model/riscv_fetch.sail @@ -4,7 +4,7 @@ function isRVC(h : half) -> bool = ~ (h[1 .. 0] == 0b11) -val fetch : unit -> FetchResult effect {escape, rmem, rreg, wmv, wmvt, wreg} +val fetch : unit -> FetchResult effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg} function fetch() -> FetchResult = /* fetch PC check for extensions: extensions return a transformed PC to fetch, * but any exceptions use the untransformed PC. @@ -22,7 +22,7 @@ function fetch() -> FetchResult = * exceptions. */ match mem_read(Execute(), ppclo, 2, false, false, false) { - MemException(e) => F_Error(E_Fetch_Access_Fault(), PC), + MemException(e) => F_Error(e, PC), MemValue(ilo) => { if isRVC(ilo) then F_RVC(ilo) @@ -36,7 +36,7 @@ function fetch() -> FetchResult = TR_Failure(e, _) => F_Error(e, PC_hi), TR_Address(ppchi, _) => { match mem_read(Execute(), ppchi, 2, false, false, false) { - MemException(e) => F_Error(E_Fetch_Access_Fault(), PC_hi), + MemException(e) => F_Error(e, PC_hi), MemValue(ihi) => F_Base(append(ihi, ilo)) } } diff --git a/model/riscv_flen_D.sail b/model/riscv_flen_D.sail new file mode 100644 index 0000000..eabd613 --- /dev/null +++ b/model/riscv_flen_D.sail @@ -0,0 +1,5 @@ +/* Define the FLEN value for the 'D' extension. */ + +type flen : Int = 64 +type flen_bytes : Int = 8 +type flenbits = bits(flen) diff --git a/model/riscv_flen_F.sail b/model/riscv_flen_F.sail new file mode 100644 index 0000000..ad5b381 --- /dev/null +++ b/model/riscv_flen_F.sail @@ -0,0 +1,5 @@ +/* Define the FLEN value for the 'F' extension. */ + +type flen : Int = 32 +type flen_bytes : Int = 4 +type flenbits = bits(flen) diff --git a/model/riscv_freg_type.sail b/model/riscv_freg_type.sail new file mode 100644 index 0000000..3b099db --- /dev/null +++ b/model/riscv_freg_type.sail @@ -0,0 +1,52 @@ +/* Definitions for floating point registers (F and D extensions) */ + +/* default register type */ +type fregtype = flenbits + +/* default zero register */ +let zero_freg : fregtype = EXTZ(0x0) + +/* default register printer */ +val FRegStr : fregtype -> string +function FRegStr(r) = BitStr(r) + +/* conversions */ + +val fregval_from_freg : fregtype -> flenbits +function fregval_from_freg(r) = r + +val fregval_into_freg : flenbits -> fregtype +function fregval_into_freg(v) = v + + +/* Rounding Mode + Rounding modes occur as a 3-bit field in F,D instructions, + and also as a 3-bit 'frm' field in the 'fcsr' CSR. + RISC-V uses the following IEEE-defined rounding modes. +*/ + +enum rounding_mode = {RM_RNE, RM_RTZ, RM_RDN, RM_RUP, RM_RMM, RM_DYN} + +enum f_madd_op_S = {FMADD_S, FMSUB_S, FNMSUB_S, FNMADD_S} + +enum f_bin_rm_op_S = {FADD_S, FSUB_S, FMUL_S, FDIV_S} + +enum f_un_rm_op_S = {FSQRT_S, FCVT_W_S, FCVT_WU_S, FCVT_S_W, FCVT_S_WU, // RV32 and RV64 + FCVT_L_S, FCVT_LU_S, FCVT_S_L, FCVT_S_LU} // RV64 only + +enum f_un_op_S = {FCLASS_S, FMV_X_W, FMV_W_X} /* RV32 and RV64 */ + +enum f_bin_op_S = {FSGNJ_S, FSGNJN_S, FSGNJX_S, FMIN_S, FMAX_S, FEQ_S, FLT_S, FLE_S} + +enum f_madd_op_D = {FMADD_D, FMSUB_D, FNMSUB_D, FNMADD_D} + +enum f_bin_rm_op_D = {FADD_D, FSUB_D, FMUL_D, FDIV_D} + +enum f_un_rm_op_D = {FSQRT_D, FCVT_W_D, FCVT_WU_D, FCVT_D_W, FCVT_D_WU, // RV32 and RV64 + FCVT_S_D, FCVT_D_S, + FCVT_L_D, FCVT_LU_D, FCVT_D_L, FCVT_D_LU} // RV64 only + +enum f_bin_op_D = {FSGNJ_D, FSGNJN_D, FSGNJX_D, FMIN_D, FMAX_D, FEQ_D, FLT_D, FLE_D} + +enum f_un_op_D = {FCLASS_D, /* RV32 and RV64 */ + FMV_X_D, FMV_D_X} /* RV64 only */ diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail index 7eb01c5..e760b90 100644 --- a/model/riscv_insts_aext.sail +++ b/model/riscv_insts_aext.sail @@ -198,21 +198,30 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = { let eares : MemoryOpResult(unit) = match (width, sizeof(xlen)) { (WORD, _) => mem_write_ea(addr, 4, aq & rl, rl, true), (DOUBLE, 64) => mem_write_ea(addr, 8, aq & rl, rl, true), - _ => internal_error ("AMO expected WORD or DOUBLE") + _ => internal_error("AMO expected WORD or DOUBLE") + }; + let is_unsigned : bool = match op { + AMOMINU => true, + AMOMAXU => true, + _ => false + }; + let rs2_val : xlenbits = match width { + WORD => if is_unsigned then EXTZ(X(rs2)[31..0]) else EXTS(X(rs2)[31..0]), + DOUBLE => X(rs2), + _ => internal_error("AMO expected WORD or DOUBLE") }; - rs2_val : xlenbits = X(rs2); match (eares) { MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL }, MemValue(_) => { - let rval : MemoryOpResult(xlenbits) = match (width, sizeof(xlen)) { - (WORD, _) => extend_value(false, mem_read(ReadWrite(Data), addr, 4, aq, aq & rl, true)), - (DOUBLE, 64) => extend_value(false, mem_read(ReadWrite(Data), addr, 8, aq, aq & rl, true)), - _ => internal_error ("AMO expected WORD or DOUBLE") + let mval : MemoryOpResult(xlenbits) = match (width, sizeof(xlen)) { + (WORD, _) => extend_value(is_unsigned, mem_read(ReadWrite(Data), addr, 4, aq, aq & rl, true)), + (DOUBLE, 64) => extend_value(is_unsigned, mem_read(ReadWrite(Data), addr, 8, aq, aq & rl, true)), + _ => internal_error("AMO expected WORD or DOUBLE") }; - match (rval) { + match (mval) { MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL }, MemValue(loaded) => { - result : xlenbits = + let result : xlenbits = match op { AMOSWAP => rs2_val, AMOADD => rs2_val + loaded, @@ -228,14 +237,18 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = { AMOMINU => to_bits(sizeof(xlen), min(unsigned(rs2_val), unsigned(loaded))), AMOMAXU => to_bits(sizeof(xlen), max(unsigned(rs2_val), unsigned(loaded))) }; - + let rval : xlenbits = match width { + WORD => EXTS(loaded[31..0]), + DOUBLE => loaded, + _ => internal_error("AMO expected WORD or DOUBLE") + }; let wval : MemoryOpResult(bool) = match (width, sizeof(xlen)) { (WORD, _) => mem_write_value(addr, 4, result[31..0], aq & rl, rl, true), (DOUBLE, 64) => mem_write_value(addr, 8, result, aq & rl, rl, true), _ => internal_error("AMO expected WORD or DOUBLE") }; match (wval) { - MemValue(true) => { X(rd) = loaded; RETIRE_SUCCESS }, + MemValue(true) => { X(rd) = rval; RETIRE_SUCCESS }, MemValue(false) => { internal_error("AMO got false from mem_write_value") }, MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL } } @@ -266,4 +279,4 @@ mapping amo_mnemonic : amoop <-> string = { } mapping clause assembly = AMO(op, aq, rl, rs2, rs1, width, rd) - <-> amo_mnemonic(op) ^ "." ^ size_mnemonic(width) ^ maybe_aq(aq) ^ maybe_rl(rl) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) + <-> amo_mnemonic(op) ^ "." ^ size_mnemonic(width) ^ maybe_aq(aq) ^ maybe_rl(rl) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs2) ^ sep() ^ "(" ^ reg_name(rs1) ^ ")" diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail index d80d34d..bc86859 100644 --- a/model/riscv_insts_base.sail +++ b/model/riscv_insts_base.sail @@ -714,9 +714,11 @@ mapping clause encdec = MRET() <-> 0b0011000 @ 0b00010 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 function clause execute MRET() = { - if cur_privilege == Machine - then set_next_pc(exception_handler(cur_privilege, CTL_MRET(), PC)) - else handle_illegal(); + if cur_privilege != Machine + then handle_illegal() + else if ~(ext_check_xret_priv (Machine)) + then ext_fail_xret_priv () + else set_next_pc(exception_handler(cur_privilege, CTL_MRET(), PC)); RETIRE_FAIL } @@ -729,15 +731,16 @@ mapping clause encdec = SRET() <-> 0b0001000 @ 0b00010 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 function clause execute SRET() = { - match cur_privilege { - User => handle_illegal(), - Supervisor => if (~ (haveSupMode ())) | mstatus.TSR() == 0b1 - then handle_illegal() - else set_next_pc(exception_handler(cur_privilege, CTL_SRET(), PC)), - Machine => if (~ (haveSupMode ())) - then handle_illegal() - else set_next_pc(exception_handler(cur_privilege, CTL_SRET(), PC)) + let sret_illegal : bool = match cur_privilege { + User => true, + Supervisor => ~ (haveSupMode ()) | mstatus.TSR() == 0b1, + Machine => ~ (haveSupMode ()) }; + if sret_illegal + then handle_illegal() + else if ~(ext_check_xret_priv (Supervisor)) + then ext_fail_xret_priv () + else set_next_pc(exception_handler(cur_privilege, CTL_SRET(), PC)); RETIRE_FAIL } diff --git a/model/riscv_insts_begin.sail b/model/riscv_insts_begin.sail index b27711b..661a353 100644 --- a/model/riscv_insts_begin.sail +++ b/model/riscv_insts_begin.sail @@ -12,7 +12,7 @@ scattered function execute val assembly : ast <-> string scattered mapping assembly -val encdec : ast <-> bits(32) +val encdec : ast <-> bits(32) effect {rreg} scattered mapping encdec val encdec_compressed : ast <-> bits(16) diff --git a/model/riscv_insts_dext.sail b/model/riscv_insts_dext.sail new file mode 100644 index 0000000..9e68248 --- /dev/null +++ b/model/riscv_insts_dext.sail @@ -0,0 +1,922 @@ +/* **************************************************************** */ +/* This file specifies the instructions in the D extension */ +/* (double precision floating point). */ + +/* RISC-V follows IEEE 754-2008 floating point arithmetic standard. */ + +/* Original version written by Rishiyur S. Nikhil, Sept-Oct 2019 */ + +/* **************************************************************** */ +/* IMPORTANT! */ +/* The files 'riscv_insts_fext.sail' and 'riscv_insts_dext.sail' */ +/* define the F and D extensions, respectively. */ +/* The texts follow each other very closely; please try to maintain */ +/* this correspondence as the files are maintained for bug-fixes, */ +/* improvements, and version updates. */ + +/* **************************************************************** */ +/* Note: Rounding Modes and Floating point accrued exception flags */ +/* are defined in riscv_insts_fext.sail. */ +/* In RISC-V, the D extension requires the F extension, so that */ +/* should have been processed before this one. */ + +/* **************************************************************** */ +/* S and D value structure (sign, exponent, mantissa) */ + +/* TODO: this should be a 'mapping' */ +val fsplit_D : bits(64) -> (bits(1), bits(11), bits(52)) +function fsplit_D x64 = (x64[63..63], x64[62..52], x64[51..0]) + +val fmake_D : (bits(1), bits(11), bits(52)) -> bits(64) +function fmake_D (sign, exp, mant) = sign @ exp @ mant + +/* ---- Canonical NaNs */ + +function canonical_NaN_D() -> bits(64) = 0x_7ff8_0000_0000_0000 + +/* ---- Structure tests */ + +val f_is_neg_inf_D : bits(64) -> bool +function f_is_neg_inf_D x64 = { + let (sign, exp, mant) = fsplit_D (x64); + ( (sign == 0b1) + & (exp == ones()) + & (mant == zeros())) +} + +val f_is_neg_norm_D : bits(64) -> bool +function f_is_neg_norm_D x64 = { + let (sign, exp, mant) = fsplit_D (x64); + ( (sign == 0b1) + & (exp != zeros()) + & (exp != ones())) +} + +val f_is_neg_subnorm_D : bits(64) -> bool +function f_is_neg_subnorm_D x64 = { + let (sign, exp, mant) = fsplit_D (x64); + ( (sign == 0b1) + & (exp == zeros()) + & (mant != zeros())) +} + +val f_is_neg_zero_D : bits(64) -> bool +function f_is_neg_zero_D x64 = { + let (sign, exp, mant) = fsplit_D (x64); + ( (sign == ones()) + & (exp == zeros()) + & (mant == zeros())) +} + +val f_is_pos_zero_D : bits(64) -> bool +function f_is_pos_zero_D x64 = { + let (sign, exp, mant) = fsplit_D (x64); + ( (sign == zeros()) + & (exp == zeros()) + & (mant == zeros())) +} + +val f_is_pos_subnorm_D : bits(64) -> bool +function f_is_pos_subnorm_D x64 = { + let (sign, exp, mant) = fsplit_D (x64); + ( (sign == zeros()) + & (exp == zeros()) + & (mant != zeros())) +} + +val f_is_pos_norm_D : bits(64) -> bool +function f_is_pos_norm_D x64 = { + let (sign, exp, mant) = fsplit_D (x64); + ( (sign == zeros()) + & (exp != zeros()) + & (exp != ones())) +} + +val f_is_pos_inf_D : bits(64) -> bool +function f_is_pos_inf_D x64 = { + let (sign, exp, mant) = fsplit_D (x64); + ( (sign == zeros()) + & (exp == ones()) + & (mant == zeros())) +} + +val f_is_SNaN_D : bits(64) -> bool +function f_is_SNaN_D x64 = { + let (sign, exp, mant) = fsplit_D (x64); + ( (exp == ones()) + & (mant [51] == bitzero) + & (mant != zeros())) +} + +val f_is_QNaN_D : bits(64) -> bool +function f_is_QNaN_D x64 = { + let (sign, exp, mant) = fsplit_D (x64); + ( (exp == ones()) + & (mant [51] == bitone)) +} + +/* **************************************************************** */ +/* Help functions used in the semantic functions */ + +val negate_D : bits(64) -> bits(64) +function negate_D (x64) = { + let (sign, exp, mant) = fsplit_D (x64); + let new_sign = if (sign == 0b0) then 0b1 else 0b0; + fmake_D (new_sign, exp, mant) +} + +val feq_quiet_D : (bits(64), bits (64)) -> (bool, bits(5)) +function feq_quiet_D (v1, v2) = { + let (s1, e1, m1) = fsplit_D (v1); + let (s2, e2, m2) = fsplit_D (v2); + + let v1Is0 = f_is_neg_zero_D(v1) | f_is_pos_zero_D(v1); + let v2Is0 = f_is_neg_zero_D(v2) | f_is_pos_zero_D(v2); + + let result = ((v1 == v2) | (v1Is0 & v2Is0)); + + let fflags = if (f_is_SNaN_D(v1) | f_is_SNaN_D(v2)) then + nvFlag() + else + zeros(); + + (result, fflags) +} + +val flt_D : (bits(64), bits (64), bool) -> (bool, bits(5)) +function flt_D (v1, v2, is_quiet) = { + let (s1, e1, m1) = fsplit_D (v1); + let (s2, e2, m2) = fsplit_D (v2); + + let v1IsNaN = f_is_QNaN_D(v1) | f_is_SNaN_D(v1); + let v2IsNaN = f_is_QNaN_D(v2) | f_is_SNaN_D(v2); + + let result : bool = + if (s1 == 0b0) & (s2 == 0b0) then + if (e1 == e2) then + unsigned (m1) < unsigned (m2) + else + unsigned (e1) < unsigned (e2) + else if (s1 == 0b0) & (s2 == 0b1) then + false + else if (s1 == 0b1) & (s2 == 0b0) then + true + else + if (e1 == e2) then + unsigned (m1) > unsigned (m2) + else + unsigned (e1) > unsigned (e2); + + let fflags = if is_quiet then + if (f_is_SNaN_D(v1) | f_is_SNaN_D(v2)) then + nvFlag() + else + zeros() + else + if (v1IsNaN | v2IsNaN) then + nvFlag() + else + zeros(); + + (result, fflags) +} + +val fle_D : (bits(64), bits (64), bool) -> (bool, bits(5)) +function fle_D (v1, v2, is_quiet) = { + let (s1, e1, m1) = fsplit_D (v1); + let (s2, e2, m2) = fsplit_D (v2); + + let v1IsNaN = f_is_QNaN_D(v1) | f_is_SNaN_D(v1); + let v2IsNaN = f_is_QNaN_D(v2) | f_is_SNaN_D(v2); + + let v1Is0 = f_is_neg_zero_D(v1) | f_is_pos_zero_D(v1); + let v2Is0 = f_is_neg_zero_D(v2) | f_is_pos_zero_D(v2); + + let result : bool = + if (s1 == 0b0) & (s2 == 0b0) then + if (e1 == e2) then + unsigned (m1) <= unsigned (m2) + else + unsigned (e1) < unsigned (e2) + else if (s1 == 0b0) & (s2 == 0b1) then + (v1Is0 & v2Is0) /* Equal in this case (+0=-0) */ + else if (s1 == 0b1) & (s2 == 0b0) then + true + else + if (e1 == e2) then + unsigned (m1) >= unsigned (m2) + else + unsigned (e1) > unsigned (e2); + + let fflags = if is_quiet then + if (f_is_SNaN_D(v1) | f_is_SNaN_D(v2)) then + nvFlag() + else + zeros() + else + if (v1IsNaN | v2IsNaN) then + nvFlag() + else + zeros(); + + (result, fflags) +} + +/* ****************************************************************** */ +/* Floating-point loads */ +/* These are defined in: riscv_insts_fext.sail */ + +/* ****************************************************************** */ +/* Floating-point stores */ +/* These are defined in: riscv_insts_fext.sail */ + +/* ****************************************************************** */ +/* Fused multiply-add */ + +/* AST */ + +union clause ast = F_MADD_TYPE_D : (regidx, regidx, regidx, rounding_mode, regidx, f_madd_op_D) + +/* AST <-> Binary encoding ================================ */ + +mapping clause encdec = + F_MADD_TYPE_D(rs3, rs2, rs1, rm, rd, FMADD_D) if is_RV32D_or_RV64D() +<-> rs3 @ 0b01 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_0011 if is_RV32D_or_RV64D() + +mapping clause encdec = + F_MADD_TYPE_D(rs3, rs2, rs1, rm, rd, FMSUB_D) if is_RV32D_or_RV64D() +<-> rs3 @ 0b01 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_0111 if is_RV32D_or_RV64D() + +mapping clause encdec = + F_MADD_TYPE_D(rs3, rs2, rs1, rm, rd, FNMSUB_D) if is_RV32D_or_RV64D() +<-> rs3 @ 0b01 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_1011 if is_RV32D_or_RV64D() + +mapping clause encdec = + F_MADD_TYPE_D(rs3, rs2, rs1, rm, rd, FNMADD_D) if is_RV32D_or_RV64D() +<-> rs3 @ 0b01 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_1111 if is_RV32D_or_RV64D() + +/* Execution semantics ================================ */ + +function clause execute (F_MADD_TYPE_D(rs3, rs2, rs1, rm, rd, op)) = { + let rs1_val_64b = F(rs1); + let rs2_val_64b = F(rs2); + let rs3_val_64b = F(rs3); + let rm_3b = encdec_rounding_mode (select_instr_or_fcsr_rm (rm)); + let (fflags, rd_val_64b) : (bits(5), bits(64)) = + match op { + FMADD_D => riscv_f64MulAdd (rm_3b, rs1_val_64b, rs2_val_64b, rs3_val_64b), + FMSUB_D => riscv_f64MulAdd (rm_3b, rs1_val_64b, rs2_val_64b, negate_D (rs3_val_64b)), + FNMSUB_D => riscv_f64MulAdd (rm_3b, negate_D (rs1_val_64b), rs2_val_64b, rs3_val_64b), + FNMADD_D => riscv_f64MulAdd (rm_3b, negate_D (rs1_val_64b), rs2_val_64b, negate_D (rs3_val_64b)) + }; + write_fflags(fflags); + F(rd) = rd_val_64b; + RETIRE_SUCCESS +} + +/* AST -> Assembly notation ================================ */ + +mapping f_madd_type_mnemonic_D : f_madd_op_D <-> string = { + FMADD_D <-> "fmadd.d", + FMSUB_D <-> "fmsub.d", + FNMSUB_D <-> "fnmsub.d", + FNMADD_D <-> "fnmadd.d" +} + +mapping clause assembly = F_MADD_TYPE_D(rs3, rs2, rs1, rm, rd, op) + <-> f_madd_type_mnemonic_D(op) + ^ spc() ^ freg_name(rd) + ^ sep() ^ freg_name(rs1) + ^ sep() ^ freg_name(rs2) + ^ sep() ^ freg_name(rs3) + ^ sep() ^ frm_mnemonic(rm) + +/* ****************************************************************** */ +/* Binary ops with rounding mode */ + +/* AST */ + +union clause ast = F_BIN_RM_TYPE_D : (regidx, regidx, rounding_mode, regidx, f_bin_rm_op_D) + +/* AST <-> Binary encoding ================================ */ + +mapping clause encdec = + F_BIN_RM_TYPE_D(rs2, rs1, rm, rd, FADD_D) if is_RV32D_or_RV64D() +<-> 0b000_0001 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32D_or_RV64D() + +mapping clause encdec = + F_BIN_RM_TYPE_D(rs2, rs1, rm, rd, FSUB_D) if is_RV32D_or_RV64D() +<-> 0b000_0101 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32D_or_RV64D() + +mapping clause encdec = + F_BIN_RM_TYPE_D(rs2, rs1, rm, rd, FMUL_D) if is_RV32D_or_RV64D() +<-> 0b000_1001 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32D_or_RV64D() + +mapping clause encdec = + F_BIN_RM_TYPE_D(rs2, rs1, rm, rd, FDIV_D) if is_RV32D_or_RV64D() +<-> 0b000_1101 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32D_or_RV64D() + +/* Execution semantics ================================ */ + +function clause execute (F_BIN_RM_TYPE_D(rs2, rs1, rm, rd, op)) = { + let rs1_val_64b = F(rs1); + let rs2_val_64b = F(rs2); + let rm_3b = encdec_rounding_mode (select_instr_or_fcsr_rm (rm)); + let (fflags, rd_val_64b) : (bits(5), bits(64)) = match op { + FADD_D => riscv_f64Add (rm_3b, rs1_val_64b, rs2_val_64b), + FSUB_D => riscv_f64Sub (rm_3b, rs1_val_64b, rs2_val_64b), + FMUL_D => riscv_f64Mul (rm_3b, rs1_val_64b, rs2_val_64b), + FDIV_D => riscv_f64Div (rm_3b, rs1_val_64b, rs2_val_64b) + }; + write_fflags(fflags); + F(rd) = rd_val_64b; + RETIRE_SUCCESS +} + +/* AST -> Assembly notation ================================ */ + +mapping f_bin_rm_type_mnemonic_D : f_bin_rm_op_D <-> string = { + FADD_D <-> "fadd.d", + FSUB_D <-> "fsub.d", + FMUL_D <-> "fmul.d", + FDIV_D <-> "fdiv.d" +} + +mapping clause assembly = F_BIN_RM_TYPE_D(rs2, rs1, rm, rd, op) + <-> f_bin_rm_type_mnemonic_D(op) + ^ spc() ^ freg_name(rd) + ^ sep() ^ freg_name(rs1) + ^ sep() ^ freg_name(rs2) + ^ sep() ^ frm_mnemonic(rm) + +/* ****************************************************************** */ +/* Unary with rounding mode */ + +/* AST */ + +union clause ast = F_UN_RM_TYPE_D : (regidx, rounding_mode, regidx, f_un_rm_op_D) + +/* AST <-> Binary encoding ================================ */ + +mapping clause encdec = + F_UN_RM_TYPE_D(rs1, rm, rd, FSQRT_D) if is_RV32D_or_RV64D() +<-> 0b010_1101 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32D_or_RV64D() + +mapping clause encdec = + F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_W_D) if is_RV32D_or_RV64D() +<-> 0b110_0001 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32D_or_RV64D() + +mapping clause encdec = + F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_WU_D) if is_RV32D_or_RV64D() +<-> 0b110_0001 @ 0b00001 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32D_or_RV64D() + +mapping clause encdec = + F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_W) if is_RV32D_or_RV64D() +<-> 0b110_1001 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32D_or_RV64D() + +mapping clause encdec = + F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_WU) if is_RV32D_or_RV64D() +<-> 0b110_1001 @ 0b00001 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32D_or_RV64D() + +mapping clause encdec = + F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_S_D) if is_RV32D_or_RV64D() +<-> 0b010_0000 @ 0b00001 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32D_or_RV64D() + +mapping clause encdec = + F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_S) if is_RV32D_or_RV64D() +<-> 0b010_0001 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32D_or_RV64D() + +/* D instructions, RV64 only */ + +mapping clause encdec = + F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_L_D) if is_RV64D() +<-> 0b110_0001 @ 0b00010 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV64D() + +mapping clause encdec = + F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_LU_D) if is_RV64D() +<-> 0b110_0001 @ 0b00011 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV64D() + +mapping clause encdec = + F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_L) if is_RV64D() +<-> 0b110_1001 @ 0b00010 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV64D() + +mapping clause encdec = + F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_LU) if is_RV64D() +<-> 0b110_1001 @ 0b00011 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV64D() + +/* Execution semantics ================================ */ + +function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FSQRT_D)) = { + let rs1_val_D = F(rs1); + let rm_3b = encdec_rounding_mode (select_instr_or_fcsr_rm (rm)); + + let (fflags, rd_val_D) = riscv_f64Sqrt (rm_3b, rs1_val_D); + + write_fflags(fflags); + F(rd) = rd_val_D; + RETIRE_SUCCESS +} + +function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_W_D)) = { + let rs1_val_D = F(rs1); + let rm_3b = encdec_rounding_mode (select_instr_or_fcsr_rm (rm)); + + let (fflags, rd_val_W) = riscv_f64ToI32 (rm_3b, rs1_val_D); + + write_fflags(fflags); + X(rd) = EXTS (rd_val_W); + RETIRE_SUCCESS +} + +function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_WU_D)) = { + let rs1_val_D = F(rs1); + let rm_3b = encdec_rounding_mode (select_instr_or_fcsr_rm (rm)); + + let (fflags, rd_val_WU) = riscv_f64ToUi32 (rm_3b, rs1_val_D); + + write_fflags(fflags); + X(rd) = EXTS (rd_val_WU); + RETIRE_SUCCESS +} + +function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_W)) = { + let rs1_val_W = X(rs1) [31..0]; + let rm_3b = encdec_rounding_mode (select_instr_or_fcsr_rm (rm)); + + let (fflags, rd_val_D) = riscv_i32ToF64 (rm_3b, rs1_val_W); + + write_fflags(fflags); + F(rd) = rd_val_D; + RETIRE_SUCCESS +} + +function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_WU)) = { + let rs1_val_WU = X(rs1) [31..0]; + let rm_3b = encdec_rounding_mode (select_instr_or_fcsr_rm (rm)); + + let (fflags, rd_val_D) = riscv_ui32ToF64 (rm_3b, rs1_val_WU); + + write_fflags(fflags); + F(rd) = rd_val_D; + RETIRE_SUCCESS +} + +function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_S_D)) = { + let rs1_val_D = F(rs1); + let rm_3b = encdec_rounding_mode (select_instr_or_fcsr_rm (rm)); + + let (fflags, rd_val_S) = riscv_f64ToF32 (rm_3b, rs1_val_D); + + write_fflags(fflags); + F(rd) = nan_box (rd_val_S); + RETIRE_SUCCESS +} + +function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_S)) = { + let rs1_val_S = nan_unbox (F(rs1)); + let rm_3b = encdec_rounding_mode (select_instr_or_fcsr_rm (rm)); + + let (fflags, rd_val_D) = riscv_f32ToF64 (rm_3b, rs1_val_S); + + write_fflags(fflags); + F(rd) = rd_val_D; + RETIRE_SUCCESS +} + +function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_L_D)) = { + let rs1_val_D = F(rs1); + let rm_3b = encdec_rounding_mode (select_instr_or_fcsr_rm (rm)); + + let (fflags, rd_val_L) = riscv_f64ToI64 (rm_3b, rs1_val_D); + + write_fflags(fflags); + X(rd) = rd_val_L; + RETIRE_SUCCESS +} + +function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_LU_D)) = { + let rs1_val_D = F(rs1); + let rm_3b = encdec_rounding_mode (select_instr_or_fcsr_rm (rm)); + + let (fflags, rd_val_LU) = riscv_f64ToUi64 (rm_3b, rs1_val_D); + + write_fflags(fflags); + X(rd) = rd_val_LU; + RETIRE_SUCCESS +} + +function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_L)) = { + let rs1_val_L = X(rs1); + let rm_3b = encdec_rounding_mode (select_instr_or_fcsr_rm (rm)); + + let (fflags, rd_val_D) = riscv_i64ToF64 (rm_3b, rs1_val_L); + + write_fflags(fflags); + F(rd) = rd_val_D; + RETIRE_SUCCESS +} + +function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_LU)) = { + let rs1_val_LU = X(rs1); + let rm_3b = encdec_rounding_mode (select_instr_or_fcsr_rm (rm)); + + let (fflags, rd_val_D) = riscv_ui64ToF64 (rm_3b, rs1_val_LU); + + write_fflags(fflags); + F(rd) = rd_val_D; + RETIRE_SUCCESS +} + +/* AST -> Assembly notation ================================ */ + +mapping f_un_rm_type_mnemonic_D : f_un_rm_op_D <-> string = { + FSQRT_D <-> "fsqrt.d", + FCVT_W_D <-> "fcvt.w.d", + FCVT_WU_D <-> "fcvt.wu.d", + FCVT_D_W <-> "fcvt.d.w", + FCVT_D_WU <-> "fcvt.d.wu", + + FCVT_L_D <-> "fcvt.l.d", + FCVT_LU_D <-> "fcvt.lu.d", + FCVT_D_L <-> "fcvt.d.l", + FCVT_D_LU <-> "fcvt.d.lu", + + FCVT_S_D <-> "fcvt.s.d", + FCVT_D_S <-> "fcvt.d.s" +} + +mapping clause assembly = F_UN_RM_TYPE_D(rs1, rm, rd, FSQRT_D) + <-> f_un_rm_type_mnemonic_D(FSQRT_D) + ^ spc() ^ freg_name(rd) + ^ sep() ^ freg_name(rs1) + ^ sep() ^ frm_mnemonic(rm) + +mapping clause assembly = F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_W_D) + <-> f_un_rm_type_mnemonic_D(FCVT_W_D) + ^ spc() ^ reg_name(rd) + ^ sep() ^ freg_name(rs1) + ^ sep() ^ frm_mnemonic(rm) + +mapping clause assembly = F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_WU_D) + <-> f_un_rm_type_mnemonic_D(FCVT_WU_D) + ^ spc() ^ reg_name(rd) + ^ sep() ^ freg_name(rs1) + ^ sep() ^ frm_mnemonic(rm) + +mapping clause assembly = F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_W) + <-> f_un_rm_type_mnemonic_D(FCVT_D_W) + ^ spc() ^ freg_name(rd) + ^ sep() ^ reg_name(rs1) + ^ sep() ^ frm_mnemonic(rm) + +mapping clause assembly = F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_WU) + <-> f_un_rm_type_mnemonic_D(FCVT_D_WU) + ^ spc() ^ freg_name(rd) + ^ sep() ^ reg_name(rs1) + ^ sep() ^ frm_mnemonic(rm) + +mapping clause assembly = F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_L_D) + <-> f_un_rm_type_mnemonic_D(FCVT_L_D) + ^ spc() ^ reg_name(rd) + ^ sep() ^ freg_name(rs1) + ^ sep() ^ frm_mnemonic(rm) + +mapping clause assembly = F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_LU_D) + <-> f_un_rm_type_mnemonic_D(FCVT_LU_D) + ^ spc() ^ reg_name(rd) + ^ sep() ^ freg_name(rs1) + ^ sep() ^ frm_mnemonic(rm) + +mapping clause assembly = F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_L) + <-> f_un_rm_type_mnemonic_D(FCVT_D_L) + ^ spc() ^ freg_name(rd) + ^ sep() ^ reg_name(rs1) + ^ sep() ^ frm_mnemonic(rm) + +mapping clause assembly = F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_LU) + <-> f_un_rm_type_mnemonic_D(FCVT_D_LU) + ^ spc() ^ freg_name(rd) + ^ sep() ^ reg_name(rs1) + ^ sep() ^ frm_mnemonic(rm) + +mapping clause assembly = F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_S_D) + <-> f_un_rm_type_mnemonic_D(FCVT_S_D) + ^ spc() ^ freg_name(rd) + ^ sep() ^ freg_name(rs1) + ^ sep() ^ frm_mnemonic(rm) + +mapping clause assembly = F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_S) + <-> f_un_rm_type_mnemonic_D(FCVT_D_S) + ^ spc() ^ freg_name(rd) + ^ sep() ^ freg_name(rs1) + ^ sep() ^ frm_mnemonic(rm) + +/* ****************************************************************** */ +/* Binary, no rounding mode */ + +/* AST */ + +union clause ast = F_BIN_TYPE_D : (regidx, regidx, regidx, f_bin_op_D) + +/* AST <-> Binary encoding ================================ */ + +mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FSGNJ_D) if is_RV32D_or_RV64D() + <-> 0b001_0001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011 if is_RV32D_or_RV64D() + +mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FSGNJN_D) if is_RV32D_or_RV64D() + <-> 0b001_0001 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011 if is_RV32D_or_RV64D() + +mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FSGNJX_D) if is_RV32D_or_RV64D() + <-> 0b001_0001 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011 if is_RV32D_or_RV64D() + +mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FMIN_D) if is_RV32D_or_RV64D() + <-> 0b001_0101 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011 if is_RV32D_or_RV64D() + +mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FMAX_D) if is_RV32D_or_RV64D() + <-> 0b001_0101 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011 if is_RV32D_or_RV64D() + +mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FEQ_D) if is_RV32D_or_RV64D() + <-> 0b101_0001 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011 if is_RV32D_or_RV64D() + +mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FLT_D) if is_RV32D_or_RV64D() + <-> 0b101_0001 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011 if is_RV32D_or_RV64D() + +mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FLE_D) if is_RV32D_or_RV64D() + <-> 0b101_0001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011 if is_RV32D_or_RV64D() + +/* Execution semantics ================================ */ + +function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FSGNJ_D)) = { + let rs1_val_D = F(rs1); + let rs2_val_D = F(rs2); + let (s1, e1, m1) = fsplit_D (rs1_val_D); + let (s2, e2, m2) = fsplit_D (rs2_val_D); + let rd_val_D = fmake_D (s2, e1, m1); + let fflags = 0b_00000; + write_fflags(fflags); + F(rd) = rd_val_D; + RETIRE_SUCCESS +} + +function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FSGNJN_D)) = { + let rs1_val_D = F(rs1); + let rs2_val_D = F(rs2); + let (s1, e1, m1) = fsplit_D (rs1_val_D); + let (s2, e2, m2) = fsplit_D (rs2_val_D); + let rd_val_D = fmake_D (0b1 ^ s2, e1, m1); + let fflags = 0b_00000; + write_fflags(fflags); + F(rd) = rd_val_D; + RETIRE_SUCCESS +} + +function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FSGNJX_D)) = { + let rs1_val_D = F(rs1); + let rs2_val_D = F(rs2); + let (s1, e1, m1) = fsplit_D (rs1_val_D); + let (s2, e2, m2) = fsplit_D (rs2_val_D); + let rd_val_D = fmake_D (s1 ^ s2, e1, m1); + let fflags = 0b_00000; + write_fflags(fflags); + F(rd) = rd_val_D; + RETIRE_SUCCESS +} + +function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FMIN_D)) = { + let rs1_val_D = F(rs1); + let rs2_val_D = F(rs2); + + let is_quiet = true; + let (rs1_lt_rs2, fflags) = fle_D (rs1_val_D, rs2_val_D, is_quiet); + + let rd_val_D = if (f_is_SNaN_D(rs1_val_D) & f_is_SNaN_D(rs2_val_D)) then canonical_NaN_D() + else if f_is_SNaN_D(rs1_val_D) then rs2_val_D + else if f_is_SNaN_D(rs2_val_D) then rs1_val_D + else if (f_is_QNaN_D(rs1_val_D) & f_is_QNaN_D(rs2_val_D)) then canonical_NaN_D() + else if f_is_QNaN_D(rs1_val_D) then rs2_val_D + else if f_is_QNaN_D(rs2_val_D) then rs1_val_D + else if (f_is_neg_zero_D(rs1_val_D) & f_is_pos_zero_D(rs2_val_D)) then rs1_val_D + else if (f_is_neg_zero_D(rs2_val_D) & f_is_pos_zero_D(rs1_val_D)) then rs2_val_D + else if rs1_lt_rs2 then rs1_val_D + else /* (not rs1_lt_rs2) */ rs2_val_D; + + write_fflags(fflags); + F(rd) = rd_val_D; + RETIRE_SUCCESS +} + +function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FMAX_D)) = { + let rs1_val_D = F(rs1); + let rs2_val_D = F(rs2); + + let is_quiet = true; + let (rs2_lt_rs1, fflags) = fle_D (rs2_val_D, rs1_val_D, is_quiet); + + let rd_val_D = if (f_is_SNaN_D(rs1_val_D) & f_is_SNaN_D(rs2_val_D)) then canonical_NaN_D() + else if f_is_SNaN_D(rs1_val_D) then rs2_val_D + else if f_is_SNaN_D(rs2_val_D) then rs1_val_D + else if (f_is_QNaN_D(rs1_val_D) & f_is_QNaN_D(rs2_val_D)) then canonical_NaN_D() + else if f_is_QNaN_D(rs1_val_D) then rs2_val_D + else if f_is_QNaN_D(rs2_val_D) then rs1_val_D + else if (f_is_neg_zero_D(rs1_val_D) & f_is_pos_zero_D(rs2_val_D)) then rs2_val_D + else if (f_is_neg_zero_D(rs2_val_D) & f_is_pos_zero_D(rs1_val_D)) then rs1_val_D + else if rs2_lt_rs1 then rs1_val_D + else /* (not rs2_lt_rs1) */ rs2_val_D; + + write_fflags(fflags); + F(rd) = rd_val_D; + RETIRE_SUCCESS +} + +function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FEQ_D)) = { + let rs1_val_D = F(rs1); + let rs2_val_D = F(rs2); + + let (rs1_eq_rs2, fflags) = feq_quiet_D (rs1_val_D, rs2_val_D); + + let rd_val : xlenbits = + if (f_is_SNaN_D(rs1_val_D) | f_is_SNaN_D(rs2_val_D)) then zeros() + else if (f_is_QNaN_D(rs1_val_D) | f_is_QNaN_D(rs2_val_D)) then zeros() + else if rs1_eq_rs2 then EXTZ(0b1) + else zeros(); + + write_fflags(fflags); + X(rd) = rd_val; + RETIRE_SUCCESS +} + +function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FLT_D)) = { + let rs1_val_D = F(rs1); + let rs2_val_D = F(rs2); + + let is_quiet = false; + let (rs1_lt_rs2, fflags) = flt_D (rs1_val_D, rs2_val_D, is_quiet); + + let rd_val : xlenbits = + if (f_is_SNaN_D(rs1_val_D) | f_is_SNaN_D(rs2_val_D)) then zeros() + else if (f_is_QNaN_D(rs1_val_D) | f_is_QNaN_D(rs2_val_D)) then zeros() + else if rs1_lt_rs2 then EXTZ(0b1) + else zeros(); + + write_fflags(fflags); + X(rd) = rd_val; + RETIRE_SUCCESS +} + +function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FLE_D)) = { + let rs1_val_D = F(rs1); + let rs2_val_D = F(rs2); + + let is_quiet = false; + let (rs1_le_rs2, fflags) = fle_D (rs1_val_D, rs2_val_D, is_quiet); + + let rd_val : xlenbits = + if (f_is_SNaN_D(rs1_val_D) | f_is_SNaN_D(rs2_val_D)) then zeros() + else if (f_is_QNaN_D(rs1_val_D) | f_is_QNaN_D(rs2_val_D)) then zeros() + else if rs1_le_rs2 then EXTZ(0b1) + else zeros(); + + write_fflags(fflags); + X(rd) = rd_val; + RETIRE_SUCCESS +} + +/* AST -> Assembly notation ================================ */ + +mapping f_bin_type_mnemonic_D : f_bin_op_D <-> string = { + FSGNJ_D <-> "fsgnj.d", + FSGNJN_D <-> "fsgnjn.d", + FSGNJX_D <-> "fsgnjx.d", + FMIN_D <-> "fmin.d", + FMAX_D <-> "fmax.d", + FEQ_D <-> "feq.d", + FLT_D <-> "flt.d", + FLE_D <-> "fle.d" +} + +mapping clause assembly = F_BIN_TYPE_D(rs2, rs1, rd, FSGNJ_D) + <-> f_bin_type_mnemonic_D(FSGNJ_D) + ^ spc() ^ freg_name(rd) + ^ sep() ^ freg_name(rs1) + ^ sep() ^ freg_name(rs2) + +mapping clause assembly = F_BIN_TYPE_D(rs2, rs1, rd, FSGNJN_D) + <-> f_bin_type_mnemonic_D(FSGNJN_D) + ^ spc() ^ freg_name(rd) + ^ sep() ^ freg_name(rs1) + ^ sep() ^ freg_name(rs2) + +mapping clause assembly = F_BIN_TYPE_D(rs2, rs1, rd, FSGNJX_D) + <-> f_bin_type_mnemonic_D(FSGNJX_D) + ^ spc() ^ freg_name(rd) + ^ sep() ^ freg_name(rs1) + ^ sep() ^ freg_name(rs2) + +mapping clause assembly = F_BIN_TYPE_D(rs2, rs1, rd, FMIN_D) + <-> f_bin_type_mnemonic_D(FMIN_D) + ^ spc() ^ freg_name(rd) + ^ sep() ^ freg_name(rs1) + ^ sep() ^ freg_name(rs2) + +mapping clause assembly = F_BIN_TYPE_D(rs2, rs1, rd, FMAX_D) + <-> f_bin_type_mnemonic_D(FMAX_D) + ^ spc() ^ freg_name(rd) + ^ sep() ^ freg_name(rs1) + ^ sep() ^ freg_name(rs2) + +mapping clause assembly = F_BIN_TYPE_D(rs2, rs1, rd, FEQ_D) + <-> f_bin_type_mnemonic_D(FEQ_D) + ^ spc() ^ reg_name(rd) + ^ sep() ^ freg_name(rs1) + ^ sep() ^ freg_name(rs2) + +mapping clause assembly = F_BIN_TYPE_D(rs2, rs1, rd, FLT_D) + <-> f_bin_type_mnemonic_D(FLT_D) + ^ spc() ^ reg_name(rd) + ^ sep() ^ freg_name(rs1) + ^ sep() ^ freg_name(rs2) + +mapping clause assembly = F_BIN_TYPE_D(rs2, rs1, rd, FLE_D) + <-> f_bin_type_mnemonic_D(FLE_D) + ^ spc() ^ reg_name(rd) + ^ sep() ^ freg_name(rs1) + ^ sep() ^ freg_name(rs2) + +/* ****************************************************************** */ +/* Unary, no rounding mode */ + +union clause ast = F_UN_TYPE_D : (regidx, regidx, f_un_op_D) + +/* AST <-> Binary encoding ================================ */ + +mapping clause encdec = F_UN_TYPE_D(rs1, rd, FCLASS_D) if haveDExt() + <-> 0b111_0001 @ 0b00000 @ rs1 @ 0b001 @ rd @ 0b101_0011 if haveDExt() + +/* D instructions, RV64 only */ + +mapping clause encdec = F_UN_TYPE_D(rs1, rd, FMV_X_D) if is_RV64D() + <-> 0b111_0001 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011 if is_RV64D() + +mapping clause encdec = F_UN_TYPE_D(rs1, rd, FMV_D_X) if is_RV64D() + <-> 0b111_1001 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011 if is_RV64D() + +/* Execution semantics ================================ */ + +function clause execute (F_UN_TYPE_D(rs1, rd, FCLASS_D)) = { + let rs1_val_D = F(rs1); + + let rd_val_10b : bits (10) = + if f_is_neg_inf_D (rs1_val_D) then 0b_00_0000_0001 + else if f_is_neg_norm_D (rs1_val_D) then 0b_00_0000_0010 + else if f_is_neg_subnorm_D (rs1_val_D) then 0b_00_0000_0100 + else if f_is_neg_zero_D (rs1_val_D) then 0b_00_0000_1000 + else if f_is_pos_zero_D (rs1_val_D) then 0b_00_0001_0000 + else if f_is_pos_subnorm_D (rs1_val_D) then 0b_00_0010_0000 + else if f_is_pos_norm_D (rs1_val_D) then 0b_00_0100_0000 + else if f_is_pos_inf_D (rs1_val_D) then 0b_00_1000_0000 + else if f_is_SNaN_D (rs1_val_D) then 0b_01_0000_0000 + else if f_is_QNaN_D (rs1_val_D) then 0b_10_0000_0000 + else zeros(); + + X(rd) = EXTZ (rd_val_10b); + RETIRE_SUCCESS +} + +function clause execute (F_UN_TYPE_D(rs1, rd, FMV_X_D)) = { + let rs1_val_D = F(rs1); + let rd_val_X = rs1_val_D; + X(rd) = rd_val_X; + RETIRE_SUCCESS +} + +function clause execute (F_UN_TYPE_D(rs1, rd, FMV_D_X)) = { + let rs1_val_X = X(rs1); + let rd_val_D = rs1_val_X; + F(rd) = rd_val_D; + RETIRE_SUCCESS +} + +/* AST -> Assembly notation ================================ */ + +mapping f_un_type_mnemonic_D : f_un_op_D <-> string = { + FMV_X_D <-> "fmv.x.d", + FCLASS_D <-> "fclass.d", + FMV_D_X <-> "fmv.d.x" +} + +mapping clause assembly = F_UN_TYPE_D(rs1, rd, FMV_X_D) + <-> f_un_type_mnemonic_D(FMV_X_D) + ^ spc() ^ reg_name(rd) + ^ sep() ^ freg_name(rs1) + +mapping clause assembly = F_UN_TYPE_D(rs1, rd, FMV_D_X) + <-> f_un_type_mnemonic_D(FMV_D_X) + ^ spc() ^ freg_name(rd) + ^ sep() ^ reg_name(rs1) + +mapping clause assembly = F_UN_TYPE_D(rs1, rd, FCLASS_D) + <-> f_un_type_mnemonic_D(FCLASS_D) + ^ spc() ^ reg_name(rd) + ^ sep() ^ freg_name(rs1) + +/* ****************************************************************** */ diff --git a/model/riscv_insts_end.sail b/model/riscv_insts_end.sail index f6223dd..6c16417 100644 --- a/model/riscv_insts_end.sail +++ b/model/riscv_insts_end.sail @@ -34,7 +34,7 @@ function print_insn insn = assembly(insn) overload to_str = {print_insn} -val decode : bits(32) -> ast effect pure +val decode : bits(32) -> ast effect {rreg} function decode bv = encdec(bv) val decodeCompressed : bits(16) -> ast effect pure diff --git a/model/riscv_insts_fext.sail b/model/riscv_insts_fext.sail new file mode 100644 index 0000000..4b9e69e --- /dev/null +++ b/model/riscv_insts_fext.sail @@ -0,0 +1,1096 @@ +/* **************************************************************** */ +/* This file specifies the instructions in the F extension */ +/* (single precision floating point). */ + +/* RISC-V follows IEEE 754-2008 floating point arithmetic standard. */ + +/* Original version written by Rishiyur S. Nikhil, Sept-Oct 2019 */ + +/* **************************************************************** */ +/* IMPORTANT! */ +/* The files 'riscv_insts_fext.sail' and 'riscv_insts_dext.sail' */ +/* define the F and D extensions, respectively. */ +/* The texts follow each other very closely; please try to maintain */ +/* this correspondence as the files are maintained for bug-fixes, */ +/* improvements, and version updates. */ + +/* **************************************************************** */ + +mapping encdec_rounding_mode : rounding_mode <-> bits(3) = { + RM_RNE <-> 0b000, + RM_RTZ <-> 0b001, + RM_RDN <-> 0b010, + RM_RUP <-> 0b011, + RM_RMM <-> 0b100, + RM_DYN <-> 0b111 +} + +mapping frm_mnemonic : rounding_mode <-> string = { + RM_RNE <-> "rne", + RM_RTZ <-> "rtz", + RM_RDN <-> "rdn", + RM_RUP <-> "rup", + RM_RMM <-> "rmm", + RM_DYN <-> "dyn" +} + +val select_instr_or_fcsr_rm : rounding_mode -> rounding_mode effect {rreg} +function select_instr_or_fcsr_rm instr_rm = + if (instr_rm == RM_DYN) + then encdec_rounding_mode (fcsr.FRM()) + else instr_rm + +/* **************************************************************** */ +/* Floating point accrued exception flags */ + +function nxFlag() -> bits(5) = 0b_00001 +function ufFlag() -> bits(5) = 0b_00010 +function ofFlag() -> bits(5) = 0b_00100 +function dzFlag() -> bits(5) = 0b_01000 +function nvFlag() -> bits(5) = 0b_10000 + +/* **************************************************************** */ +/* S and D value structure (sign, exponent, mantissa) */ + +/* TODO: this should be a 'mapping' */ +val fsplit_S : bits(32) -> (bits(1), bits(8), bits(23)) +function fsplit_S x32 = (x32[31..31], x32[30..23], x32[22..0]) + +val fmake_S : (bits(1), bits(8), bits(23)) -> bits(32) +function fmake_S (sign, exp, mant) = sign @ exp @ mant + +/* ---- Canonical NaNs */ + +function canonical_NaN_S() -> bits(32) = 0x_7fc0_0000 + +/* ---- Structure tests */ + +val f_is_neg_inf_S : bits(32) -> bool +function f_is_neg_inf_S x32 = { + let (sign, exp, mant) = fsplit_S (x32); + ( (sign == 0b1) + & (exp == ones()) + & (mant == zeros())) +} + +val f_is_neg_norm_S : bits(32) -> bool +function f_is_neg_norm_S x32 = { + let (sign, exp, mant) = fsplit_S (x32); + ( (sign == 0b1) + & (exp != zeros()) + & (exp != ones())) +} + +val f_is_neg_subnorm_S : bits(32) -> bool +function f_is_neg_subnorm_S x32 = { + let (sign, exp, mant) = fsplit_S (x32); + ( (sign == 0b1) + & (exp == zeros()) + & (mant != zeros())) +} + +val f_is_neg_zero_S : bits(32) -> bool +function f_is_neg_zero_S x32 = { + let (sign, exp, mant) = fsplit_S (x32); + ( (sign == ones()) + & (exp == zeros()) + & (mant == zeros())) +} + +val f_is_pos_zero_S : bits(32) -> bool +function f_is_pos_zero_S x32 = { + let (sign, exp, mant) = fsplit_S (x32); + ( (sign == zeros()) + & (exp == zeros()) + & (mant == zeros())) +} + +val f_is_pos_subnorm_S : bits(32) -> bool +function f_is_pos_subnorm_S x32 = { + let (sign, exp, mant) = fsplit_S (x32); + ( (sign == zeros()) + & (exp == zeros()) + & (mant != zeros())) +} + +val f_is_pos_norm_S : bits(32) -> bool +function f_is_pos_norm_S x32 = { + let (sign, exp, mant) = fsplit_S (x32); + ( (sign == zeros()) + & (exp != zeros()) + & (exp != ones())) +} + +val f_is_pos_inf_S : bits(32) -> bool +function f_is_pos_inf_S x32 = { + let (sign, exp, mant) = fsplit_S (x32); + ( (sign == zeros()) + & (exp == ones()) + & (mant == zeros())) +} + +val f_is_SNaN_S : bits(32) -> bool +function f_is_SNaN_S x32 = { + let (sign, exp, mant) = fsplit_S (x32); + ( (exp == ones()) + & (mant [22] == bitzero) + & (mant != zeros())) +} + +val f_is_QNaN_S : bits(32) -> bool +function f_is_QNaN_S x32 = { + let (sign, exp, mant) = fsplit_S (x32); + ( (exp == ones()) + & (mant [22] == bitone)) +} + +/* **************************************************************** */ +/* Help functions used in the semantic functions */ + +val negate_S : bits(32) -> bits(32) +function negate_S (x32) = { + let (sign, exp, mant) = fsplit_S (x32); + let new_sign = if (sign == 0b0) then 0b1 else 0b0; + fmake_S (new_sign, exp, mant) +} + +val feq_quiet_S : (bits(32), bits (32)) -> (bool, bits(5)) +function feq_quiet_S (v1, v2) = { + let (s1, e1, m1) = fsplit_S (v1); + let (s2, e2, m2) = fsplit_S (v2); + + let v1Is0 = f_is_neg_zero_S(v1) | f_is_pos_zero_S(v1); + let v2Is0 = f_is_neg_zero_S(v2) | f_is_pos_zero_S(v2); + + let result = ((v1 == v2) | (v1Is0 & v2Is0)); + + let fflags = if (f_is_SNaN_S(v1) | f_is_SNaN_S(v2)) then + nvFlag() + else + zeros(); + + (result, fflags) +} + +val flt_S : (bits(32), bits (32), bool) -> (bool, bits(5)) +function flt_S (v1, v2, is_quiet) = { + let (s1, e1, m1) = fsplit_S (v1); + let (s2, e2, m2) = fsplit_S (v2); + + let v1IsNaN = f_is_QNaN_S(v1) | f_is_SNaN_S(v1); + let v2IsNaN = f_is_QNaN_S(v2) | f_is_SNaN_S(v2); + + let result : bool = + if (s1 == 0b0) & (s2 == 0b0) then + if (e1 == e2) then + unsigned (m1) < unsigned (m2) + else + unsigned (e1) < unsigned (e2) + else if (s1 == 0b0) & (s2 == 0b1) then + false + else if (s1 == 0b1) & (s2 == 0b0) then + true + else + if (e1 == e2) then + unsigned (m1) > unsigned (m2) + else + unsigned (e1) > unsigned (e2); + + let fflags = if is_quiet then + if (f_is_SNaN_S(v1) | f_is_SNaN_S(v2)) then + nvFlag() + else + zeros() + else + if (v1IsNaN | v2IsNaN) then + nvFlag() + else + zeros(); + + (result, fflags) +} + +val fle_S : (bits(32), bits (32), bool) -> (bool, bits(5)) +function fle_S (v1, v2, is_quiet) = { + let (s1, e1, m1) = fsplit_S (v1); + let (s2, e2, m2) = fsplit_S (v2); + + let v1IsNaN = f_is_QNaN_S(v1) | f_is_SNaN_S(v1); + let v2IsNaN = f_is_QNaN_S(v2) | f_is_SNaN_S(v2); + + let v1Is0 = f_is_neg_zero_S(v1) | f_is_pos_zero_S(v1); + let v2Is0 = f_is_neg_zero_S(v2) | f_is_pos_zero_S(v2); + + let result : bool = + if (s1 == 0b0) & (s2 == 0b0) then + if (e1 == e2) then + unsigned (m1) <= unsigned (m2) + else + unsigned (e1) < unsigned (e2) + else if (s1 == 0b0) & (s2 == 0b1) then + (v1Is0 & v2Is0) /* Equal in this case (+0=-0) */ + else if (s1 == 0b1) & (s2 == 0b0) then + true + else + if (e1 == e2) then + unsigned (m1) >= unsigned (m2) + else + unsigned (e1) > unsigned (e2); + + let fflags = if is_quiet then + if (f_is_SNaN_S(v1) | f_is_SNaN_S(v2)) then + nvFlag() + else + zeros() + else + if (v1IsNaN | v2IsNaN) then + nvFlag() + else + zeros(); + + (result, fflags) +} + +/* **************************************************************** */ +/* NaN boxing/unboxing. */ +/* When 32-bit floats (single-precision) are stored in 64-bit regs */ +/* they must be 'NaN boxed' (upper 32b all ones). */ +/* When 32-bit floats (single-precision) are read from 64-bit regs */ +/* they must be 'NaN unboxed'. */ + +val nan_box : bits(32) -> flenbits +function nan_box val_32b = + if (sizeof(flen) == 32) + then val_32b + else 0x_FFFF_FFFF @ val_32b + +val nan_unbox : flenbits -> bits(32) +function nan_unbox regval = + if (sizeof(flen) == 32) + then regval + else if regval [63..32] == 0x_FFFF_FFFF + then regval [31..0] + else canonical_NaN_S() + +/* **************************************************************** */ +/* Help-functions for 'encdec()' to restrict to certain */ +/* combinations of {F,D} x {RV32,RV64} */ + +function is_RV32F_or_RV64F () -> bool = (haveFExt() & (sizeof(xlen) == 32 | sizeof(xlen) == 64)) +function is_RV64F () -> bool = (haveFExt() & sizeof(xlen) == 64) + +function is_RV32D_or_RV64D () -> bool = (haveDExt() & (sizeof(xlen) == 32 | sizeof(xlen) == 64)) +function is_RV64D () -> bool = (haveDExt() & sizeof(xlen) == 64) + +/* ****************************************************************** */ +/* Floating-point loads */ + +/* AST */ +/* FLW and FLD; W/D is encoded in 'word_width' */ + +union clause ast = LOAD_FP : (bits(12), regidx, regidx, word_width) + +/* AST <-> Binary encoding ================================ */ + +mapping clause encdec = LOAD_FP(imm, rs1, rd, WORD) if is_RV32F_or_RV64F() + <-> imm @ rs1 @ 0b010 @ rd @ 0b000_0111 if is_RV32F_or_RV64F() + +mapping clause encdec = LOAD_FP(imm, rs1, rd, DOUBLE) if is_RV32D_or_RV64D() + <-> imm @ rs1 @ 0b011 @ rd @ 0b000_0111 if is_RV32D_or_RV64D() + +/* Execution semantics ================================ */ + +val process_fload64 : (regidx, xlenbits, MemoryOpResult(bits(64))) + -> Retired effect {escape, rreg, wreg} +function process_fload64(rd, addr, value) = + if sizeof(flen) == 64 + then match value { + MemValue(result) => { F(rd) = result; RETIRE_SUCCESS }, + MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL } + } + else { + /* should not get here */ + RETIRE_FAIL + } + +val process_fload32 : (regidx, xlenbits, MemoryOpResult(bits(32))) + -> Retired effect {escape, rreg, wreg} +function process_fload32(rd, addr, value) = + match value { + MemValue(result) => { F(rd) = nan_box(result); RETIRE_SUCCESS }, + MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL } + } + + +function clause execute(LOAD_FP(imm, rs1, rd, width)) = { + let offset : xlenbits = EXTS(imm); + /* Get the address, X(rs1) + offset. + Some extensions perform additional checks on address validity. */ + match ext_data_get_addr(rs1, offset, Read(Data), width) { + Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, + Ext_DataAddr_OK(vaddr) => + if check_misaligned(vaddr, width) + then { handle_mem_exception(vaddr, E_Load_Addr_Align()); RETIRE_FAIL } + else match translateAddr(vaddr, Read(Data)) { + TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + TR_Address(addr, _) => { + let (aq, rl, res) = (false, false, false); + match (width, sizeof(xlen)) { + (BYTE, _) => { handle_illegal(); RETIRE_FAIL }, + (HALF, _) => { handle_illegal(); RETIRE_FAIL }, + (WORD, _) => + process_fload32(rd, vaddr, mem_read(Read(Data), addr, 4, aq, rl, res)), + (DOUBLE, 64) => + process_fload64(rd, vaddr, mem_read(Read(Data), addr, 8, aq, rl, res)) + } + } + } + } +} + +/* AST -> Assembly notation ================================ */ + +mapping clause assembly = LOAD_FP(imm, rs1, rd, width) + <-> "fl" ^ size_mnemonic(width) + ^ spc() ^ freg_name(rd) + ^ sep() ^ hex_bits_12(imm) + ^ opt_spc() ^ "(" ^ opt_spc() ^ reg_name(rs1) ^ opt_spc() ^ ")" + +/* ****************************************************************** */ +/* Floating-point stores */ + +/* AST */ +/* FLW and FLD; W/D is encoded in 'width' */ + +union clause ast = STORE_FP : (bits(12), regidx, regidx, word_width) + +/* AST <-> Binary encoding ================================ */ + +mapping clause encdec = STORE_FP(imm7 @ imm5, rs2, rs1, WORD) if is_RV32F_or_RV64F() + <-> imm7 : bits(7) @ rs2 @ rs1 @ 0b010 @ imm5 : bits(5) @ 0b010_0111 if is_RV32F_or_RV64F() + +mapping clause encdec = STORE_FP(imm7 @ imm5, rs2, rs1, DOUBLE) if is_RV32D_or_RV64D() + <-> imm7 : bits(7) @ rs2 @ rs1 @ 0b011 @ imm5 : bits(5) @ 0b010_0111 if is_RV32D_or_RV64D() + +/* Execution semantics ================================ */ + +val process_fstore : (xlenbits, MemoryOpResult(bool)) -> Retired effect {escape, rreg, wreg} +function process_fstore(vaddr, value) = + match value { + MemValue(true) => { RETIRE_SUCCESS }, + MemValue(false) => { internal_error("store got false from mem_write_value") }, + MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL } + } + +function clause execute (STORE_FP(imm, rs2, rs1, width)) = { + let offset : xlenbits = EXTS(imm); + let (aq, rl, con) = (false, false, false); + /* Get the address, X(rs1) + offset. + Some extensions perform additional checks on address validity. */ + match ext_data_get_addr(rs1, offset, Write(Data), width) { + Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, + Ext_DataAddr_OK(vaddr) => + if check_misaligned(vaddr, width) + then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); RETIRE_FAIL } + else match translateAddr(vaddr, Write(Data)) { + TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + TR_Address(addr, _) => { + let eares : MemoryOpResult(unit) = match width { + BYTE => MemValue () /* bogus placeholder for illegal size */, + HALF => MemValue () /* bogus placeholder for illegal size */, + WORD => mem_write_ea(addr, 4, aq, rl, false), + DOUBLE => mem_write_ea(addr, 8, aq, rl, false) + }; + match (eares) { + MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL }, + MemValue(_) => { + let rs2_val = F(rs2); + match (width, sizeof(xlen)) { + (BYTE, _) => { handle_illegal(); RETIRE_FAIL }, + (HALF, _) => { handle_illegal(); RETIRE_FAIL }, + (WORD, _) => process_fstore (vaddr, mem_write_value(addr, 4, rs2_val[31..0], aq, rl, con)), + (DOUBLE, 64) => process_fstore (vaddr, mem_write_value(addr, 8, rs2_val, aq, rl, con)) + }; + } + } + } + } + } +} + +/* AST -> Assembly notation ================================ */ + +mapping clause assembly = STORE_FP(imm, rs2, rs1, width) + <-> "fs" ^ size_mnemonic(width) + ^ spc() ^ freg_name(rs2) + ^ sep() ^ hex_bits_12(imm) + ^ opt_spc() ^ "(" ^ opt_spc() ^ reg_name(rs1) ^ opt_spc() ^ ")" + +/* ****************************************************************** */ +/* Fused multiply-add */ + +/* AST */ + +union clause ast = F_MADD_TYPE_S : (regidx, regidx, regidx, rounding_mode, regidx, f_madd_op_S) + +/* AST <-> Binary encoding ================================ */ + +mapping clause encdec = + F_MADD_TYPE_S(rs3, rs2, rs1, rm, rd, FMADD_S) if is_RV32F_or_RV64F() +<-> rs3 @ 0b00 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_0011 if is_RV32F_or_RV64F() + +mapping clause encdec = + F_MADD_TYPE_S(rs3, rs2, rs1, rm, rd, FMSUB_S) if is_RV32F_or_RV64F() +<-> rs3 @ 0b00 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_0111 if is_RV32F_or_RV64F() + +mapping clause encdec = + F_MADD_TYPE_S(rs3, rs2, rs1, rm, rd, FNMSUB_S) if is_RV32F_or_RV64F() +<-> rs3 @ 0b00 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_1011 if is_RV32F_or_RV64F() + +mapping clause encdec = + F_MADD_TYPE_S(rs3, rs2, rs1, rm, rd, FNMADD_S) if is_RV32F_or_RV64F() +<-> rs3 @ 0b00 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_1111 if is_RV32F_or_RV64F() + +/* Execution semantics ================================ */ + +function clause execute (F_MADD_TYPE_S(rs3, rs2, rs1, rm, rd, op)) = { + let rs1_val_32b = nan_unbox (F(rs1)); + let rs2_val_32b = nan_unbox (F(rs2)); + let rs3_val_32b = nan_unbox (F(rs3)); + let rm_3b = encdec_rounding_mode (select_instr_or_fcsr_rm (rm)); + let (fflags, rd_val_32b) : (bits(5), bits(32)) = + match op { + FMADD_S => riscv_f32MulAdd (rm_3b, rs1_val_32b, rs2_val_32b, rs3_val_32b), + FMSUB_S => riscv_f32MulAdd (rm_3b, rs1_val_32b, rs2_val_32b, negate_S (rs3_val_32b)), + FNMSUB_S => riscv_f32MulAdd (rm_3b, negate_S (rs1_val_32b), rs2_val_32b, rs3_val_32b), + FNMADD_S => riscv_f32MulAdd (rm_3b, negate_S (rs1_val_32b), rs2_val_32b, negate_S (rs3_val_32b)) + }; + write_fflags(fflags); + F(rd) = nan_box (rd_val_32b); + RETIRE_SUCCESS +} + +/* AST -> Assembly notation ================================ */ + +mapping f_madd_type_mnemonic_S : f_madd_op_S <-> string = { + FMADD_S <-> "fmadd.s", + FMSUB_S <-> "fmsub.s", + FNMSUB_S <-> "fnmsub.s", + FNMADD_S <-> "fnmadd.s" +} + +mapping clause assembly = F_MADD_TYPE_S(rs3, rs2, rs1, rm, rd, op) + <-> f_madd_type_mnemonic_S(op) + ^ spc() ^ freg_name(rd) + ^ sep() ^ freg_name(rs1) + ^ sep() ^ freg_name(rs2) + ^ sep() ^ freg_name(rs3) + ^ sep() ^ frm_mnemonic(rm) + +/* ****************************************************************** */ +/* Binary ops with rounding mode */ + +/* AST */ + +union clause ast = F_BIN_RM_TYPE_S : (regidx, regidx, rounding_mode, regidx, f_bin_rm_op_S) + +/* AST <-> Binary encoding ================================ */ + +mapping clause encdec = + F_BIN_RM_TYPE_S(rs2, rs1, rm, rd, FADD_S) if is_RV32F_or_RV64F() +<-> 0b000_0000 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32F_or_RV64F() + +mapping clause encdec = + F_BIN_RM_TYPE_S(rs2, rs1, rm, rd, FSUB_S) if is_RV32F_or_RV64F() +<-> 0b000_0100 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32F_or_RV64F() + +mapping clause encdec = + F_BIN_RM_TYPE_S(rs2, rs1, rm, rd, FMUL_S) if is_RV32F_or_RV64F() +<-> 0b000_1000 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32F_or_RV64F() + +mapping clause encdec = + F_BIN_RM_TYPE_S(rs2, rs1, rm, rd, FDIV_S) if is_RV32F_or_RV64F() +<-> 0b000_1100 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32F_or_RV64F() + +/* Execution semantics ================================ */ + +function clause execute (F_BIN_RM_TYPE_S(rs2, rs1, rm, rd, op)) = { + let rs1_val_32b = nan_unbox (F(rs1)); + let rs2_val_32b = nan_unbox (F(rs2)); + let rm_3b = encdec_rounding_mode (select_instr_or_fcsr_rm (rm)); + let (fflags, rd_val_32b) : (bits(5), bits(32)) = match op { + FADD_S => riscv_f32Add (rm_3b, rs1_val_32b, rs2_val_32b), + FSUB_S => riscv_f32Sub (rm_3b, rs1_val_32b, rs2_val_32b), + FMUL_S => riscv_f32Mul (rm_3b, rs1_val_32b, rs2_val_32b), + FDIV_S => riscv_f32Div (rm_3b, rs1_val_32b, rs2_val_32b) + }; + write_fflags(fflags); + F(rd) = nan_box (rd_val_32b); + RETIRE_SUCCESS +} + +/* AST -> Assembly notation ================================ */ + +mapping f_bin_rm_type_mnemonic_S : f_bin_rm_op_S <-> string = { + FADD_S <-> "fadd.s", + FSUB_S <-> "fsub.s", + FMUL_S <-> "fmul.s", + FDIV_S <-> "fdiv.s" +} + +mapping clause assembly = F_BIN_RM_TYPE_S(rs2, rs1, rm, rd, op) + <-> f_bin_rm_type_mnemonic_S(op) + ^ spc() ^ freg_name(rd) + ^ sep() ^ freg_name(rs1) + ^ sep() ^ freg_name(rs2) + ^ sep() ^ frm_mnemonic(rm) + +/* ****************************************************************** */ +/* Unary with rounding mode */ + +/* AST */ + +union clause ast = F_UN_RM_TYPE_S : (regidx, rounding_mode, regidx, f_un_rm_op_S) + +/* AST <-> Binary encoding ================================ */ + +mapping clause encdec = + F_UN_RM_TYPE_S(rs1, rm, rd, FSQRT_S) if is_RV32F_or_RV64F() +<-> 0b010_1100 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32F_or_RV64F() + +mapping clause encdec = + F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_W_S) if is_RV32F_or_RV64F() +<-> 0b110_0000 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32F_or_RV64F() + +mapping clause encdec = + F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_WU_S) if is_RV32F_or_RV64F() +<-> 0b110_0000 @ 0b00001 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32F_or_RV64F() + +mapping clause encdec = + F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_W) if is_RV32F_or_RV64F() +<-> 0b110_1000 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32F_or_RV64F() + +mapping clause encdec = + F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_WU) if is_RV32F_or_RV64F() +<-> 0b110_1000 @ 0b00001 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32F_or_RV64F() + +/* F instructions, RV64 only */ + +mapping clause encdec = + F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_L_S) if is_RV64F() +<-> 0b110_0000 @ 0b00010 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV64F() + +mapping clause encdec = + F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_LU_S) if is_RV64F() +<-> 0b110_0000 @ 0b00011 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV64F() + +mapping clause encdec = + F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_L) if is_RV64F() +<-> 0b110_1000 @ 0b00010 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV64F() + +mapping clause encdec = + F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_LU) if is_RV64F() +<-> 0b110_1000 @ 0b00011 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV64F() + +/* Execution semantics ================================ */ + +function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FSQRT_S)) = { + let rs1_val_S = nan_unbox (F(rs1)); + let rm_3b = encdec_rounding_mode (select_instr_or_fcsr_rm (rm)); + + let (fflags, rd_val_S) = riscv_f32Sqrt (rm_3b, rs1_val_S); + + write_fflags(fflags); + F(rd) = nan_box (rd_val_S); + RETIRE_SUCCESS +} + +function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_W_S)) = { + let rs1_val_S = nan_unbox (F(rs1)); + let rm_3b = encdec_rounding_mode (select_instr_or_fcsr_rm (rm)); + + let (fflags, rd_val_W) = riscv_f32ToI32 (rm_3b, rs1_val_S); + + write_fflags(fflags); + X(rd) = EXTS (rd_val_W); + RETIRE_SUCCESS +} + +function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_WU_S)) = { + let rs1_val_S = nan_unbox (F(rs1)); + let rm_3b = encdec_rounding_mode (select_instr_or_fcsr_rm (rm)); + + let (fflags, rd_val_WU) = riscv_f32ToUi32 (rm_3b, rs1_val_S); + + write_fflags(fflags); + X(rd) = EXTS (rd_val_WU); + RETIRE_SUCCESS +} + +function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_W)) = { + let rs1_val_W = X(rs1) [31..0]; + let rm_3b = encdec_rounding_mode (select_instr_or_fcsr_rm (rm)); + + let (fflags, rd_val_S) = riscv_i32ToF32 (rm_3b, rs1_val_W); + + write_fflags(fflags); + F(rd) = nan_box (rd_val_S); + RETIRE_SUCCESS +} + +function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_WU)) = { + let rs1_val_WU = X(rs1) [31..0]; + let rm_3b = encdec_rounding_mode (select_instr_or_fcsr_rm (rm)); + + let (fflags, rd_val_S) = riscv_ui32ToF32 (rm_3b, rs1_val_WU); + + write_fflags(fflags); + F(rd) = nan_box (rd_val_S); + RETIRE_SUCCESS +} + +function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_L_S)) = { + if sizeof(flen) == 64 + then { + let rs1_val_S = nan_unbox (F(rs1)); + let rm_3b = encdec_rounding_mode (select_instr_or_fcsr_rm (rm)); + + let (fflags, rd_val_L) = riscv_f32ToI64 (rm_3b, rs1_val_S); + + write_fflags(fflags); + X(rd) = rd_val_L; + RETIRE_SUCCESS + } else { + /* this would not decode on RV32 */ + RETIRE_FAIL + } +} + +function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_LU_S)) = { + if sizeof(flen) == 64 + then { + let rs1_val_S = nan_unbox (F(rs1)); + let rm_3b = encdec_rounding_mode (select_instr_or_fcsr_rm (rm)); + + let (fflags, rd_val_LU) = riscv_f32ToUi64 (rm_3b, rs1_val_S); + + write_fflags(fflags); + X(rd) = rd_val_LU; + RETIRE_SUCCESS + } else { + /* this would not decode on RV32 */ + RETIRE_FAIL + } +} + +function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_L)) = { + if sizeof(flen) == 64 + then { + let rs1_val_L = X(rs1); + let rm_3b = encdec_rounding_mode (select_instr_or_fcsr_rm (rm)); + + let (fflags, rd_val_S) = riscv_i64ToF32 (rm_3b, rs1_val_L); + + write_fflags(fflags); + F(rd) = nan_box (rd_val_S); + RETIRE_SUCCESS + } else { + /* this would not decode on RV32 */ + RETIRE_FAIL + } +} + +function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_LU)) = { + if sizeof(flen) == 64 + then { + let rs1_val_LU = X(rs1); + let rm_3b = encdec_rounding_mode (select_instr_or_fcsr_rm (rm)); + + let (fflags, rd_val_S) = riscv_ui64ToF32 (rm_3b, rs1_val_LU); + + write_fflags(fflags); + F(rd) = nan_box (rd_val_S); + RETIRE_SUCCESS + } else { + /* this would not decode on RV32 */ + RETIRE_FAIL + } +} + +/* AST -> Assembly notation ================================ */ + +mapping f_un_rm_type_mnemonic_S : f_un_rm_op_S <-> string = { + FSQRT_S <-> "fsqrt.s", + FCVT_W_S <-> "fcvt.w.s", + FCVT_WU_S <-> "fcvt.wu.s", + FCVT_S_W <-> "fcvt.s.w", + FCVT_S_WU <-> "fcvt.s.wu", + + FCVT_L_S <-> "fcvt.l.s", + FCVT_LU_S <-> "fcvt.lu.s", + FCVT_S_L <-> "fcvt.s.l", + FCVT_S_LU <-> "fcvt.s.lu" +} + +mapping clause assembly = F_UN_RM_TYPE_S(rs1, rm, rd, FSQRT_S) + <-> f_un_rm_type_mnemonic_S(FSQRT_S) + ^ spc() ^ freg_name(rd) + ^ sep() ^ freg_name(rs1) + ^ sep() ^ frm_mnemonic(rm) + +mapping clause assembly = F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_W_S) + <-> f_un_rm_type_mnemonic_S(FCVT_W_S) + ^ spc() ^ reg_name(rd) + ^ sep() ^ freg_name(rs1) + ^ sep() ^ frm_mnemonic(rm) + +mapping clause assembly = F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_WU_S) + <-> f_un_rm_type_mnemonic_S(FCVT_WU_S) + ^ spc() ^ reg_name(rd) + ^ sep() ^ freg_name(rs1) + ^ sep() ^ frm_mnemonic(rm) + +mapping clause assembly = F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_W) + <-> f_un_rm_type_mnemonic_S(FCVT_S_W) + ^ spc() ^ freg_name(rd) + ^ sep() ^ reg_name(rs1) + ^ sep() ^ frm_mnemonic(rm) + +mapping clause assembly = F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_WU) + <-> f_un_rm_type_mnemonic_S(FCVT_S_WU) + ^ spc() ^ freg_name(rd) + ^ sep() ^ reg_name(rs1) + ^ sep() ^ frm_mnemonic(rm) + +mapping clause assembly = F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_L_S) + <-> f_un_rm_type_mnemonic_S(FCVT_L_S) + ^ spc() ^ reg_name(rd) + ^ sep() ^ freg_name(rs1) + ^ sep() ^ frm_mnemonic(rm) + +mapping clause assembly = F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_LU_S) + <-> f_un_rm_type_mnemonic_S(FCVT_LU_S) + ^ spc() ^ reg_name(rd) + ^ sep() ^ freg_name(rs1) + ^ sep() ^ frm_mnemonic(rm) + +mapping clause assembly = F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_L) + <-> f_un_rm_type_mnemonic_S(FCVT_S_L) + ^ spc() ^ freg_name(rd) + ^ sep() ^ reg_name(rs1) + ^ sep() ^ frm_mnemonic(rm) + +mapping clause assembly = F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_LU) + <-> f_un_rm_type_mnemonic_S(FCVT_S_LU) + ^ spc() ^ freg_name(rd) + ^ sep() ^ reg_name(rs1) + ^ sep() ^ frm_mnemonic(rm) + + +/* ****************************************************************** */ +/* Binary, no rounding mode */ + +/* AST */ + +union clause ast = F_BIN_TYPE_S : (regidx, regidx, regidx, f_bin_op_S) + +/* AST <-> Binary encoding ================================ */ + +mapping clause encdec = F_BIN_TYPE_S(rs2, rs1, rd, FSGNJ_S) if is_RV32F_or_RV64F() + <-> 0b001_0000 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011 if is_RV32F_or_RV64F() + +mapping clause encdec = F_BIN_TYPE_S(rs2, rs1, rd, FSGNJN_S) if is_RV32F_or_RV64F() + <-> 0b001_0000 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011 if is_RV32F_or_RV64F() + +mapping clause encdec = F_BIN_TYPE_S(rs2, rs1, rd, FSGNJX_S) if is_RV32F_or_RV64F() + <-> 0b001_0000 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011 if is_RV32F_or_RV64F() + +mapping clause encdec = F_BIN_TYPE_S(rs2, rs1, rd, FMIN_S) if is_RV32F_or_RV64F() + <-> 0b001_0100 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011 if is_RV32F_or_RV64F() + +mapping clause encdec = F_BIN_TYPE_S(rs2, rs1, rd, FMAX_S) if is_RV32F_or_RV64F() + <-> 0b001_0100 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011 if is_RV32F_or_RV64F() + +mapping clause encdec = F_BIN_TYPE_S(rs2, rs1, rd, FEQ_S) if is_RV32F_or_RV64F() + <-> 0b101_0000 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011 if is_RV32F_or_RV64F() + +mapping clause encdec = F_BIN_TYPE_S(rs2, rs1, rd, FLT_S) if is_RV32F_or_RV64F() + <-> 0b101_0000 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011 if is_RV32F_or_RV64F() + +mapping clause encdec = F_BIN_TYPE_S(rs2, rs1, rd, FLE_S) if is_RV32F_or_RV64F() + <-> 0b101_0000 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011 if is_RV32F_or_RV64F() + +/* Execution semantics ================================ */ + +function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FSGNJ_S)) = { + let rs1_val_S = nan_unbox (F(rs1)); + let rs2_val_S = nan_unbox (F(rs2)); + let (s1, e1, m1) = fsplit_S (rs1_val_S); + let (s2, e2, m2) = fsplit_S (rs2_val_S); + let rd_val_S = fmake_S (s2, e1, m1); + let fflags = 0b_00000; + write_fflags(fflags); + F(rd) = nan_box (rd_val_S); + RETIRE_SUCCESS +} + +function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FSGNJN_S)) = { + let rs1_val_S = nan_unbox (F(rs1)); + let rs2_val_S = nan_unbox (F(rs2)); + let (s1, e1, m1) = fsplit_S (rs1_val_S); + let (s2, e2, m2) = fsplit_S (rs2_val_S); + let rd_val_S = fmake_S (0b1 ^ s2, e1, m1); + let fflags = 0b_00000; + write_fflags(fflags); + F(rd) = nan_box (rd_val_S); + RETIRE_SUCCESS +} + +function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FSGNJX_S)) = { + let rs1_val_S = nan_unbox (F(rs1)); + let rs2_val_S = nan_unbox (F(rs2)); + let (s1, e1, m1) = fsplit_S (rs1_val_S); + let (s2, e2, m2) = fsplit_S (rs2_val_S); + let rd_val_S = fmake_S (s1 ^ s2, e1, m1); + let fflags = 0b_00000; + write_fflags(fflags); + F(rd) = nan_box (rd_val_S); + RETIRE_SUCCESS +} + +function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FMIN_S)) = { + let rs1_val_S = nan_unbox (F(rs1)); + let rs2_val_S = nan_unbox (F(rs2)); + + let is_quiet = true; + let (rs1_lt_rs2, fflags) = fle_S (rs1_val_S, rs2_val_S, is_quiet); + + let rd_val_S = if (f_is_SNaN_S(rs1_val_S) & f_is_SNaN_S(rs2_val_S)) then canonical_NaN_S() + else if f_is_SNaN_S(rs1_val_S) then rs2_val_S + else if f_is_SNaN_S(rs2_val_S) then rs1_val_S + else if (f_is_QNaN_S(rs1_val_S) & f_is_QNaN_S(rs2_val_S)) then canonical_NaN_S() + else if f_is_QNaN_S(rs1_val_S) then rs2_val_S + else if f_is_QNaN_S(rs2_val_S) then rs1_val_S + else if (f_is_neg_zero_S(rs1_val_S) & f_is_pos_zero_S(rs2_val_S)) then rs1_val_S + else if (f_is_neg_zero_S(rs2_val_S) & f_is_pos_zero_S(rs1_val_S)) then rs2_val_S + else if rs1_lt_rs2 then rs1_val_S + else /* (not rs1_lt_rs2) */ rs2_val_S; + + write_fflags(fflags); + F(rd) = nan_box (rd_val_S); + RETIRE_SUCCESS +} + +function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FMAX_S)) = { + let rs1_val_S = nan_unbox (F(rs1)); + let rs2_val_S = nan_unbox (F(rs2)); + + let is_quiet = true; + let (rs2_lt_rs1, fflags) = fle_S (rs2_val_S, rs1_val_S, is_quiet); + + let rd_val_S = if (f_is_SNaN_S(rs1_val_S) & f_is_SNaN_S(rs2_val_S)) then canonical_NaN_S() + else if f_is_SNaN_S(rs1_val_S) then rs2_val_S + else if f_is_SNaN_S(rs2_val_S) then rs1_val_S + else if (f_is_QNaN_S(rs1_val_S) & f_is_QNaN_S(rs2_val_S)) then canonical_NaN_S() + else if f_is_QNaN_S(rs1_val_S) then rs2_val_S + else if f_is_QNaN_S(rs2_val_S) then rs1_val_S + else if (f_is_neg_zero_S(rs1_val_S) & f_is_pos_zero_S(rs2_val_S)) then rs2_val_S + else if (f_is_neg_zero_S(rs2_val_S) & f_is_pos_zero_S(rs1_val_S)) then rs1_val_S + else if rs2_lt_rs1 then rs1_val_S + else /* (not rs2_lt_rs1) */ rs2_val_S; + + write_fflags(fflags); + F(rd) = nan_box (rd_val_S); + RETIRE_SUCCESS +} + +function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FEQ_S)) = { + let rs1_val_S = nan_unbox (F(rs1)); + let rs2_val_S = nan_unbox (F(rs2)); + + let (rs1_eq_rs2, fflags) = feq_quiet_S (rs1_val_S, rs2_val_S); + + let rd_val : xlenbits = + if (f_is_SNaN_S(rs1_val_S) | f_is_SNaN_S(rs2_val_S)) then zeros() + else if (f_is_QNaN_S(rs1_val_S) | f_is_QNaN_S(rs2_val_S)) then zeros() + else if rs1_eq_rs2 then EXTZ(0b1) + else zeros(); + + write_fflags(fflags); + X(rd) = rd_val; + RETIRE_SUCCESS +} + +function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FLT_S)) = { + let rs1_val_S = nan_unbox (F(rs1)); + let rs2_val_S = nan_unbox (F(rs2)); + + let is_quiet = false; + let (rs1_lt_rs2, fflags) = flt_S (rs1_val_S, rs2_val_S, is_quiet); + + let rd_val : xlenbits = + if (f_is_SNaN_S(rs1_val_S) | f_is_SNaN_S(rs2_val_S)) then zeros() + else if (f_is_QNaN_S(rs1_val_S) | f_is_QNaN_S(rs2_val_S)) then zeros() + else if rs1_lt_rs2 then EXTZ(0b1) + else zeros(); + + write_fflags(fflags); + X(rd) = rd_val; + RETIRE_SUCCESS +} + +function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FLE_S)) = { + let rs1_val_S = nan_unbox (F(rs1)); + let rs2_val_S = nan_unbox (F(rs2)); + + let is_quiet = false; + let (rs1_le_rs2, fflags) = fle_S (rs1_val_S, rs2_val_S, is_quiet); + + let rd_val : xlenbits = + if (f_is_SNaN_S(rs1_val_S) | f_is_SNaN_S(rs2_val_S)) then zeros() + else if (f_is_QNaN_S(rs1_val_S) | f_is_QNaN_S(rs2_val_S)) then zeros() + else if rs1_le_rs2 then EXTZ(0b1) + else zeros(); + + write_fflags(fflags); + X(rd) = rd_val; + RETIRE_SUCCESS +} + +/* AST -> Assembly notation ================================ */ + +mapping f_bin_type_mnemonic_S : f_bin_op_S <-> string = { + FSGNJ_S <-> "fsgnj.s", + FSGNJN_S <-> "fsgnjn.s", + FSGNJX_S <-> "fsgnjx.s", + FMIN_S <-> "fmin.s", + FMAX_S <-> "fmax.s", + FEQ_S <-> "feq.s", + FLT_S <-> "flt.s", + FLE_S <-> "fle.s" +} + +mapping clause assembly = F_BIN_TYPE_S(rs2, rs1, rd, FSGNJ_S) + <-> f_bin_type_mnemonic_S(FSGNJ_S) + ^ spc() ^ freg_name(rd) + ^ sep() ^ freg_name(rs1) + ^ sep() ^ freg_name(rs2) + +mapping clause assembly = F_BIN_TYPE_S(rs2, rs1, rd, FSGNJN_S) + <-> f_bin_type_mnemonic_S(FSGNJN_S) + ^ spc() ^ freg_name(rd) + ^ sep() ^ freg_name(rs1) + ^ sep() ^ freg_name(rs2) + +mapping clause assembly = F_BIN_TYPE_S(rs2, rs1, rd, FSGNJX_S) + <-> f_bin_type_mnemonic_S(FSGNJX_S) + ^ spc() ^ freg_name(rd) + ^ sep() ^ freg_name(rs1) + ^ sep() ^ freg_name(rs2) + +mapping clause assembly = F_BIN_TYPE_S(rs2, rs1, rd, FMIN_S) + <-> f_bin_type_mnemonic_S(FMIN_S) + ^ spc() ^ freg_name(rd) + ^ sep() ^ freg_name(rs1) + ^ sep() ^ freg_name(rs2) + +mapping clause assembly = F_BIN_TYPE_S(rs2, rs1, rd, FMAX_S) + <-> f_bin_type_mnemonic_S(FMAX_S) + ^ spc() ^ freg_name(rd) + ^ sep() ^ freg_name(rs1) + ^ sep() ^ freg_name(rs2) + +mapping clause assembly = F_BIN_TYPE_S(rs2, rs1, rd, FEQ_S) + <-> f_bin_type_mnemonic_S(FEQ_S) + ^ spc() ^ reg_name(rd) + ^ sep() ^ freg_name(rs1) + ^ sep() ^ freg_name(rs2) + +mapping clause assembly = F_BIN_TYPE_S(rs2, rs1, rd, FLT_S) + <-> f_bin_type_mnemonic_S(FLT_S) + ^ spc() ^ reg_name(rd) + ^ sep() ^ freg_name(rs1) + ^ sep() ^ freg_name(rs2) + +mapping clause assembly = F_BIN_TYPE_S(rs2, rs1, rd, FLE_S) + <-> f_bin_type_mnemonic_S(FLE_S) + ^ spc() ^ reg_name(rd) + ^ sep() ^ freg_name(rs1) + ^ sep() ^ freg_name(rs2) + +/* ****************************************************************** */ +/* Unary, no rounding mode */ + +union clause ast = F_UN_TYPE_S : (regidx, regidx, f_un_op_S) + +/* AST <-> Binary encoding ================================ */ + +mapping clause encdec = F_UN_TYPE_S(rs1, rd, FCLASS_S) if haveFExt() + <-> 0b111_0000 @ 0b00000 @ rs1 @ 0b001 @ rd @ 0b101_0011 if haveFExt() + +mapping clause encdec = F_UN_TYPE_S(rs1, rd, FMV_X_W) if haveFExt() + <-> 0b111_0000 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveFExt() + +mapping clause encdec = F_UN_TYPE_S(rs1, rd, FMV_W_X) if haveFExt() + <-> 0b111_1000 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveFExt() + +/* Execution semantics ================================ */ + +function clause execute (F_UN_TYPE_S(rs1, rd, FCLASS_S)) = { + let rs1_val_S = nan_unbox (F(rs1)); + + let rd_val_10b : bits (10) = + if f_is_neg_inf_S (rs1_val_S) then 0b_00_0000_0001 + else if f_is_neg_norm_S (rs1_val_S) then 0b_00_0000_0010 + else if f_is_neg_subnorm_S (rs1_val_S) then 0b_00_0000_0100 + else if f_is_neg_zero_S (rs1_val_S) then 0b_00_0000_1000 + else if f_is_pos_zero_S (rs1_val_S) then 0b_00_0001_0000 + else if f_is_pos_subnorm_S (rs1_val_S) then 0b_00_0010_0000 + else if f_is_pos_norm_S (rs1_val_S) then 0b_00_0100_0000 + else if f_is_pos_inf_S (rs1_val_S) then 0b_00_1000_0000 + else if f_is_SNaN_S (rs1_val_S) then 0b_01_0000_0000 + else if f_is_QNaN_S (rs1_val_S) then 0b_10_0000_0000 + else zeros(); + + X(rd) = EXTZ (rd_val_10b); + RETIRE_SUCCESS +} + +function clause execute (F_UN_TYPE_S(rs1, rd, FMV_X_W)) = { + let rs1_val_S = F(rs1)[31..0]; + let rd_val_X : xlenbits = EXTS(rs1_val_S); + X(rd) = rd_val_X; + RETIRE_SUCCESS +} + +function clause execute (F_UN_TYPE_S(rs1, rd, FMV_W_X)) = { + let rs1_val_X = X(rs1); + let rd_val_S = rs1_val_X [31..0]; + F(rd) = nan_box (rd_val_S); + RETIRE_SUCCESS +} + +/* AST -> Assembly notation ================================ */ + +mapping f_un_type_mnemonic_S : f_un_op_S <-> string = { + FMV_X_W <-> "fmv.x.w", + FCLASS_S <-> "fclass.s", + FMV_W_X <-> "fmv.w.x" +} + +mapping clause assembly = F_UN_TYPE_S(rs1, rd, FMV_X_W) + <-> f_un_type_mnemonic_S(FMV_X_W) + ^ spc() ^ reg_name(rd) + ^ sep() ^ freg_name(rs1) + +mapping clause assembly = F_UN_TYPE_S(rs1, rd, FMV_W_X) + <-> f_un_type_mnemonic_S(FMV_W_X) + ^ spc() ^ freg_name(rd) + ^ sep() ^ reg_name(rs1) + +mapping clause assembly = F_UN_TYPE_S(rs1, rd, FCLASS_S) + <-> f_un_type_mnemonic_S(FCLASS_S) + ^ spc() ^ reg_name(rd) + ^ sep() ^ freg_name(rs1) + +/* ****************************************************************** */ diff --git a/model/riscv_insts_next.sail b/model/riscv_insts_next.sail index 2af2eeb..0d23452 100644 --- a/model/riscv_insts_next.sail +++ b/model/riscv_insts_next.sail @@ -9,6 +9,8 @@ mapping clause encdec = URET() function clause execute URET() = { if (~ (haveUsrMode())) then handle_illegal() + else if ~ (ext_check_xret_priv (User)) + then ext_fail_xret_priv () else set_next_pc(exception_handler(cur_privilege, CTL_URET(), PC)); RETIRE_FAIL } diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail index dd8a4a0..3f8ccd8 100644 --- a/model/riscv_insts_zicsr.sail +++ b/model/riscv_insts_zicsr.sail @@ -122,22 +122,22 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = { (0x3A2, _) => { pmpWriteCfgReg(2, value); Some(value) }, // pmpcfg2 (0x3A3, 32) => { pmpWriteCfgReg(3, value); Some(value) }, // pmpcfg3 - (0x3B0, _) => { pmpaddr0 = pmpWriteAddr(pmp0cfg, pmpaddr0, value); Some(pmpaddr0) }, - (0x3B1, _) => { pmpaddr1 = pmpWriteAddr(pmp1cfg, pmpaddr1, value); Some(pmpaddr1) }, - (0x3B2, _) => { pmpaddr2 = pmpWriteAddr(pmp2cfg, pmpaddr2, value); Some(pmpaddr2) }, - (0x3B3, _) => { pmpaddr3 = pmpWriteAddr(pmp3cfg, pmpaddr3, value); Some(pmpaddr3) }, - (0x3B4, _) => { pmpaddr4 = pmpWriteAddr(pmp4cfg, pmpaddr4, value); Some(pmpaddr4) }, - (0x3B5, _) => { pmpaddr5 = pmpWriteAddr(pmp5cfg, pmpaddr5, value); Some(pmpaddr5) }, - (0x3B6, _) => { pmpaddr6 = pmpWriteAddr(pmp6cfg, pmpaddr6, value); Some(pmpaddr6) }, - (0x3B7, _) => { pmpaddr7 = pmpWriteAddr(pmp7cfg, pmpaddr7, value); Some(pmpaddr7) }, - (0x3B8, _) => { pmpaddr8 = pmpWriteAddr(pmp8cfg, pmpaddr8, value); Some(pmpaddr8) }, - (0x3B9, _) => { pmpaddr9 = pmpWriteAddr(pmp9cfg, pmpaddr9, value); Some(pmpaddr9) }, - (0x3BA, _) => { pmpaddr10 = pmpWriteAddr(pmp10cfg, pmpaddr10, value); Some(pmpaddr10) }, - (0x3BB, _) => { pmpaddr11 = pmpWriteAddr(pmp11cfg, pmpaddr11, value); Some(pmpaddr11) }, - (0x3BC, _) => { pmpaddr12 = pmpWriteAddr(pmp12cfg, pmpaddr12, value); Some(pmpaddr12) }, - (0x3BD, _) => { pmpaddr13 = pmpWriteAddr(pmp13cfg, pmpaddr13, value); Some(pmpaddr13) }, - (0x3BE, _) => { pmpaddr14 = pmpWriteAddr(pmp14cfg, pmpaddr14, value); Some(pmpaddr14) }, - (0x3BF, _) => { pmpaddr15 = pmpWriteAddr(pmp15cfg, pmpaddr15, value); Some(pmpaddr15) }, + (0x3B0, _) => { pmpaddr0 = pmpWriteAddr(pmpLocked(pmp0cfg), pmpTORLocked(pmp1cfg), pmpaddr0, value); Some(pmpaddr0) }, + (0x3B1, _) => { pmpaddr1 = pmpWriteAddr(pmpLocked(pmp1cfg), pmpTORLocked(pmp2cfg), pmpaddr1, value); Some(pmpaddr1) }, + (0x3B2, _) => { pmpaddr2 = pmpWriteAddr(pmpLocked(pmp2cfg), pmpTORLocked(pmp3cfg), pmpaddr2, value); Some(pmpaddr2) }, + (0x3B3, _) => { pmpaddr3 = pmpWriteAddr(pmpLocked(pmp3cfg), pmpTORLocked(pmp4cfg), pmpaddr3, value); Some(pmpaddr3) }, + (0x3B4, _) => { pmpaddr4 = pmpWriteAddr(pmpLocked(pmp4cfg), pmpTORLocked(pmp5cfg), pmpaddr4, value); Some(pmpaddr4) }, + (0x3B5, _) => { pmpaddr5 = pmpWriteAddr(pmpLocked(pmp5cfg), pmpTORLocked(pmp6cfg), pmpaddr5, value); Some(pmpaddr5) }, + (0x3B6, _) => { pmpaddr6 = pmpWriteAddr(pmpLocked(pmp6cfg), pmpTORLocked(pmp7cfg), pmpaddr6, value); Some(pmpaddr6) }, + (0x3B7, _) => { pmpaddr7 = pmpWriteAddr(pmpLocked(pmp7cfg), pmpTORLocked(pmp8cfg), pmpaddr7, value); Some(pmpaddr7) }, + (0x3B8, _) => { pmpaddr8 = pmpWriteAddr(pmpLocked(pmp8cfg), pmpTORLocked(pmp9cfg), pmpaddr8, value); Some(pmpaddr8) }, + (0x3B9, _) => { pmpaddr9 = pmpWriteAddr(pmpLocked(pmp9cfg), pmpTORLocked(pmp10cfg), pmpaddr9, value); Some(pmpaddr9) }, + (0x3BA, _) => { pmpaddr10 = pmpWriteAddr(pmpLocked(pmp10cfg), pmpTORLocked(pmp11cfg), pmpaddr10, value); Some(pmpaddr10) }, + (0x3BB, _) => { pmpaddr11 = pmpWriteAddr(pmpLocked(pmp11cfg), pmpTORLocked(pmp12cfg), pmpaddr11, value); Some(pmpaddr11) }, + (0x3BC, _) => { pmpaddr12 = pmpWriteAddr(pmpLocked(pmp12cfg), pmpTORLocked(pmp13cfg), pmpaddr12, value); Some(pmpaddr12) }, + (0x3BD, _) => { pmpaddr13 = pmpWriteAddr(pmpLocked(pmp13cfg), pmpTORLocked(pmp14cfg), pmpaddr13, value); Some(pmpaddr13) }, + (0x3BE, _) => { pmpaddr14 = pmpWriteAddr(pmpLocked(pmp14cfg), pmpTORLocked(pmp15cfg), pmpaddr14, value); Some(pmpaddr14) }, + (0x3BF, _) => { pmpaddr15 = pmpWriteAddr(pmpLocked(pmp15cfg), false, pmpaddr15, value); Some(pmpaddr15) }, /* machine mode counters */ (0xB00, _) => { mcycle[(sizeof(xlen) - 1) .. 0] = value; Some(value) }, @@ -179,6 +179,8 @@ function clause execute CSR(csr, rs1, rd, is_imm, op) = { }; if ~ (check_CSR(csr, cur_privilege, isWrite)) then { handle_illegal(); RETIRE_FAIL } + else if ~ (ext_check_CSR(csr, cur_privilege, isWrite)) + then { ext_check_CSR_fail(); RETIRE_FAIL } else { let csr_val = readCSR(csr); /* could have side-effects, so technically shouldn't perform for CSRW[I] with rd == 0 */ if isWrite then { @@ -206,6 +208,6 @@ mapping csr_mnemonic : csrop <-> string = { } mapping clause assembly = CSR(csr, rs1, rd, true, op) - <-> csr_mnemonic(op) ^ "i" ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_5(rs1) ^ sep() ^ csr_name_map(csr) + <-> csr_mnemonic(op) ^ "i" ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_5(rs1) ^ sep() ^ hex_bits_12(csr) mapping clause assembly = CSR(csr, rs1, rd, false, op) - <-> csr_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ csr_name_map(csr) + <-> csr_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_12(csr) diff --git a/model/riscv_iris.sail b/model/riscv_iris.sail new file mode 100644 index 0000000..80f3515 --- /dev/null +++ b/model/riscv_iris.sail @@ -0,0 +1,1176 @@ +default Order dec + +$include <smt.sail> +$include <option.sail> +$include <arith.sail> +$include <string.sail> +$include <vector_dec.sail> +$include <regfp.sail> + +val string_startswith = "string_startswith" : (string, string) -> bool +val string_drop = "string_drop" : (string, nat) -> string +val string_take = "string_take" : (string, nat) -> string +val string_length = "string_length" : string -> nat +val string_append = {c: "concat_str", _: "string_append"} : (string, string) -> string + +val eq_anything = {ocaml: "(fun (x, y) -> x = y)", interpreter: "eq_anything", lem: "eq", coq: "generic_eq", c: "eq_anything"} : forall ('a : Type). ('a, 'a) -> bool + +overload operator == = {eq_string, eq_anything} + +val "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg} +/* sneaky deref with no effect necessary for bitfield writes */ +val _reg_deref = "reg_deref" : forall ('a : Type). register('a) -> 'a + +val any_vector_update = {ocaml: "update", lem: "update_list_dec", coq: "vector_update"} : forall 'n ('a : Type). + (vector('n, dec, 'a), int, 'a) -> vector('n, dec, 'a) + +overload vector_update = {any_vector_update} + +val update_subrange = {ocaml: "update_subrange", interpreter: "update_subrange", lem: "update_subrange_vec_dec", coq: "update_subrange_vec_dec"} : forall 'n 'm 'o. + (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n) + +val vector_concat = {ocaml: "append", lem: "append_list", coq: "vec_concat"} : forall ('n : Int) ('m : Int) ('a : Type). + (vector('n, dec, 'a), vector('m, dec, 'a)) -> vector('n + 'm, dec, 'a) + +overload append = {vector_concat} + +overload ~ = {not_bool, not_vec} + +val neq_vec = {lem: "neq"} : forall 'n. (bits('n), bits('n)) -> bool + +function neq_vec (x, y) = not_bool(eq_bits(x, y)) + +val neq_anything = {lem: "neq", coq: "generic_neq"} : forall ('a : Type). ('a, 'a) -> bool + +function neq_anything (x, y) = not_bool(x == y) + +overload operator != = {neq_vec, neq_anything} + +overload operator & = {and_vec} + +overload operator | = {or_vec} + +val string_of_int = {c: "string_of_int", ocaml: "string_of_int", interpreter: "string_of_int", lem: "stringFromInteger", coq: "string_of_int"} : int -> string + +val "string_of_bits" : forall 'n. bits('n) -> string + +function string_of_bit(b: bit) -> string = + match b { + bitzero => "0b0", + bitone => "0b1" + } + +overload BitStr = {string_of_bits, string_of_bit} + +val xor_vec = {c: "xor_bits", _: "xor_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) + +val int_power = {ocaml: "int_power", interpreter: "int_power", lem: "pow", coq: "pow", c: "pow_int"} : (int, int) -> int + +overload operator ^ = {xor_vec, int_power, concat_str} + +val sub_vec = {c: "sub_bits", _: "sub_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) + +val sub_vec_int = {c: "sub_bits_int", _: "sub_vec_int"} : forall 'n. (bits('n), int) -> bits('n) + +overload operator - = {sub_vec, sub_vec_int} + +val quot_round_zero = {ocaml: "quot_round_zero", interpreter: "quot_round_zero", lem: "hardware_quot", c: "tdiv_int", coq: "Z.quot"} : (int, int) -> int +val rem_round_zero = {ocaml: "rem_round_zero", interpreter: "rem_round_zero", lem: "hardware_mod", c: "tmod_int", coq: "Z.rem"} : (int, int) -> int + +/* The following should get us euclidean modulus, and is compatible with pre and post 0.9 versions of sail */ +overload operator % = {emod_int, mod} + +val min_nat = {ocaml: "min_int", interpreter: "min_int", lem: "min", coq: "min_nat", c: "min_int"} : (nat, nat) -> nat + +val min_int = {ocaml: "min_int", interpreter: "min_int", lem: "min", coq: "Z.min", c: "min_int"} : (int, int) -> int + +val max_nat = {ocaml: "max_int", interpreter: "max_int", lem: "max", coq: "max_nat", c: "max_int"} : (nat, nat) -> nat + +val max_int = {ocaml: "max_int", interpreter: "max_int", lem: "max", coq: "Z.max", c: "max_int"} : (int, int) -> int + +overload min = {min_nat, min_int} + +overload max = {max_nat, max_int} + +val pow2 = "pow2" : forall 'n. atom('n) -> atom(2 ^ 'n) + +val print = "print_endline" : string -> unit +val print_string = "print_string" : (string, string) -> unit + +val print_instr = {ocaml: "Platform.print_instr", interpreter: "print_endline", c: "print_instr", lem: "print_dbg", _: "print_endline"} : string -> unit +val print_reg = {ocaml: "Platform.print_reg", interpreter: "print_endline", c: "print_reg", lem: "print_dbg", _: "print_endline"} : string -> unit +val print_mem = {ocaml: "Platform.print_mem_access", interpreter: "print_endline", c: "print_mem_access", lem: "print_dbg", _: "print_endline"} : string -> unit +val print_platform = {ocaml: "Platform.print_platform", interpreter: "print_endline", c: "print_platform", lem: "print_dbg", _: "print_endline"} : string -> unit + +val get_config_print_instr = {ocaml: "Platform.get_config_print_instr", c:"get_config_print_instr"} : unit -> bool +val get_config_print_reg = {ocaml: "Platform.get_config_print_reg", c:"get_config_print_reg"} : unit -> bool +val get_config_print_mem = {ocaml: "Platform.get_config_print_mem", c:"get_config_print_mem"} : unit -> bool + +val get_config_print_platform = {ocaml: "Platform.get_config_print_platform", c:"get_config_print_platform"} : unit -> bool +// defaults for other backends +function get_config_print_instr () = false +function get_config_print_reg () = false +function get_config_print_mem () = false +function get_config_print_platform () = false + +val EXTS : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m) +val EXTZ : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m) + +function EXTS(m, v) = sail_sign_extend(v, m) +function EXTZ(m, v) = sail_zero_extend(v, m) + +val zeros_implicit : forall 'n, 'n >= 0 . implicit('n) -> bits('n) +function zeros_implicit (n) = sail_zeros(n) +overload zeros = {zeros_implicit} + +val ones : forall 'n, 'n >= 0 . implicit('n) -> bits('n) +function ones (n) = sail_ones (n) + +val bool_to_bits : bool -> bits(1) +function bool_to_bits x = if x then 0b1 else 0b0 + +val bit_to_bool : bit -> bool +function bit_to_bool b = match b { + bitone => true, + bitzero => false +} + +val to_bits : forall 'l, 'l >= 0.(atom('l), int) -> bits('l) +function to_bits (l, n) = get_slice_int(l, n, 0) + +infix 4 <_s +infix 4 >=_s +infix 4 <_u +infix 4 >=_u +infix 4 <=_u + +val operator <_s : forall 'n, 'n > 0. (bits('n), bits('n)) -> bool +val operator >=_s : forall 'n, 'n > 0. (bits('n), bits('n)) -> bool +val operator <_u : forall 'n. (bits('n), bits('n)) -> bool +val operator >=_u : forall 'n. (bits('n), bits('n)) -> bool +val operator <=_u : forall 'n. (bits('n), bits('n)) -> bool + +function operator <_s (x, y) = signed(x) < signed(y) +function operator >=_s (x, y) = signed(x) >= signed(y) +function operator <_u (x, y) = unsigned(x) < unsigned(y) +function operator >=_u (x, y) = unsigned(x) >= unsigned(y) +function operator <=_u (x, y) = unsigned(x) <= unsigned(y) + +infix 7 >> +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) + +overload operator >> = {shift_bits_right, shiftr} +overload operator << = {shift_bits_left, shiftl} + +/* Ideally these would be sail builtin */ + +function shift_right_arith64 (v : bits(64), shift : bits(6)) -> bits(64) = + let v128 : bits(128) = EXTS(v) in + (v128 >> shift)[63..0] + +function shift_right_arith32 (v : bits(32), shift : bits(5)) -> bits(32) = + let v64 : bits(64) = EXTS(v) in + (v64 >> shift)[31..0] + +val "decimal_string_of_bits" : forall 'n. bits('n) -> string +val hex_bits : forall 'n . (atom('n), bits('n)) <-> string + +/* Define the XLEN value for the architecture. */ + +type xlen : Int = 64 +type xlen_bytes : Int = 8 +type xlenbits = bits(xlen) +/* The default metadata carries no information, and is implemented + * using a unit type. + */ + +type mem_meta = unit + +let default_meta : mem_meta = () + +val __WriteRAM_Meta : forall 'n. (xlenbits, atom('n), mem_meta) -> unit effect {wmvt} +function __WriteRAM_Meta(addr, width, meta) = () + +val __ReadRAM_Meta : forall 'n. (xlenbits, atom('n)) -> mem_meta effect {rmem} +function __ReadRAM_Meta(addr, width) = () +/* These functions define the primitives for physical memory access. + * They depend on the XLEN of the architecture. + * + * They also depend on the type of metadata that is read and written + * to physical memory. For models that do not require this metadata, + * a unit type can be used. + * + * The underlying __read_mem and __write_mem functions are from the + * Sail library. The metadata primitives __{Read,Write}RAM_Meta are + * in prelude_mem_metadata. + */ + + +/* This is a slightly arbitrary limit on the maximum number of bytes + in a memory access. It helps to generate slightly better C code + because it means width argument can be fast native integer. It + would be even better if it could be <= 8 bytes so that data can + also be a 64-bit int but CHERI needs 128-bit accesses for + 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_ea : forall 'n, 0 < 'n <= max_mem_access . (write_kind, xlenbits, atom('n)) -> unit effect {eamem} +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} +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) + + +/* Basic type and function definitions used pervasively in the model. */ + +/* this value is only defined for the runtime platform for ELF loading + * checks, and not used in the model. + */ +let xlen_val = sizeof(xlen) + +let xlen_max_unsigned = 2 ^ sizeof(xlen) - 1 +let xlen_max_signed = 2 ^ (sizeof(xlen) - 1) - 1 +let xlen_min_signed = 0 - 2 ^ (sizeof(xlen) - 1) + +type half = bits(16) +type word = bits(32) + +/* register identifiers */ + +type regidx = bits(5) +type cregidx = bits(3) /* identifiers in RVC instructions */ +type csreg = bits(12) /* CSR addressing */ + +/* register file indexing */ + +type regno ('n : Int), 0 <= 'n < 32 = atom('n) + +val regidx_to_regno : bits(5) -> {'n, 0 <= 'n < 32. regno('n)} +function regidx_to_regno b = let 'r = unsigned(b) in r + +/* mapping RVC register indices into normal indices */ +val creg2reg_idx : cregidx -> regidx +function creg2reg_idx(creg) = 0b01 @ creg + +/* some architecture and ABI relevant register identifiers */ +let zreg : regidx = 0b00000 /* x0, zero register */ +let ra : regidx = 0b00001 /* x1, return address */ +let sp : regidx = 0b00010 /* x2, stack pointer */ + +/* instruction fields */ + +type opcode = bits(7) +type imm12 = bits(12) +type imm20 = bits(20) +type amo = bits(1) /* amo opcode flags */ + +/* base architecture definitions */ + +enum Architecture = {RV32, RV64, RV128} +type arch_xlen = bits(2) +function architecture(a : arch_xlen) -> option(Architecture) = + match (a) { + 0b01 => Some(RV32), + 0b10 => Some(RV64), + 0b11 => Some(RV128), + _ => None() + } + +function arch_to_bits(a : Architecture) -> arch_xlen = + match (a) { + RV32 => 0b01, + RV64 => 0b10, + RV128 => 0b11 + } + +/* enum denoting whether an executed instruction retires */ + +enum Retired = {RETIRE_SUCCESS, RETIRE_FAIL} + +/* memory access types */ + +union AccessType ('a : Type) = { + Read : 'a, + Write : 'a, + ReadWrite : 'a, + Execute : unit +} + +enum word_width = {BYTE, HALF, WORD, DOUBLE} +/* model-internal exceptions */ + +union exception = { + Error_not_implemented : string, + Error_internal_error : unit +} + +val not_implemented : forall ('a : Type). string -> 'a effect {escape} +function not_implemented message = throw(Error_not_implemented(message)) + +val internal_error : forall ('a : Type). string -> 'a effect {escape} +function internal_error(s) = { + assert (false, s); + throw Error_internal_error() +} + +/* instruction opcode grouping */ +enum bop = {RISCV_BEQ, RISCV_BNE, RISCV_BLT, + RISCV_BGE, RISCV_BLTU, RISCV_BGEU} /* branch ops */ +enum iop = {RISCV_ADDI, RISCV_SLTI, RISCV_SLTIU, + RISCV_XORI, RISCV_ORI, RISCV_ANDI} /* immediate ops */ + +mapping bool_bits : bool <-> bits(1) = { + true <-> 0b1, + false <-> 0b0 +} + +mapping bool_not_bits : bool <-> bits(1) = { + true <-> 0b0, + false <-> 0b1 +} + +mapping size_bits : word_width <-> bits(2) = { + BYTE <-> 0b00, + HALF <-> 0b01, + WORD <-> 0b10, + DOUBLE <-> 0b11 +} + +val word_width_bytes : word_width -> {'s, 's == 1 | 's == 2 | 's == 4 | 's == 8 . atom('s)} +function word_width_bytes width = match width { + BYTE => 1, + HALF => 2, + WORD => 4, + DOUBLE => 8 +} +// Extensions for memory Accesstype. + +type ext_access_type = unit + +let Data : ext_access_type = () + +let default_write_acc : ext_access_type = Data + +val accessType_to_str : AccessType(ext_access_type) -> string +function accessType_to_str (a) = + match (a) { + Read(Data) => "R", + Write(Data) => "W", + ReadWrite(Data) => "RW", + Execute() => "X" + } + +overload to_str = {accessType_to_str} +/* default register type */ +type regtype = xlenbits + +/* default zero register */ +let zero_reg : regtype = EXTZ(0x0) + +/* default register printer */ +val RegStr : regtype -> string +function RegStr(r) = BitStr(r) + +/* conversions */ + +val regval_from_reg : regtype -> xlenbits +function regval_from_reg(r) = r + +val regval_into_reg : xlenbits -> regtype +function regval_into_reg(v) = v +/* program counter */ + +register PC : xlenbits +register nextPC : xlenbits + +/* internal state to hold instruction bits for faulting instructions */ +register instbits : xlenbits + +/* register file and accessors */ + +register Xs : vector(32, dec, regtype) + +register x1 : regtype +register x2 : regtype +register x3 : regtype +register x4 : regtype +register x5 : regtype +register x6 : regtype +register x7 : regtype +register x8 : regtype +register x9 : regtype +register x10 : regtype +register x11 : regtype +register x12 : regtype +register x13 : regtype +register x14 : regtype +register x15 : regtype +register x16 : regtype +register x17 : regtype +register x18 : regtype +register x19 : regtype +register x20 : regtype +register x21 : regtype +register x22 : regtype +register x23 : regtype +register x24 : regtype +register x25 : regtype +register x26 : regtype +register x27 : regtype +register x28 : regtype +register x29 : regtype +register x30 : regtype +register x31 : regtype + +val rX : forall 'n, 0 <= 'n < 32. regno('n) -> xlenbits effect {rreg, escape} +function rX r = { + let v : regtype = + match r { + 0 => zero_reg, + 1 => x1, + 2 => x2, + 3 => x3, + 4 => x4, + 5 => x5, + 6 => x6, + 7 => x7, + 8 => x8, + 9 => x9, + 10 => x10, + 11 => x11, + 12 => x12, + 13 => x13, + 14 => x14, + 15 => x15, + 16 => x16, + 17 => x17, + 18 => x18, + 19 => x19, + 20 => x20, + 21 => x21, + 22 => x22, + 23 => x23, + 24 => x24, + 25 => x25, + 26 => x26, + 27 => x27, + 28 => x28, + 29 => x29, + 30 => x30, + 31 => x31, + _ => {assert(false, "invalid register number"); zero_reg} + }; + regval_from_reg(v) +} + +val wX : forall 'n, 0 <= 'n < 32. (regno('n), xlenbits) -> unit effect {wreg, escape} +function wX (r, in_v) = { + let v = regval_into_reg(in_v); + match r { + 0 => (), + 1 => x1 = v, + 2 => x2 = v, + 3 => x3 = v, + 4 => x4 = v, + 5 => x5 = v, + 6 => x6 = v, + 7 => x7 = v, + 8 => x8 = v, + 9 => x9 = v, + 10 => x10 = v, + 11 => x11 = v, + 12 => x12 = v, + 13 => x13 = v, + 14 => x14 = v, + 15 => x15 = v, + 16 => x16 = v, + 17 => x17 = v, + 18 => x18 = v, + 19 => x19 = v, + 20 => x20 = v, + 21 => x21 = v, + 22 => x22 = v, + 23 => x23 = v, + 24 => x24 = v, + 25 => x25 = v, + 26 => x26 = v, + 27 => x27 = v, + 28 => x28 = v, + 29 => x29 = v, + 30 => x30 = v, + 31 => x31 = v, + _ => assert(false, "invalid register number") + }; + if (r != 0) then { + if get_config_print_reg() + then print_reg("x" ^ string_of_int(r) ^ " <- " ^ RegStr(v)); + } +} + +function rX_bits(i: bits(5)) -> xlenbits = rX(unsigned(i)) + +function wX_bits(i: bits(5), data: xlenbits) -> unit = { + wX(unsigned(i)) = data +} + +overload X = {rX_bits, wX_bits, rX, wX} + +val init_base_regs : unit -> unit effect {wreg} +function init_base_regs () = { + x1 = zero_reg; + x2 = zero_reg; + x3 = zero_reg; + x4 = zero_reg; + x5 = zero_reg; + x6 = zero_reg; + x7 = zero_reg; + x8 = zero_reg; + x9 = zero_reg; + x10 = zero_reg; + x11 = zero_reg; + x12 = zero_reg; + x13 = zero_reg; + x14 = zero_reg; + x15 = zero_reg; + x16 = zero_reg; + x17 = zero_reg; + x18 = zero_reg; + x19 = zero_reg; + x20 = zero_reg; + x21 = zero_reg; + x22 = zero_reg; + x23 = zero_reg; + x24 = zero_reg; + x25 = zero_reg; + x26 = zero_reg; + x27 = zero_reg; + x28 = zero_reg; + x29 = zero_reg; + x30 = zero_reg; + x31 = zero_reg +} +/* accessors for default architectural addresses, for use from within instructions */ + +/*! + Retrieves the architectural PC value. This is not necessarily the value + found in the PC register as extensions may choose to override this function. + The value in the PC register is the absolute virtual address of the instruction + to fetch. + */ +val get_arch_pc : unit -> xlenbits effect {rreg} +function get_arch_pc() = PC + +val get_next_pc : unit -> xlenbits effect {rreg} +function get_next_pc() = nextPC + +val set_next_pc : xlenbits -> unit effect {wreg} +function set_next_pc(pc) = { + nextPC = pc +} + +val tick_pc : unit -> unit effect {rreg, wreg} +function tick_pc() = { + PC = nextPC +} + +/* Extensions may wish to interpose on fetch, control transfer, and data + * addresses used to access memory and perhaps modify them. This file + * defines the return values used by functions that perform this interposition. + * + * The model defines defaults for these functions in riscv_addr_checks.sail; + * extensions would need to define their own functions to override them. + */ + +union Ext_FetchAddr_Check ('a : Type) = { + Ext_FetchAddr_OK : xlenbits, /* PC value to use for the actual fetch */ + Ext_FetchAddr_Error : 'a +} + +union Ext_ControlAddr_Check ('a : Type) = { + Ext_ControlAddr_OK : xlenbits, /* PC value to use for the target of the control operation */ + Ext_ControlAddr_Error : 'a +} + +union Ext_DataAddr_Check ('a : Type) = { + Ext_DataAddr_OK : xlenbits, /* Address to use for the data access */ + Ext_DataAddr_Error : 'a +} +/* default fetch address checks */ + +type ext_fetch_addr_error = unit + +/* Since fetch is done in granules, the check function gets two arguments: + * start_pc: the PC at the start of the current fetch sequence + * pc: the PC for the current granule + * + * returns: the *virtual* memory address to use for the fetch. + * any address translation errors are reported for pc, not the returned value. + */ +function ext_fetch_check_pc(start_pc : xlenbits, pc : xlenbits) -> Ext_FetchAddr_Check(ext_fetch_addr_error) = + Ext_FetchAddr_OK(pc) + +function ext_handle_fetch_check_error(err : ext_fetch_addr_error) -> unit = + () + +/* default control address checks */ + +type ext_control_addr_error = unit + +/* these functions return the address to use as the target for + * the control transfer. any address translation or other errors + * are reported for the original value, not the returned value. + * + * NOTE: the input value does *not* have bit[0] set to 0, to enable + * more accurate bounds checking. There is no constraint on the output + * value, which will have bit[0] cleared by the caller if needed. + */ + +/* the control address is derived from a non-PC register, e.g. in JALR */ +function ext_control_check_addr(pc : xlenbits) -> Ext_ControlAddr_Check(ext_control_addr_error) = + Ext_ControlAddr_OK(pc) + +/* the control address is derived from the PC register, e.g. in JAL */ +function ext_control_check_pc(pc : xlenbits) -> Ext_ControlAddr_Check(ext_control_addr_error) = + Ext_ControlAddr_OK(pc) + +function ext_handle_control_check_error(err : ext_control_addr_error) -> unit = + () + + +/* The default data address function does not perform any checks so + just uses unit for error type. */ +type ext_data_addr_error = unit + +/* Default data addr is just base register + immediate offset (may be zero). + Extensions might override and add additional checks. */ +function ext_data_get_addr(base : regidx, offset : xlenbits, acc : AccessType(ext_access_type), width : word_width) + -> Ext_DataAddr_Check(ext_data_addr_error) = + let addr = X(base) + offset in + Ext_DataAddr_OK(addr) + +/* Machine-mode and supervisor-mode functionality. */ + +union ExceptionType = { + E_Fetch_Addr_Align : unit, + E_Fetch_Access_Fault : unit, + E_Illegal_Instr : unit, + E_Breakpoint : unit, + E_Load_Addr_Align : unit, + E_Load_Access_Fault : unit, + E_SAMO_Addr_Align : unit, + E_SAMO_Access_Fault : unit, + E_U_EnvCall : unit, + E_S_EnvCall : unit, + E_Reserved_10 : unit, + E_M_EnvCall : unit, + E_Fetch_Page_Fault : unit, + E_Load_Page_Fault : unit, + E_Reserved_14 : unit, + E_SAMO_Page_Fault : unit, +} + +function handle_mem_exception(addr : xlenbits, e : ExceptionType) -> unit = { + assert(false); +} + + +/* memory access exceptions, defined here for use by the platform model. */ + +union MemoryOpResult ('a : Type) = { + MemValue : 'a, + MemException : ExceptionType +} + +val MemoryOpResult_add_meta : forall ('t : Type). (MemoryOpResult('t), mem_meta) -> MemoryOpResult(('t, mem_meta)) +function MemoryOpResult_add_meta(r, m) = match r { + MemValue(v) => MemValue(v, m), + MemException(e) => MemException(e) +} + +val MemoryOpResult_drop_meta : forall ('t : Type). MemoryOpResult(('t, mem_meta)) -> MemoryOpResult('t) +function MemoryOpResult_drop_meta(r) = match r { + MemValue(v, m) => MemValue(v), + MemException(e) => MemException(e) +} + +/* whether the platform supports misaligned accesses without trapping to M-mode. if false, + * misaligned loads/stores are trapped to Machine mode. + */ +function plat_enable_misaligned_access () : unit -> bool = true + +/* Platform-specific handling of instruction faults */ + +function handle_illegal() -> unit = { + assert(false); +} + +/* Physical memory model. + * + * This assumes that the platform memory map has been defined, so that accesses + * to MMIO regions can be dispatched. + * + * The implementation below supports the reading and writing of memory + * metadata in addition to raw memory data. + * + * The external API for this module is + * {mem_read, mem_read_meta, mem_write_ea, mem_write_value_meta, mem_write_value} + * where mem_write_value is a special case of mem_write_value_meta that uses + * a default value of the metadata. + * + * The internal implementation first performs a PMP check (if PMP is + * enabled), and then dispatches to MMIO regions or physical memory as + * per the platform memory map. + */ + +function is_aligned_addr forall 'n. (addr : xlenbits, width : atom('n)) -> bool = + unsigned(addr) % width == 0 + +function read_kind_of_flags (aq : bool, rl : bool, res : bool) -> option(read_kind) = + match (aq, rl, res) { + (false, false, false) => Some(Read_plain), + (true, false, false) => Some(Read_RISCV_acquire), + (true, true, false) => Some(Read_RISCV_strong_acquire), + (false, false, true) => Some(Read_RISCV_reserved), + (true, false, true) => Some(Read_RISCV_reserved_acquire), + (true, true, true) => Some(Read_RISCV_reserved_strong_acquire), + (false, true, false) => None(), /* should these be instead throwing error_not_implemented as below? */ + (false, true, true) => None() + } + +// 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)) = { + let result = (match read_kind_of_flags(aq, rl, res) { + Some(rk) => Some(read_ram(rk, paddr, width, meta)), + None() => None() + }) : option((bits(8 * 'n), mem_meta)); + match (t, result) { + (Execute(), None()) => MemException(E_Fetch_Access_Fault()), + (Read(Data), None()) => MemException(E_Load_Access_Fault()), + (_, None()) => MemException(E_SAMO_Access_Fault()), + (_, Some(v, m)) => { MemValue(v, m) } + } +} + +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} + +function mem_read (typ, paddr, width, aq, rl, res) = { + let result : MemoryOpResult(bits(8 * 'n)) = + if (aq | res) & (~ (is_aligned_addr(paddr, width))) + then MemException(E_Load_Addr_Align()) + else match (aq, rl, res) { + (false, true, false) => throw(Error_not_implemented("load.rl")), + (false, true, true) => throw(Error_not_implemented("lr.rl")), + (_, _, _) => MemoryOpResult_drop_meta(phys_mem_read(typ, paddr, width, aq, rl, res, false)) + }; + result +} + +val mem_write_ea : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(unit) effect {eamem, escape} + +function mem_write_ea (addr, width, aq, rl, con) = { + if (rl | con) & (~ (is_aligned_addr(addr, width))) + then MemException(E_SAMO_Addr_Align()) + else match (aq, rl, con) { + (false, false, false) => MemValue(write_ram_ea(Write_plain, addr, width)), + (false, true, false) => MemValue(write_ram_ea(Write_RISCV_release, addr, width)), + (false, false, true) => MemValue(write_ram_ea(Write_RISCV_conditional, addr, width)), + (false, true , true) => MemValue(write_ram_ea(Write_RISCV_conditional_release, addr, width)), + (true, false, false) => throw(Error_not_implemented("store.aq")), + (true, true, false) => MemValue(write_ram_ea(Write_RISCV_strong_release, addr, width)), + (true, false, true) => throw(Error_not_implemented("sc.aq")), + (true, true , true) => MemValue(write_ram_ea(Write_RISCV_conditional_strong_release, addr, width)) + } +} + +// 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) = { + let result = MemValue(write_ram(wk, paddr, width, data, meta)); + result +} + +/* Atomic accesses can be done to MMIO regions, e.g. in kernel access to device registers. */ + +/* Memory write with an explicit metadata value. Metadata writes are + * currently assumed to have the same alignment constraints as their + * data. + * NOTE: The wreg effect is due to MMIO, the rreg is due to checking mtime. + */ +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} +function mem_write_value_meta (paddr, width, value, ext_acc, meta, aq, rl, con) = { + if (rl | con) & (~ (is_aligned_addr(paddr, width))) + then MemException(E_SAMO_Addr_Align()) + else match (aq, rl, con) { + (false, false, false) => phys_mem_write(Write_plain, paddr, width, value, meta), + (false, true, false) => phys_mem_write(Write_RISCV_release, paddr, width, value, meta), + (false, false, true) => phys_mem_write(Write_RISCV_conditional, paddr, width, value, meta), + (false, true , true) => phys_mem_write(Write_RISCV_conditional_release, paddr, width, value, meta), + (true, true, false) => phys_mem_write(Write_RISCV_strong_release, paddr, width, value, meta), + (true, true , true) => phys_mem_write(Write_RISCV_conditional_strong_release, paddr, width, value, meta), + // throw an illegal instruction here? + (true, false, false) => throw(Error_not_implemented("store.aq")), + (true, false, true) => throw(Error_not_implemented("sc.aq")) + } +} + +/* Memory write with a default metadata value. */ +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} +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) + +/* Result of address translation */ + +type ext_ptw = unit + +union TR_Result('paddr : Type, 'failure : Type) = { + TR_Address : ('paddr, ext_ptw), + TR_Failure : ('failure, ext_ptw) +} + +val translateAddr : (xlenbits, AccessType(ext_access_type)) -> TR_Result(xlenbits, ExceptionType) effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg} +function translateAddr(vAddr, ac) = { + TR_Address(vAddr, ()); +} + +/* Instruction definitions. + * + * This includes decoding, execution, and assembly parsing and printing. + */ + +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} +scattered function execute + +val encdec : ast <-> bits(32) +scattered mapping encdec + +///* see riscv_jalr_seq.sail or riscv_jalr_rmem.sail for the execute clause. */ +// +///* ***************************************************************** +//union clause ast = BTYPE : (bits(13), regidx, regidx, bop) +// +//mapping encdec_bop : bop <-> bits(3) = { +// RISCV_BEQ <-> 0b000, +// RISCV_BNE <-> 0b001, +// RISCV_BLT <-> 0b100, +// RISCV_BGE <-> 0b101, +// RISCV_BLTU <-> 0b110, +// RISCV_BGEU <-> 0b111 +//} +// +//mapping clause encdec = BTYPE(imm7_6 @ imm5_0 @ imm7_5_0 @ imm5_4_1 @ 0b0, rs2, rs1, op) +// <-> imm7_6 : bits(1) @ imm7_5_0 : bits(6) @ rs2 @ rs1 @ encdec_bop(op) @ imm5_4_1 : bits(4) @ imm5_0 : bits(1) @ 0b1100011 +// +//function clause execute (BTYPE(imm, rs2, rs1, op)) = { +// let rs1_val = X(rs1); +// let rs2_val = X(rs2); +// let taken : bool = match op { +// RISCV_BEQ => rs1_val == rs2_val, +// RISCV_BNE => rs1_val != rs2_val, +// RISCV_BLT => rs1_val <_s rs2_val, +// RISCV_BGE => rs1_val >=_s rs2_val, +// RISCV_BLTU => rs1_val <_u rs2_val, +// RISCV_BGEU => rs1_val >=_u rs2_val +// }; +// let t : xlenbits = PC + EXTS(imm); +// if taken then { +// /* Extensions get the first checks on the prospective target address. */ +// match ext_control_check_pc(t) { +// Ext_ControlAddr_Error(e) => { +// assert(false); +// RETIRE_FAIL +// }, +// Ext_ControlAddr_OK(target) => { +// if bit_to_bool(target[1]) & (~ (haveRVC())) then { +// handle_mem_exception(target, E_Fetch_Addr_Align()); +// RETIRE_FAIL; +// } else { +// set_next_pc(target); +// RETIRE_SUCCESS +// } +// } +// } +// } else RETIRE_SUCCESS +//} + +/* ****************************************************************** */ +union clause ast = ITYPE : (bits(12), regidx, regidx, iop) + +mapping encdec_iop : iop <-> bits(3) = { + RISCV_ADDI <-> 0b000, + RISCV_SLTI <-> 0b010, + RISCV_SLTIU <-> 0b011, + RISCV_ANDI <-> 0b111, + RISCV_ORI <-> 0b110, + RISCV_XORI <-> 0b100 +} + +mapping clause encdec = ITYPE(imm, rs1, rd, op) + <-> imm @ rs1 @ encdec_iop(op) @ rd @ 0b0010011 + +function clause execute (ITYPE (imm, rs1, rd, op)) = { + let rs1_val = X(rs1); + let immext : xlenbits = EXTS(imm); + let result : xlenbits = match op { + RISCV_ADDI => rs1_val + immext, + RISCV_SLTI => EXTZ(bool_to_bits(rs1_val <_s immext)), + RISCV_SLTIU => EXTZ(bool_to_bits(rs1_val <_u immext)), + RISCV_ANDI => rs1_val & immext, + RISCV_ORI => rs1_val | immext, + RISCV_XORI => rs1_val ^ immext + }; + X(rd) = result; + RETIRE_SUCCESS +} + +mapping itype_mnemonic : iop <-> string = { + RISCV_ADDI <-> "addi", + RISCV_SLTI <-> "slti", + RISCV_SLTIU <-> "sltiu", + RISCV_XORI <-> "xori", + RISCV_ORI <-> "ori", + RISCV_ANDI <-> "andi" +} + +/* ****************************************************************** */ +union clause ast = LOAD : (bits(12), regidx, regidx, bool, word_width, bool, bool) + +/* unsigned loads are only present for widths strictly less than xlen, + signed loads also present for widths equal to xlen */ +mapping clause encdec = LOAD(imm, rs1, rd, is_unsigned, size, false, false) if (word_width_bytes(size) < sizeof(xlen_bytes)) | (not_bool(is_unsigned) & word_width_bytes(size) <= sizeof(xlen_bytes)) + <-> imm @ rs1 @ bool_bits(is_unsigned) @ size_bits(size) @ rd @ 0b0000011 if (word_width_bytes(size) < sizeof(xlen_bytes)) | (not_bool(is_unsigned) & word_width_bytes(size) <= sizeof(xlen_bytes)) + +val extend_value : forall 'n, 0 < 'n <= xlen_bytes. (bool, MemoryOpResult(bits(8 * 'n))) -> MemoryOpResult(xlenbits) +function extend_value(is_unsigned, value) = match (value) { + MemValue(v) => MemValue(if is_unsigned then EXTZ(v) else EXTS(v) : xlenbits), + 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} +function process_load(rd, addr, value, is_unsigned) = + match extend_value(is_unsigned, value) { + MemValue(result) => { X(rd) = result; RETIRE_SUCCESS }, + MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL } + } + +function check_misaligned(vaddr : xlenbits, width : word_width) -> bool = + if plat_enable_misaligned_access() then false + else match width { + BYTE => false, + HALF => vaddr[0] == bitone, + WORD => vaddr[0] == bitone | vaddr[1] == bitone, + DOUBLE => vaddr[0] == bitone | vaddr[1] == bitone | vaddr[2] == bitone + } + +function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = { + let offset : xlenbits = EXTS(imm); + /* Get the address, X(rs1) + offset. + Some extensions perform additional checks on address validity. */ + match ext_data_get_addr(rs1, offset, Read(Data), width) { + Ext_DataAddr_Error(e) => { assert(false); RETIRE_FAIL }, + Ext_DataAddr_OK(vaddr) => + if check_misaligned(vaddr, width) + then { handle_mem_exception(vaddr, E_Load_Addr_Align()); RETIRE_FAIL } + else match translateAddr(vaddr, Read(Data)) { + TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + TR_Address(addr, _) => + match (width, sizeof(xlen)) { + (BYTE, _) => + process_load(rd, vaddr, mem_read(Read(Data), addr, 1, aq, rl, false), is_unsigned), + (HALF, _) => + process_load(rd, vaddr, mem_read(Read(Data), addr, 2, aq, rl, false), is_unsigned), + (WORD, _) => + process_load(rd, vaddr, mem_read(Read(Data), addr, 4, aq, rl, false), is_unsigned), + (DOUBLE, 64) => + process_load(rd, vaddr, mem_read(Read(Data), addr, 8, aq, rl, false), is_unsigned) + } + } + } +} + +/* ****************************************************************** */ +union clause ast = STORE : (bits(12), regidx, regidx, word_width, bool, bool) + +mapping clause encdec = STORE(imm7 @ imm5, rs2, rs1, size, false, false) if word_width_bytes(size) <= sizeof(xlen_bytes) + <-> imm7 : bits(7) @ rs2 @ rs1 @ 0b0 @ size_bits(size) @ imm5 : bits(5) @ 0b0100011 if word_width_bytes(size) <= sizeof(xlen_bytes) + +/* NOTE: Currently, we only EA if address translation is successful. + This may need revisiting. */ +function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = { + let offset : xlenbits = EXTS(imm); + /* Get the address, X(rs1) + offset. + Some extensions perform additional checks on address validity. */ + match ext_data_get_addr(rs1, offset, Write(Data), width) { + Ext_DataAddr_Error(e) => { assert (false); RETIRE_FAIL }, + Ext_DataAddr_OK(vaddr) => + if check_misaligned(vaddr, width) + then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); RETIRE_FAIL } + else match translateAddr(vaddr, Write(Data)) { + TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + TR_Address(addr, _) => { + let eares : MemoryOpResult(unit) = match width { + BYTE => mem_write_ea(addr, 1, aq, rl, false), + HALF => mem_write_ea(addr, 2, aq, rl, false), + WORD => mem_write_ea(addr, 4, aq, rl, false), + DOUBLE => mem_write_ea(addr, 8, aq, rl, false) + }; + match (eares) { + MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL }, + MemValue(_) => { + let rs2_val = X(rs2); + let res : MemoryOpResult(bool) = match (width, sizeof(xlen)) { + (BYTE, _) => mem_write_value(addr, 1, rs2_val[7..0], aq, rl, false), + (HALF, _) => mem_write_value(addr, 2, rs2_val[15..0], aq, rl, false), + (WORD, _) => mem_write_value(addr, 4, rs2_val[31..0], aq, rl, false), + (DOUBLE, 64) => mem_write_value(addr, 8, rs2_val, aq, rl, false) + }; + match (res) { + MemValue(true) => RETIRE_SUCCESS, + MemValue(false) => internal_error("store got false from mem_write_value"), + MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL } + } + } + } + } + } + } +} + +/* Put the illegal instructions last to use their wildcard match. */ + +/* ****************************************************************** */ + +union clause ast = ILLEGAL : word + +mapping clause encdec = ILLEGAL(s) <-> s + +function clause execute (ILLEGAL(s)) = { handle_illegal(); RETIRE_FAIL } + +/* ****************************************************************** */ + +/* End definitions */ +end ast +end execute +end encdec +end encdec_compressed + +val decode : bits(32) -> ast effect pure +function decode bv = encdec(bv) + +/* The result of a fetch, which includes any possible error + * from an extension that interposes on the fetch operation. + */ + +union FetchResult = { + F_Ext_Error : ext_fetch_addr_error, /* For extensions */ + F_Base : word, /* Base ISA */ + F_RVC : half, /* Compressed ISA */ + F_Error : (ExceptionType, xlenbits) /* standard exception and PC */ +} +/* The default implementation of hooks for the step() and main() functions. */ + +function ext_init() -> unit = () + +function ext_fetch_hook(f : FetchResult) -> FetchResult = f + +function ext_pre_step_hook() -> unit = () +function ext_post_step_hook() -> unit = () +/* Extensions may wish to interpose and transform decoded instructions, + * based on other machine state. This is supported via a post-decode + * instruction hook, the default implementation of which is provided below. + */ + +val ext_post_decode_hook : ast -> ast effect {rreg} +function ext_post_decode_hook(x) = x + +val fetch : unit -> FetchResult effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg} +function fetch() -> FetchResult = + /* fetch PC check for extensions: extensions return a transformed PC to fetch, + * but any exceptions use the untransformed PC. + */ + match ext_fetch_check_pc(PC, PC) { + Ext_FetchAddr_Error(e) => F_Ext_Error(e), + Ext_FetchAddr_OK(use_pc) => { + if (use_pc[0] != bitzero | (use_pc[1] != bitzero)) + then F_Error(E_Fetch_Addr_Align(), PC) + else match translateAddr(use_pc, Execute()) { + TR_Failure(e, _) => F_Error(e, PC), + TR_Address(ppc, _) => { + match mem_read(Execute(), ppc, 4, false, false, false) { + MemException(e) => F_Error(e, PC), + MemValue(ibits) => F_Base(ibits) + } + } + } + } + } + +/* The emulator fetch-execute-interrupt dispatch loop. */ + +/* returns whether to increment the step count in the trace */ +function step(step_no : int) -> bool = { + /* for step extensions */ + ext_pre_step_hook(); + + let (retired, stepped) : (Retired, bool) = + /* the extension hook interposes on the fetch result */ + let f : FetchResult = ext_fetch_hook(fetch()) in + match f { + /* extension error */ + F_Ext_Error(e) => { + ext_handle_fetch_check_error(e); + (RETIRE_FAIL, false) + }, + /* standard error */ + F_Error(e, addr) => { + handle_mem_exception(addr, e); + (RETIRE_FAIL, false) + }, + F_Base(w) => { + let ast = decode(w); + nextPC = PC + 4; + (execute(ext_post_decode_hook(ast)), true) + } + }; + + tick_pc(); + + /* for step extensions */ + ext_post_step_hook(); + + stepped +} + +function loop () : unit -> unit = { + step_no : int = 0; + while (true) do { + let stepped = step(step_no); + if stepped then step_no = step_no + 1; + } +} + + +function main () : unit -> unit = { + // PC = __GetSlice_int(64, elf_entry(), 0); + PC = sail_zero_extend(0x1000, sizeof(xlen)); + print_bits("PC = ", PC); + + try { + loop() + } catch { + Error_not_implemented(s) => print_string("Error: Not implemented: ", s), + Error_internal_error() => print("Error: internal error") + } +} diff --git a/model/riscv_mem.sail b/model/riscv_mem.sail index d02c49d..b3fa37d 100644 --- a/model/riscv_mem.sail +++ b/model/riscv_mem.sail @@ -7,7 +7,7 @@ * metadata in addition to raw memory data. * * The external API for this module is - * {mem_read, mem_write_ea, mem_write_value_meta, mem_write_value} + * {mem_read, mem_read_meta, mem_write_ea, mem_write_value_meta, mem_write_value} * where mem_write_value is a special case of mem_write_value_meta that uses * a default value of the metadata. * @@ -19,43 +19,53 @@ function is_aligned_addr forall 'n. (addr : xlenbits, width : atom('n)) -> bool = unsigned(addr) % width == 0 -// 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) -> MemoryOpResult(bits(8 * 'n)) = { - let result = (match (aq, rl, res) { - (false, false, false) => Some(read_ram(Read_plain, paddr, width)), - (true, false, false) => Some(read_ram(Read_RISCV_acquire, paddr, width)), - (true, true, false) => Some(read_ram(Read_RISCV_strong_acquire, paddr, width)), - (false, false, true) => Some(read_ram(Read_RISCV_reserved, paddr, width)), - (true, false, true) => Some(read_ram(Read_RISCV_reserved_acquire, paddr, width)), - (true, true, true) => Some(read_ram(Read_RISCV_reserved_strong_acquire, paddr, width)), +function read_kind_of_flags (aq : bool, rl : bool, res : bool) -> option(read_kind) = + match (aq, rl, res) { + (false, false, false) => Some(Read_plain), + (true, false, false) => Some(Read_RISCV_acquire), + (true, true, false) => Some(Read_RISCV_strong_acquire), + (false, false, true) => Some(Read_RISCV_reserved), + (true, false, true) => Some(Read_RISCV_reserved_acquire), + (true, true, true) => Some(Read_RISCV_reserved_strong_acquire), (false, true, false) => None(), /* should these be instead throwing error_not_implemented as below? */ (false, true, true) => None() - }) : option(bits(8 * 'n)); + } + +// 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)) = { + let result = (match read_kind_of_flags(aq, rl, res) { + Some(rk) => Some(read_ram(rk, paddr, width, meta)), + None() => None() + }) : option((bits(8 * 'n), mem_meta)); match (t, result) { (Execute(), None()) => MemException(E_Fetch_Access_Fault()), (Read(Data), None()) => MemException(E_Load_Access_Fault()), (_, None()) => MemException(E_SAMO_Access_Fault()), - (_, Some(v)) => { if get_config_print_mem() + (_, Some(v, m)) => { if get_config_print_mem() then print_mem("mem[" ^ to_str(t) ^ "," ^ BitStr(paddr) ^ "] -> " ^ BitStr(v)); - MemValue(v) } + MemValue(v, m) } } } /* 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) -> MemoryOpResult(bits(8 * 'n)) = +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)) = if within_mmio_readable(paddr, width) - then mmio_read(paddr, width) + then MemoryOpResult_add_meta(mmio_read(t, paddr, width), default_meta) else if within_phys_mem(paddr, width) - then phys_mem_read(t, paddr, width, aq, rl, res) - else MemException(E_Load_Access_Fault()) + then phys_mem_read(t, paddr, width, aq, rl, res, meta) + else match t { + Execute() => MemException(E_Fetch_Access_Fault()), + Read(Data) => MemException(E_Load_Access_Fault()), + _ => MemException(E_SAMO_Access_Fault()) + } /* PMP checks if enabled */ -function pmp_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) -> MemoryOpResult(bits(8 * 'n)) = +function pmp_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)) = if (~ (plat_enable_pmp ())) - then checked_mem_read(t, paddr, width, aq, rl, res) + then checked_mem_read(t, paddr, width, aq, rl, res, meta) else { match pmpCheck(paddr, width, t, effectivePrivilege(mstatus, cur_privilege)) { - None() => checked_mem_read(t, paddr, width, aq, rl, res), + None() => checked_mem_read(t, paddr, width, aq, rl, res, meta), Some(e) => MemException(e) } } @@ -70,7 +80,8 @@ function rvfi_read (addr, width, result) = { MemValue(v) => if width <= 8 then { rvfi_exec->rvfi_mem_rdata() = sail_zero_extend(v,64); rvfi_exec->rvfi_mem_rmask() = rvfi_encode_width_mask(width) } - else (), + else { rvfi_exec->rvfi_mem_rdata() = v[63..0]; + rvfi_exec->rvfi_mem_rmask() = 0xFF}, MemException(_) => () }; } @@ -81,24 +92,29 @@ $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, 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)) 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} $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, 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)) 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} $endif -function mem_read (typ, paddr, width, aq, rl, res) = { - let result : MemoryOpResult(bits(8 * 'n)) = - if (aq | res) & (~ (is_aligned_addr(paddr, width))) - then MemException(E_Load_Addr_Align()) - else match (aq, rl, res) { - (false, true, false) => throw(Error_not_implemented("load.rl")), - (false, true, true) => throw(Error_not_implemented("lr.rl")), - (_, _, _) => pmp_mem_read(typ, paddr, width, aq, rl, res) - }; - rvfi_read(paddr, width, result); - result +function mem_read_meta (typ, paddr, width, aq, rl, res, meta) = { + let result : MemoryOpResult((bits(8 * 'n), mem_meta)) = + if (aq | res) & (~ (is_aligned_addr(paddr, width))) + then MemException(E_Load_Addr_Align()) + else match (aq, rl, res) { + (false, true, false) => throw(Error_not_implemented("load.rl")), + (false, true, true) => throw(Error_not_implemented("lr.rl")), + (_, _, _) => pmp_mem_read(typ, paddr, width, aq, rl, res, meta) + }; + rvfi_read(paddr, width, MemoryOpResult_drop_meta(result)); + result } +function mem_read (typ, paddr, width, aq, rl, res) = + MemoryOpResult_drop_meta(mem_read_meta(typ, paddr, width, aq, rl, res, false)) + val mem_write_ea : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(unit) effect {eamem, escape} function mem_write_ea (addr, width, aq, rl, con) = { @@ -123,6 +139,9 @@ function rvfi_write (addr, width, value) = { if width <= 8 then { rvfi_exec->rvfi_mem_wdata() = sail_zero_extend(value,64); rvfi_exec->rvfi_mem_wmask() = rvfi_encode_width_mask(width); + } else { + rvfi_exec->rvfi_mem_wdata() = value[63..0]; + rvfi_exec->rvfi_mem_wmask() = 0xFF; } } $else diff --git a/model/riscv_platform.sail b/model/riscv_platform.sail index 7cc63cc..7e07cf1 100644 --- a/model/riscv_platform.sail +++ b/model/riscv_platform.sail @@ -142,8 +142,8 @@ let MTIMECMP_BASE_HI : xlenbits = EXTZ(0x04004) let MTIME_BASE : xlenbits = EXTZ(0x0bff8) let MTIME_BASE_HI : xlenbits = EXTZ(0x0bffc) -val clint_load : forall 'n, 'n > 0. (xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rreg} -function clint_load(addr, width) = { +val clint_load : forall 'n, 'n > 0. (AccessType(ext_access_type), xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rreg} +function clint_load(t, addr, width) = { let addr = addr - plat_clint_base (); /* FIXME: For now, only allow exact aligned access. */ if addr == MSIP_BASE & ('n == 8 | 'n == 4) @@ -194,7 +194,11 @@ function clint_load(addr, width) = { else { if get_config_print_platform() then print_platform("clint[" ^ BitStr(addr) ^ "] -> <not-mapped>"); - MemException(E_Load_Access_Fault()) + match t { + Execute() => MemException(E_Fetch_Access_Fault()), + Read(Data) => MemException(E_Load_Access_Fault()), + _ => MemException(E_SAMO_Access_Fault()) + } } } @@ -274,8 +278,8 @@ register htif_exit_code : bits(64) * dispatched the address. */ -val htif_load : forall 'n, 'n > 0. (xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rreg} -function htif_load(paddr, width) = { +val htif_load : forall 'n, 'n > 0. (AccessType(ext_access_type), xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rreg} +function htif_load(t, paddr, width) = { if get_config_print_platform() then print_platform("htif[" ^ BitStr(paddr) ^ "] -> " ^ BitStr(htif_tohost)); /* FIXME: For now, only allow the expected access widths. */ @@ -285,7 +289,11 @@ function htif_load(paddr, width) = { then MemValue(sail_zero_extend(htif_tohost[31..0], 32)) /* FIXME: Redundant zero_extend currently required by Lem backend */ else if width == 4 & paddr == plat_htif_tohost() + 4 then MemValue(sail_zero_extend(htif_tohost[63..32], 32)) /* FIXME: Redundant zero_extend currently required by Lem backend */ - else MemException(E_Load_Access_Fault()) + else match t { + Execute() => MemException(E_Fetch_Access_Fault()), + Read(Data) => MemException(E_Load_Access_Fault()), + _ => MemException(E_SAMO_Access_Fault()) + } } /* The rreg,wreg effects are an artifact of using 'register' to implement device state. */ @@ -351,12 +359,16 @@ $else function within_mmio_writable forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : atom('n)) -> bool = false $endif -function mmio_read forall 'n, 0 < 'n <= max_mem_access . (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 : atom('n)) -> MemoryOpResult(bits(8 * 'n)) = if within_clint(paddr, width) - then clint_load(paddr, width) + then clint_load(t, paddr, width) else if within_htif_readable(paddr, width) & (1 <= 'n) - then htif_load(paddr, width) - else MemException(E_Load_Access_Fault()) + then htif_load(t, paddr, width) + else match t { + Execute() => MemException(E_Fetch_Access_Fault()), + Read(Data) => MemException(E_Load_Access_Fault()), + _ => 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) = if within_clint(paddr, width) diff --git a/model/riscv_pmp_control.sail b/model/riscv_pmp_control.sail index 4f43a6c..1970afc 100644 --- a/model/riscv_pmp_control.sail +++ b/model/riscv_pmp_control.sail @@ -40,7 +40,7 @@ function pmpCheckRWX(ent, acc) = { val pmpCheckPerms: (Pmpcfg_ent, AccessType(ext_access_type), Privilege) -> bool function pmpCheckPerms(ent, acc, priv) = { match priv { - Machine => if ent.L() == 0b1 + Machine => if pmpLocked(ent) then pmpCheckRWX(ent, acc) else true, _ => pmpCheckRWX(ent, acc) diff --git a/model/riscv_pmp_regs.sail b/model/riscv_pmp_regs.sail index 978ef18..a823a06 100644 --- a/model/riscv_pmp_regs.sail +++ b/model/riscv_pmp_regs.sail @@ -85,9 +85,15 @@ function pmpReadCfgReg(n) = { } } -/* Helper to handle locked entries */ +/* Helpers to handle locked entries */ +function pmpLocked(cfg: Pmpcfg_ent) -> bool = + cfg.L() == 0b1 + +function pmpTORLocked(cfg: Pmpcfg_ent) -> bool = + (cfg.L() == 0b1) & (pmpAddrMatchType_of_bits(cfg.A()) == TOR) + function pmpWriteCfg(cfg: Pmpcfg_ent, v: bits(8)) -> Pmpcfg_ent = - if cfg.L() == 0b1 then cfg else Mk_Pmpcfg_ent(v) + if pmpLocked(cfg) then cfg else Mk_Pmpcfg_ent(v) val pmpWriteCfgReg : forall 'n, 0 <= 'n < 4 . (atom('n), xlenbits) -> unit effect {rreg, wreg} function pmpWriteCfgReg(n, v) = { @@ -137,7 +143,7 @@ function pmpWriteCfgReg(n, v) = { } } -function pmpWriteAddr(cfg: Pmpcfg_ent, reg: xlenbits, v: xlenbits) -> xlenbits = +function pmpWriteAddr(locked: bool, tor_locked: bool, reg: xlenbits, v: xlenbits) -> xlenbits = if sizeof(xlen) == 32 - then { if cfg.L() == 0b1 then reg else v } - else { if cfg.L() == 0b1 then reg else EXTZ(v[53..0]) } + then { if (locked | tor_locked) then reg else v } + else { if (locked | tor_locked) then reg else EXTZ(v[53..0]) } diff --git a/model/riscv_softfloat_interface.sail b/model/riscv_softfloat_interface.sail new file mode 100644 index 0000000..1cc16a9 --- /dev/null +++ b/model/riscv_softfloat_interface.sail @@ -0,0 +1,260 @@ +/* **************************************************************** */ +/* This file lists all the external Berkeley softfloat functions */ +/* invoked from the SAIL spec for RISC-V F and D extensions */ +/* (in: riscv_insts_fdext.sail) */ +/* */ +/* Each of these functions corresponds to one in 'SoftFloat.hs' */ +/* in https://github.com/GaloisInc/softfloat-hs.git */ +/* written by Ben Selfridge, */ +/* which is a set of pure-functional Haskell wrappers on the */ +/* Berkely softfloat C library written by John Hauser. */ + +/* For now, the bodies of all these functions are placeholders */ +/* while we develop riscv_insts_fdext.sail */ +/* They should be replaced with external calls to Berkeley softfloat*/ +/* functions in a similar manner to the Haskell softfloat wrappers. */ + +/* **************************************************************** */ +/* All arguments and results have one of these types */ + +type bits_rm = bits(3) /* Rounding mode */ +type bits_fflags = bits(5) /* Accrued exceptions: NV,DZ,OF,UF,NX */ +type bits_S = bits(32) /* Single-precision float value */ +type bits_D = bits(64) /* Double-precision float value */ + +type bits_W = bits(32) /* Signed integer */ +type bits_WU = bits(32) /* Unsigned integer */ + +type bits_L = bits(64) /* Signed integer */ +type bits_LU = bits(64) /* Unsigned integer */ + +/* ***************************************************************** */ +/* Internal registers to pass results across the softfloat interface + * to avoid return types involving structures. + */ +register float_result : bits(64) +register float_fflags : bits(64) + +/* **************************************************************** */ +/* ADD/SUB/MUL/DIV */ + +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} +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} +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} +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} +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} +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} +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} +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} +function riscv_f64Div (rm, v1, v2) = { + extern_f64Div(rm, v1, v2); + (float_fflags[4 .. 0], float_result) +} + +/* **************************************************************** */ +/* MULTIPLY-ADD */ + +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} +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} +function riscv_f64MulAdd (rm, v1, v2, v3) = { + extern_f64MulAdd(rm, v1, v2, v3); + (float_fflags[4 .. 0], float_result) +} + +/* **************************************************************** */ +/* SQUARE ROOT */ + +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} +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} +function riscv_f64Sqrt (rm, v) = { + extern_f64Sqrt(rm, v); + (float_fflags[4 .. 0], float_result) +} + +/* **************************************************************** */ +/* CONVERSIONS */ + +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} +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} +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} +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} +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} +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} +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} +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} +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} +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} +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} +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} +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} +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} +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} +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} +function riscv_ui64ToF64 (rm, v) = { + extern_ui64ToF64(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} +function riscv_f32ToF64 (rm, v) = { + extern_f32ToF64(rm, v); + (float_fflags[4 .. 0], float_result) +} + +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} +function riscv_f64ToF32 (rm, v) = { + extern_f64ToF32(rm, v); + (float_fflags[4 .. 0], float_result[31 .. 0]) +} + +/* **************************************************************** */ diff --git a/model/riscv_step_rvfi.sail b/model/riscv_step_rvfi.sail index 0ab482a..dd24365 100644 --- a/model/riscv_step_rvfi.sail +++ b/model/riscv_step_rvfi.sail @@ -12,6 +12,7 @@ function ext_post_step_hook() -> unit = { val ext_init : unit -> unit effect {wreg} function ext_init() = { init_base_regs(); + init_fdext_regs(); /* these are here so that the C backend doesn't prune them out. */ rvfi_set_instr_packet(0x0000000000000000); print_bits("", rvfi_get_cmd()); diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index 8162cb8..d906f5e 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -454,6 +454,14 @@ function init_sys() -> unit = { misa->U() = 0b1; /* user-mode */ misa->S() = 0b1; /* supervisor-mode */ + /* On RV64, we currently support either both F and D, or neither. + * On RV32, we currently only support F. + */ + misa->F() = bool_to_bits(sys_enable_fdext()); /* single-precision */ + misa->D() = if sizeof(xlen) == 64 + then bool_to_bits(sys_enable_fdext()) /* double-precision */ + else 0b0; + mstatus = set_mstatus_SXL(mstatus, misa.MXL()); mstatus = set_mstatus_UXL(mstatus, misa.MXL()); mstatus->SD() = 0b0; @@ -489,3 +497,15 @@ union MemoryOpResult ('a : Type) = { MemValue : 'a, MemException : ExceptionType } + +val MemoryOpResult_add_meta : forall ('t : Type). (MemoryOpResult('t), mem_meta) -> MemoryOpResult(('t, mem_meta)) +function MemoryOpResult_add_meta(r, m) = match r { + MemValue(v) => MemValue(v, m), + MemException(e) => MemException(e) +} + +val MemoryOpResult_drop_meta : forall ('t : Type). MemoryOpResult(('t, mem_meta)) -> MemoryOpResult('t) +function MemoryOpResult_drop_meta(r) = match r { + MemValue(v, m) => MemValue(v), + MemException(e) => MemException(e) +} diff --git a/model/riscv_sys_exceptions.sail b/model/riscv_sys_exceptions.sail index 94d869e..fa693e8 100644 --- a/model/riscv_sys_exceptions.sail +++ b/model/riscv_sys_exceptions.sail @@ -2,6 +2,11 @@ type ext_exception = unit +/* Is XRET from given mode permitted by extension? */ +function ext_check_xret_priv (p : Privilege) : Privilege -> bool = true +/* Called if above check fails */ +function ext_fail_xret_priv () : unit -> unit = () + function handle_trap_extension(p : Privilege, pc : xlenbits, u : option(unit)) -> unit = () /* used for traps and ECALL */ diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 722c1d5..3b808a6 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -74,6 +74,8 @@ register misa : Misa val sys_enable_writable_misa = {c: "sys_enable_writable_misa", ocaml: "Platform.enable_writable_misa", _: "sys_enable_writable_misa"} : unit -> bool /* whether misa.c was enabled at boot */ val sys_enable_rvc = {c: "sys_enable_rvc", ocaml: "Platform.enable_rvc", _: "sys_enable_rvc"} : unit -> bool +/* whether misa.{f,d} were enabled at boot */ +val sys_enable_fdext = {c: "sys_enable_fdext", ocaml: "Platform.enable_fdext", _: "sys_enable_fdext"} : unit -> bool /* This function allows an extension to veto a write to Misa if it would violate an alignment restriction on @@ -101,6 +103,7 @@ function haveMulDiv() -> bool = misa.M() == 0b1 function haveSupMode() -> bool = misa.S() == 0b1 function haveUsrMode() -> bool = misa.U() == 0b1 function haveNExt() -> bool = misa.N() == 0b1 +/* see below for F and D extension tests */ bitfield Mstatus : xlenbits = { SD : xlen - 1, @@ -177,7 +180,6 @@ function legalize_mstatus(o : Mstatus, v : xlenbits) -> Mstatus = { * to support code running in S/U-modes. Spike does this, and for now, we match it. * FIXME: This should be made a platform parameter. */ - // let m = update_FS(m, extStatus_to_bits(Off)); let dirty = extStatus_of_bits(m.FS()) == Dirty | extStatus_of_bits(m.XS()) == Dirty; let m = update_SD(m, bool_to_bits(dirty)); @@ -213,6 +215,10 @@ function in32BitMode() -> bool = { cur_Architecture() == RV32 } +/* F and D extensions have to enabled both via misa.{FD} as well as mstatus.FS */ +function haveFExt() -> bool = (misa.F() == 0b1) & (mstatus.FS() != 0b00) +function haveDExt() -> bool = (misa.D() == 0b1) & (mstatus.FS() != 0b00) + /* interrupt processing state */ bitfield Minterrupts : xlenbits = { diff --git a/model/riscv_termination_rv32.sail b/model/riscv_termination_rv32.sail index 7cf8cb8..7318421 100644 --- a/model/riscv_termination_rv32.sail +++ b/model/riscv_termination_rv32.sail @@ -1 +1 @@ -termination_measure walk32(_,_,_,_,_,_,level,_) = level +termination_measure walk32(_,_,_,_,_,_,level,_,_) = level diff --git a/model/riscv_types.sail b/model/riscv_types.sail index cacf0db..987743a 100644 --- a/model/riscv_types.sail +++ b/model/riscv_types.sail @@ -108,8 +108,6 @@ enum word_width = {BYTE, HALF, WORD, DOUBLE} /* architectural interrupt definitions */ -type exc_code = bits(8) - enum InterruptType = { I_U_Software, I_S_Software, @@ -181,7 +179,7 @@ function exceptionType_to_bits(e) = E_SAMO_Page_Fault() => 0x0f, /* extensions */ - E_Extension(e) => 0x18 /* First code for a custom extension */ + E_Extension(e) => ext_exc_type_to_bits(e) } val num_of_ExceptionType : ExceptionType -> {'n, (0 <= 'n < xlen). int('n)} @@ -205,7 +203,7 @@ function num_of_ExceptionType(e) = E_SAMO_Page_Fault() => 15, /* extensions */ - E_Extension(e) => 24 /* First code for a custom extension */ + E_Extension(e) => num_of_ext_exc_type(e) } @@ -230,7 +228,7 @@ function exceptionType_to_str(e) = E_SAMO_Page_Fault() => "store/amo-page-fault", /* extensions */ - E_Extension(e) => "extension-exception" + E_Extension(e) => ext_exc_type_to_str(e) } overload to_str = {exceptionType_to_str} diff --git a/model/riscv_types_common.sail b/model/riscv_types_common.sail new file mode 100644 index 0000000..9db34a0 --- /dev/null +++ b/model/riscv_types_common.sail @@ -0,0 +1 @@ +type exc_code = bits(8) diff --git a/model/riscv_types_ext.sail b/model/riscv_types_ext.sail index 5a05c39..6562981 100644 --- a/model/riscv_types_ext.sail +++ b/model/riscv_types_ext.sail @@ -20,3 +20,15 @@ type ext_exc_type = unit /* No exception extensions */ /* Default translation of PTW errors into exception annotations */ function ext_translate_exception(e : ext_ptw_error) -> ext_exc_type = e + +/* Default conversion of extension exceptions to bits */ +val ext_exc_type_to_bits : ext_exc_type -> exc_code +function ext_exc_type_to_bits(e) = 0x18 /* First code for a custom extension */ + +/* Default conversion of extension exceptions to integers */ +val num_of_ext_exc_type : ext_exc_type -> {'n, (0 <= 'n < xlen). int('n)} +function num_of_ext_exc_type(e) = 24 /* First code for a custom extension */ + +/* Default conversion of extension exceptions to strings */ +val ext_exc_type_to_str : ext_exc_type -> string +function ext_exc_type_to_str(e) = "extension-exception" diff --git a/model/riscv_vmem_rv32.sail b/model/riscv_vmem_rv32.sail index 4ff7891..bea786c 100644 --- a/model/riscv_vmem_rv32.sail +++ b/model/riscv_vmem_rv32.sail @@ -26,7 +26,7 @@ function translationMode(priv) = { /* Top-level address translation dispatcher */ -val translateAddr : (xlenbits, AccessType(ext_access_type)) -> TR_Result(xlenbits, ExceptionType) effect {escape, rmem, rreg, wmv, wmvt, wreg} +val translateAddr : (xlenbits, AccessType(ext_access_type)) -> TR_Result(xlenbits, ExceptionType) effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg} function translateAddr(vAddr, ac) = { let effPriv : Privilege = match ac { Execute() => cur_privilege, diff --git a/model/riscv_vmem_rv64.sail b/model/riscv_vmem_rv64.sail index c55e9dc..8b7dc44 100644 --- a/model/riscv_vmem_rv64.sail +++ b/model/riscv_vmem_rv64.sail @@ -33,7 +33,7 @@ function translationMode(priv) = { /* Top-level address translation dispatcher */ -val translateAddr : (xlenbits, AccessType(ext_access_type)) -> TR_Result(xlenbits, ExceptionType) effect {escape, rmem, rreg, wmv, wmvt, wreg} +val translateAddr : (xlenbits, AccessType(ext_access_type)) -> TR_Result(xlenbits, ExceptionType) effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg} function translateAddr(vAddr, ac) = { let effPriv : Privilege = match ac { Execute() => cur_privilege, diff --git a/model/riscv_vmem_sv32.sail b/model/riscv_vmem_sv32.sail index e535915..1a27072 100644 --- a/model/riscv_vmem_sv32.sail +++ b/model/riscv_vmem_sv32.sail @@ -6,7 +6,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, rreg, escape} +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} function walk32(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { let va = Mk_SV32_Vaddr(vaddr); let pt_ofs : paddr32 = shiftl(EXTZ(shiftr(va.VPNi(), (level * SV32_LEVEL_BITS))[(SV32_LEVEL_BITS - 1) .. 0]), @@ -37,13 +37,13 @@ function walk32(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { PTW_Failure(PTW_Invalid_PTE(), ext_ptw) } else { if isPTEPtr(pbits, ext_pte) then { - if level == 0 then { + if level > 0 then { + /* walk down the pointer to the next level */ + walk32(vaddr, ac, priv, mxr, do_sum, shiftl(EXTZ(pte.PPNi()), PAGESIZE_BITS), level - 1, is_global, ext_ptw) + } else { /* last-level PTE contains a pointer instead of a leaf */ /* print("walk32: last-level pte contains a ptr"); */ PTW_Failure(PTW_Invalid_PTE(), ext_ptw) - } else { - /* walk down the pointer to the next level */ - walk32(vaddr, ac, priv, mxr, do_sum, shiftl(EXTZ(pte.PPNi()), PAGESIZE_BITS), level - 1, is_global, ext_ptw) } } else { /* leaf PTE */ match checkPTEPermission(ac, priv, mxr, do_sum, pattr, ext_pte, ext_ptw) { @@ -115,7 +115,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} +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} 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 a1edc4e..37c98a2 100644 --- a/model/riscv_vmem_sv39.sail +++ b/model/riscv_vmem_sv39.sail @@ -1,6 +1,6 @@ /* 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, rreg, escape} +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} function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { let va = Mk_SV39_Vaddr(vaddr); let pt_ofs : paddr64 = shiftl(EXTZ(shiftr(va.VPNi(), (level * SV39_LEVEL_BITS))[(SV39_LEVEL_BITS - 1) .. 0]), @@ -31,13 +31,13 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { PTW_Failure(PTW_Invalid_PTE(), ext_ptw) } else { if isPTEPtr(pbits, ext_pte) then { - if level == 0 then { + if level > 0 then { + /* walk down the pointer to the next level */ + walk39(vaddr, ac, priv, mxr, do_sum, shiftl(EXTZ(pte.PPNi()), PAGESIZE_BITS), level - 1, is_global, ext_ptw) + } else { /* last-level PTE contains a pointer instead of a leaf */ /* print("walk39: last-level pte contains a ptr"); */ PTW_Failure(PTW_Invalid_PTE(), ext_ptw) - } else { - /* walk down the pointer to the next level */ - walk39(vaddr, ac, priv, mxr, do_sum, shiftl(EXTZ(pte.PPNi()), PAGESIZE_BITS), level - 1, is_global, ext_ptw) } } else { /* leaf PTE */ match checkPTEPermission(ac, priv, mxr, do_sum, pattr, ext_pte, ext_ptw) { @@ -109,7 +109,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} +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} 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 6bfeea4..36304cf 100644 --- a/model/riscv_vmem_sv48.sail +++ b/model/riscv_vmem_sv48.sail @@ -1,6 +1,6 @@ /* 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, rreg, escape} +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} function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { let va = Mk_SV48_Vaddr(vaddr); let pt_ofs : paddr64 = shiftl(EXTZ(shiftr(va.VPNi(), (level * SV48_LEVEL_BITS))[(SV48_LEVEL_BITS - 1) .. 0]), @@ -31,13 +31,13 @@ function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { PTW_Failure(PTW_Invalid_PTE(), ext_ptw) } else { if isPTEPtr(pbits, ext_pte) then { - if level == 0 then { + if level > 0 then { + /* walk down the pointer to the next level */ + walk48(vaddr, ac, priv, mxr, do_sum, shiftl(EXTZ(pte.PPNi()), PAGESIZE_BITS), level - 1, is_global, ext_ptw) + } else { /* last-level PTE contains a pointer instead of a leaf */ /* print("walk48: last-level pte contains a ptr"); */ PTW_Failure(PTW_Invalid_PTE(), ext_ptw) - } else { - /* walk down the pointer to the next level */ - walk48(vaddr, ac, priv, mxr, do_sum, shiftl(EXTZ(pte.PPNi()), PAGESIZE_BITS), level - 1, is_global, ext_ptw) } } else { /* leaf PTE */ match checkPTEPermission(ac, priv, mxr, do_sum, pattr, ext_pte, ext_ptw) { @@ -109,7 +109,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} +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} 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), |