From a39a1ac64e8e716c5bb588f11809dec661ae0f1d Mon Sep 17 00:00:00 2001 From: Alasdair Date: Fri, 1 Mar 2024 19:57:18 +0000 Subject: Add read-only CSR MCONFIGPTR CSR MCONFIGPTR is defined in RISCV priv spec 1.12 but is missing from the RISC-V SAIL model. This commit adds the read-only CSR MCONFIGPTR. Co-authored-by: Dan Smathers --- model/riscv_csr_map.sail | 1 + model/riscv_insts_zicsr.sail | 1 + model/riscv_sys_control.sail | 2 ++ model/riscv_sys_regs.sail | 1 + 4 files changed, 5 insertions(+) (limited to 'model') diff --git a/model/riscv_csr_map.sail b/model/riscv_csr_map.sail index 9e3e804..22cffd5 100644 --- a/model/riscv_csr_map.sail +++ b/model/riscv_csr_map.sail @@ -58,6 +58,7 @@ mapping clause csr_name_map = 0xF11 <-> "mvendorid" mapping clause csr_name_map = 0xF12 <-> "marchid" mapping clause csr_name_map = 0xF13 <-> "mimpid" mapping clause csr_name_map = 0xF14 <-> "mhartid" +mapping clause csr_name_map = 0xF15 <-> "mconfigptr" /* machine trap setup */ mapping clause csr_name_map = 0x300 <-> "mstatus" mapping clause csr_name_map = 0x301 <-> "misa" diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail index d106ad2..7c52abd 100644 --- a/model/riscv_insts_zicsr.sail +++ b/model/riscv_insts_zicsr.sail @@ -29,6 +29,7 @@ function readCSR csr : csreg -> xlenbits = { (0xF12, _) => marchid, (0xF13, _) => mimpid, (0xF14, _) => mhartid, + (0xF15, _) => mconfigptr, (0x300, _) => mstatus.bits, (0x301, _) => misa.bits, (0x302, _) => medeleg.bits, diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index ecc53ae..1baa337 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -21,6 +21,7 @@ function is_CSR_defined (csr : csreg, p : Privilege) -> bool = 0xf12 => p == Machine, // marchdid 0xf13 => p == Machine, // mimpid 0xf14 => p == Machine, // mhartid + 0xf15 => p == Machine, // mconfigptr /* machine mode: trap setup */ 0x300 => p == Machine, // mstatus 0x301 => p == Machine, // misa @@ -477,6 +478,7 @@ function init_sys() -> unit = { cur_privilege = Machine; mhartid = zero_extend(0b0); + mconfigptr = zero_extend(0b0); misa[MXL] = arch_to_bits(if sizeof(xlen) == 32 then RV32 else RV64); misa[A] = 0b1; /* atomics */ diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 3e198b4..f3cd7e3 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -515,6 +515,7 @@ register mimpid : xlenbits register marchid : xlenbits /* TODO: this should be readonly, and always 0 for now */ register mhartid : xlenbits +register mconfigptr : xlenbits /* S-mode registers */ -- cgit v1.1 From 495b52ca2a1a4f132419bf6cf7174414d607589e Mon Sep 17 00:00:00 2001 From: Tim Hutt Date: Fri, 5 Apr 2024 09:13:16 +0100 Subject: Add missing check for RV64 on float conversion instructions These two instructions are RV64-only, as noted in the comment, but were missing the check. There are other instructions in this file that did have the check so it was just an ommission. --- model/riscv_insts_dext.sail | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'model') diff --git a/model/riscv_insts_dext.sail b/model/riscv_insts_dext.sail index 58c5d5d..03b5824 100644 --- a/model/riscv_insts_dext.sail +++ b/model/riscv_insts_dext.sail @@ -902,11 +902,11 @@ mapping clause encdec = F_UN_TYPE_D(rs1, rd, FCLASS_D) if /* D instructions, RV64 only */ -mapping clause encdec = F_UN_TYPE_D(rs1, rd, FMV_X_D) if haveDExt() - <-> 0b111_0001 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveDExt() +mapping clause encdec = F_UN_TYPE_D(rs1, rd, FMV_X_D) if haveDExt() & sizeof(xlen) >= 64 + <-> 0b111_0001 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveDExt() & sizeof(xlen) >= 64 -mapping clause encdec = F_UN_TYPE_D(rs1, rd, FMV_D_X) if haveDExt() - <-> 0b111_1001 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveDExt() +mapping clause encdec = F_UN_TYPE_D(rs1, rd, FMV_D_X) if haveDExt() & sizeof(xlen) >= 64 + <-> 0b111_1001 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveDExt() & sizeof(xlen) >= 64 /* Execution semantics ================================ */ -- cgit v1.1 From d7373930aa2c6a0334125ec6cdd7110fd31b8f86 Mon Sep 17 00:00:00 2001 From: Jordan Carlin Date: Mon, 25 Mar 2024 12:48:40 -0700 Subject: Correct fcvtmod.w.d flag generation logic --- model/riscv_insts_zfa.sail | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'model') diff --git a/model/riscv_insts_zfa.sail b/model/riscv_insts_zfa.sail index 9f1e199..5f9f713 100644 --- a/model/riscv_insts_zfa.sail +++ b/model/riscv_insts_zfa.sail @@ -745,7 +745,9 @@ function fcvtmod_helper(x64) = { else integer; /* Raise FP exception flags, honoring the precedence of nV > nX */ - let flags : bits(5) = if (true_exp > 31) then nvFlag() + let max_integer = if sign == 0b1 then unsigned(0x80000000) + else unsigned(0x7fffffff); + let flags : bits(5) = if (true_exp > 31 | unsigned(integer) > max_integer) then nvFlag() else if (fractional != zeros()) then nxFlag() else zeros(); -- cgit v1.1 From c5ee87dfcc862a69ccad6e560423da4bb0e99dd6 Mon Sep 17 00:00:00 2001 From: Jordan Carlin Date: Tue, 26 Mar 2024 11:40:41 -0700 Subject: split fcvtmod.w.d invalid check into 2 if statements --- model/riscv_insts_zfa.sail | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'model') diff --git a/model/riscv_insts_zfa.sail b/model/riscv_insts_zfa.sail index 5f9f713..1443daf 100644 --- a/model/riscv_insts_zfa.sail +++ b/model/riscv_insts_zfa.sail @@ -747,7 +747,8 @@ function fcvtmod_helper(x64) = { /* Raise FP exception flags, honoring the precedence of nV > nX */ let max_integer = if sign == 0b1 then unsigned(0x80000000) else unsigned(0x7fffffff); - let flags : bits(5) = if (true_exp > 31 | unsigned(integer) > max_integer) then nvFlag() + let flags : bits(5) = if true_exp > 31 then nvFlag() + else if unsigned(integer) > max_integer then nvFlag() else if (fractional != zeros()) then nxFlag() else zeros(); -- cgit v1.1 From 34e43b27fa47472cf0abd035f49114734a283d29 Mon Sep 17 00:00:00 2001 From: Martin Berger Date: Mon, 29 Apr 2024 23:26:40 +0100 Subject: Add Svinval extension. These changes add the "Svinval" Standard Extension for Fine-Grained Address-Translation Cache Invalidation, Version 1.0 to the sail-riscv model. This extension defines five new instructions: SINVAL.VMA, SFENCE.W.INVAL, SFENCE.INVAL.IR, HINVAL.VVMA, HINVAL.GVMA. HINVAL.VVMA & HINVAL.GVMA are omitted since they build on the Hypervisor Extension which is yet to be included in the model. SFENCE.W.INVAL & SFENCE.INVAL.IR are treated as nops pending integration of the coherency model (rmem) with sail. The specification says that SINVAL.VMA behaves just as SFENCE.VMA, except there are additional ordering constraints with respect to the new SFENCE.W.INVAL & SFENCE.INVAL.IR instructions. Since these are nops, we can treat SINVAL.VMA as if it were SFENCE.VMA. --- model/riscv_insts_base.sail | 46 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 46 insertions(+) (limited to 'model') diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail index 9c4630b..f102cbd 100644 --- a/model/riscv_insts_base.sail +++ b/model/riscv_insts_base.sail @@ -794,3 +794,49 @@ function clause execute SFENCE_VMA(rs1, rs2) = { mapping clause assembly = SFENCE_VMA(rs1, rs2) <-> "sfence.vma" ^ spc() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) + +/* ****************************************************************** */ +union clause ast = SINVAL_VMA : (regidx, regidx) + +mapping clause encdec = + SINVAL_VMA(rs1, rs2) if haveSvinval() + <-> 0b0001011 @ rs2 : regidx @ rs1 : regidx @ 0b000 @ 0b00000 @ 0b1110011 if haveSvinval() + +function clause execute SINVAL_VMA(rs1, rs2) = { + execute(SFENCE_VMA(rs1, rs2)) +} + +mapping clause assembly = SINVAL_VMA(rs1, rs2) + <-> "sinval.vma" ^ spc() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) + +/* ****************************************************************** */ +union clause ast = SFENCE_W_INVAL : unit + +mapping clause encdec = + SFENCE_W_INVAL() if haveSvinval() + <-> 0b0001100 @ 0b00000 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 if haveSvinval() + +function clause execute SFENCE_W_INVAL() = { + if cur_privilege == User + then { handle_illegal(); RETIRE_FAIL } + else { RETIRE_SUCCESS } +} + +mapping clause assembly = SFENCE_W_INVAL() <-> "sfence.w.inval" + +/* ****************************************************************** */ +union clause ast = SFENCE_INVAL_IR : unit + +mapping clause encdec = + SFENCE_INVAL_IR() if haveSvinval() + <-> 0b0001100 @ 0b00001 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 if haveSvinval() + +function clause execute SFENCE_INVAL_IR() = { + if cur_privilege == User + then { handle_illegal(); RETIRE_FAIL } + else { RETIRE_SUCCESS } +} + +mapping clause assembly = SFENCE_INVAL_IR() <-> "sfence.inval.ir" + +/* ****************************************************************** */ -- cgit v1.1 From 66095cacc025de50eddeccb5d0f166846df1a717 Mon Sep 17 00:00:00 2001 From: Martin Berger Date: Tue, 30 Apr 2024 00:09:59 +0100 Subject: fixup! Add Svinval extension. --- model/riscv_sys_regs.sail | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'model') diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index f3cd7e3..6c66492 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -84,6 +84,8 @@ val sys_enable_writable_misa = {c: "sys_enable_writable_misa", ocaml: "Platform. 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 +/* whether Svinval was enabled at boot */ +val sys_enable_svinval = {c: "sys_enable_svinval", ocaml: "Platform.enable_svinval", _: "sys_enable_svinval"} : unit -> bool /* whether Zcb was enabled at boot */ val sys_enable_zcb = {c: "sys_enable_zcb", ocaml: "Platform.enable_zcb", _: "sys_enable_zcb"} : unit -> bool /* whether zfinx was enabled at boot */ @@ -311,6 +313,8 @@ function haveZfh() -> bool = (misa[F] == 0b1) & (mstatus[FS] != 0b00) /* V extension has to enable both via misa.V as well as mstatus.VS */ function haveVExt() -> bool = (misa[V] == 0b1) & (mstatus[VS] != 0b00) +function haveSvinval() -> bool = sys_enable_svinval() + /* Zcb has simple code-size saving instructions. (The Zcb extension depends on the Zca extension.) */ function haveZcb() -> bool = sys_enable_zcb() -- cgit v1.1 From 418cf128bf212058dfc6a9a3d952edf2a61ce920 Mon Sep 17 00:00:00 2001 From: Martin Berger Date: Tue, 30 Apr 2024 00:47:04 +0100 Subject: fixup! fixup! fixup! Add Svinval extension. --- model/riscv_insts_base.sail | 46 ------------------------------------- model/riscv_insts_svinval.sail | 52 ++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 52 insertions(+), 46 deletions(-) create mode 100644 model/riscv_insts_svinval.sail (limited to 'model') diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail index f102cbd..9c4630b 100644 --- a/model/riscv_insts_base.sail +++ b/model/riscv_insts_base.sail @@ -794,49 +794,3 @@ function clause execute SFENCE_VMA(rs1, rs2) = { mapping clause assembly = SFENCE_VMA(rs1, rs2) <-> "sfence.vma" ^ spc() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) - -/* ****************************************************************** */ -union clause ast = SINVAL_VMA : (regidx, regidx) - -mapping clause encdec = - SINVAL_VMA(rs1, rs2) if haveSvinval() - <-> 0b0001011 @ rs2 : regidx @ rs1 : regidx @ 0b000 @ 0b00000 @ 0b1110011 if haveSvinval() - -function clause execute SINVAL_VMA(rs1, rs2) = { - execute(SFENCE_VMA(rs1, rs2)) -} - -mapping clause assembly = SINVAL_VMA(rs1, rs2) - <-> "sinval.vma" ^ spc() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) - -/* ****************************************************************** */ -union clause ast = SFENCE_W_INVAL : unit - -mapping clause encdec = - SFENCE_W_INVAL() if haveSvinval() - <-> 0b0001100 @ 0b00000 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 if haveSvinval() - -function clause execute SFENCE_W_INVAL() = { - if cur_privilege == User - then { handle_illegal(); RETIRE_FAIL } - else { RETIRE_SUCCESS } -} - -mapping clause assembly = SFENCE_W_INVAL() <-> "sfence.w.inval" - -/* ****************************************************************** */ -union clause ast = SFENCE_INVAL_IR : unit - -mapping clause encdec = - SFENCE_INVAL_IR() if haveSvinval() - <-> 0b0001100 @ 0b00001 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 if haveSvinval() - -function clause execute SFENCE_INVAL_IR() = { - if cur_privilege == User - then { handle_illegal(); RETIRE_FAIL } - else { RETIRE_SUCCESS } -} - -mapping clause assembly = SFENCE_INVAL_IR() <-> "sfence.inval.ir" - -/* ****************************************************************** */ diff --git a/model/riscv_insts_svinval.sail b/model/riscv_insts_svinval.sail new file mode 100644 index 0000000..ea74838 --- /dev/null +++ b/model/riscv_insts_svinval.sail @@ -0,0 +1,52 @@ +/*=======================================================================================*/ +/* This Sail RISC-V architecture model, comprising all files and */ +/* directories except where otherwise noted is subject the BSD */ +/* two-clause license in the LICENSE file. */ +/* */ +/* SPDX-License-Identifier: BSD-2-Clause */ +/*=======================================================================================*/ + +union clause ast = SINVAL_VMA : (regidx, regidx) + +mapping clause encdec = + SINVAL_VMA(rs1, rs2) if haveSvinval() + <-> 0b0001011 @ rs2 : regidx @ rs1 : regidx @ 0b000 @ 0b00000 @ 0b1110011 if haveSvinval() + +function clause execute SINVAL_VMA(rs1, rs2) = { + execute(SFENCE_VMA(rs1, rs2)) +} + +mapping clause assembly = SINVAL_VMA(rs1, rs2) + <-> "sinval.vma" ^ spc() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) + +/* ****************************************************************** */ + +union clause ast = SFENCE_W_INVAL : unit + +mapping clause encdec = + SFENCE_W_INVAL() if haveSvinval() + <-> 0b0001100 @ 0b00000 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 if haveSvinval() + +function clause execute SFENCE_W_INVAL() = { + if cur_privilege == User + then { handle_illegal(); RETIRE_FAIL } + else { RETIRE_SUCCESS } +} + +mapping clause assembly = SFENCE_W_INVAL() <-> "sfence.w.inval" + +/* ****************************************************************** */ + +union clause ast = SFENCE_INVAL_IR : unit + +mapping clause encdec = + SFENCE_INVAL_IR() if haveSvinval() + <-> 0b0001100 @ 0b00001 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 if haveSvinval() + +function clause execute SFENCE_INVAL_IR() = { + if cur_privilege == User + then { handle_illegal(); RETIRE_FAIL } + else { RETIRE_SUCCESS } +} + +mapping clause assembly = SFENCE_INVAL_IR() <-> "sfence.inval.ir" -- cgit v1.1 From 5c55b5bb6f6d69dc3ff58a2ce9b25c4e582f6e88 Mon Sep 17 00:00:00 2001 From: Martin Berger Date: Tue, 30 Apr 2024 09:33:57 +0100 Subject: Add Svinval extension. These changes add the "Svinval" Standard Extension for Fine-Grained Address-Translation Cache Invalidation, Version 1.0 to the sail-riscv model. This extension defines five new instructions: SINVAL.VMA, SFENCE.W.INVAL, SFENCE.INVAL.IR, HINVAL.VVMA, HINVAL.GVMA. HINVAL.VVMA & HINVAL.GVMA are omitted since they build on the Hypervisor Extension which is yet to be included in the model. SFENCE.W.INVAL & SFENCE.INVAL.IR are treated as nops pending integration of the coherency model (rmem) with sail. The specification says that SINVAL.VMA behaves just as SFENCE.VMA, except there are additional ordering constraints with respect to the new SFENCE.W.INVAL & SFENCE.INVAL.IR instructions. Since these are nops, we can treat SINVAL.VMA as if it were SFENCE.VMA. Co-authored-by: Kristin Barber --- model/riscv_insts_svinval.sail | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'model') diff --git a/model/riscv_insts_svinval.sail b/model/riscv_insts_svinval.sail index ea74838..168fb17 100644 --- a/model/riscv_insts_svinval.sail +++ b/model/riscv_insts_svinval.sail @@ -30,7 +30,7 @@ mapping clause encdec = function clause execute SFENCE_W_INVAL() = { if cur_privilege == User then { handle_illegal(); RETIRE_FAIL } - else { RETIRE_SUCCESS } + else { RETIRE_SUCCESS } // Implemented as no-op as all memory operations are visible immediately the current Sail model } mapping clause assembly = SFENCE_W_INVAL() <-> "sfence.w.inval" @@ -46,7 +46,7 @@ mapping clause encdec = function clause execute SFENCE_INVAL_IR() = { if cur_privilege == User then { handle_illegal(); RETIRE_FAIL } - else { RETIRE_SUCCESS } + else { RETIRE_SUCCESS } // Implemented as no-op as all memory operations are visible immediately in current Sail model } mapping clause assembly = SFENCE_INVAL_IR() <-> "sfence.inval.ir" -- cgit v1.1 From f65c4b2c17dfd031581c4faa9939a569a239fce9 Mon Sep 17 00:00:00 2001 From: Tim Hutt Date: Wed, 6 Mar 2024 11:14:14 +0000 Subject: Add missing decoder guards for crypto extensions These guards were missing from one side of each clause. --- model/riscv_insts_zkn.sail | 50 +++++++++++++++++++++++----------------------- model/riscv_insts_zks.sail | 8 ++++---- 2 files changed, 29 insertions(+), 29 deletions(-) (limited to 'model') diff --git a/model/riscv_insts_zkn.sail b/model/riscv_insts_zkn.sail index 160d6e4..8bcd250 100644 --- a/model/riscv_insts_zkn.sail +++ b/model/riscv_insts_zkn.sail @@ -17,16 +17,16 @@ union clause ast = SHA256SUM0 : (regidx, regidx) union clause ast = SHA256SUM1 : (regidx, regidx) mapping clause encdec = SHA256SUM0 (rs1, rd) if haveZknh() - <-> 0b00 @ 0b01000 @ 0b00000 @ rs1 @ 0b001 @ rd @ 0b0010011 + <-> 0b00 @ 0b01000 @ 0b00000 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZknh() mapping clause encdec = SHA256SUM1 (rs1, rd) if haveZknh() - <-> 0b00 @ 0b01000 @ 0b00001 @ rs1 @ 0b001 @ rd @ 0b0010011 + <-> 0b00 @ 0b01000 @ 0b00001 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZknh() mapping clause encdec = SHA256SIG0 (rs1, rd) if haveZknh() - <-> 0b00 @ 0b01000 @ 0b00010 @ rs1 @ 0b001 @ rd @ 0b0010011 + <-> 0b00 @ 0b01000 @ 0b00010 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZknh() mapping clause encdec = SHA256SIG1 (rs1, rd) if haveZknh() - <-> 0b00 @ 0b01000 @ 0b00011 @ rs1 @ 0b001 @ rd @ 0b0010011 + <-> 0b00 @ 0b01000 @ 0b00011 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZknh() mapping clause assembly = SHA256SIG0 (rs1, rd) <-> "sha256sig0" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) @@ -76,7 +76,7 @@ function clause execute (SHA256SUM1(rs1, rd)) = { union clause ast = AES32ESMI : (bits(2), regidx, regidx, regidx) mapping clause encdec = AES32ESMI (bs, rs2, rs1, rd) if haveZkne() & sizeof(xlen) == 32 - <-> bs @ 0b10011 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 + <-> bs @ 0b10011 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if haveZkne() & sizeof(xlen) == 32 mapping clause assembly = AES32ESMI (bs, rs2, rs1, rd) <-> "aes32esmi" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) ^ sep() ^ hex_bits_2(bs) @@ -94,7 +94,7 @@ function clause execute (AES32ESMI (bs, rs2, rs1, rd)) = { union clause ast = AES32ESI : (bits(2), regidx, regidx, regidx) mapping clause encdec = AES32ESI (bs, rs2, rs1, rd) if haveZkne() & sizeof(xlen) == 32 - <-> bs @ 0b10001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 + <-> bs @ 0b10001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if haveZkne() & sizeof(xlen) == 32 mapping clause assembly = AES32ESI (bs, rs2, rs1, rd) <-> "aes32esi" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) ^ sep() ^ hex_bits_2(bs) @@ -116,7 +116,7 @@ function clause execute (AES32ESI (bs, rs2, rs1, rd)) = { union clause ast = AES32DSMI : (bits(2), regidx, regidx, regidx) mapping clause encdec = AES32DSMI (bs, rs2, rs1, rd) if haveZknd() & sizeof(xlen) == 32 - <-> bs @ 0b10111 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 + <-> bs @ 0b10111 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if haveZknd() & sizeof(xlen) == 32 mapping clause assembly = AES32DSMI (bs, rs2, rs1, rd) <-> "aes32dsmi" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) ^ sep() ^ hex_bits_2(bs) @@ -134,7 +134,7 @@ function clause execute (AES32DSMI (bs, rs2, rs1, rd)) = { union clause ast = AES32DSI : (bits(2), regidx, regidx, regidx) mapping clause encdec = AES32DSI (bs, rs2, rs1, rd) if haveZknd() & sizeof(xlen) == 32 - <-> bs @ 0b10101 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 + <-> bs @ 0b10101 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if haveZknd() & sizeof(xlen) == 32 mapping clause assembly = AES32DSI (bs, rs2, rs1, rd) <-> "aes32dsi" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) ^ sep() ^ hex_bits_2(bs) @@ -161,22 +161,22 @@ union clause ast = SHA512SUM0R : (regidx, regidx, regidx) union clause ast = SHA512SUM1R : (regidx, regidx, regidx) mapping clause encdec = SHA512SUM0R (rs2, rs1, rd) if haveZknh() & sizeof(xlen) == 32 - <-> 0b01 @ 0b01000 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 + <-> 0b01 @ 0b01000 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if haveZknh() & sizeof(xlen) == 32 mapping clause encdec = SHA512SUM1R (rs2, rs1, rd) if haveZknh() & sizeof(xlen) == 32 - <-> 0b01 @ 0b01001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 + <-> 0b01 @ 0b01001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if haveZknh() & sizeof(xlen) == 32 mapping clause encdec = SHA512SIG0L (rs2, rs1, rd) if haveZknh() & sizeof(xlen) == 32 - <-> 0b01 @ 0b01010 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 + <-> 0b01 @ 0b01010 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if haveZknh() & sizeof(xlen) == 32 mapping clause encdec = SHA512SIG0H (rs2, rs1, rd) if haveZknh() & sizeof(xlen) == 32 - <-> 0b01 @ 0b01110 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 + <-> 0b01 @ 0b01110 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if haveZknh() & sizeof(xlen) == 32 mapping clause encdec = SHA512SIG1L (rs2, rs1, rd) if haveZknh() & sizeof(xlen) == 32 - <-> 0b01 @ 0b01011 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 + <-> 0b01 @ 0b01011 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if haveZknh() & sizeof(xlen) == 32 mapping clause encdec = SHA512SIG1H (rs2, rs1, rd) if haveZknh() & sizeof(xlen) == 32 - <-> 0b01 @ 0b01111 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 + <-> 0b01 @ 0b01111 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if haveZknh() & sizeof(xlen) == 32 mapping clause assembly = SHA512SIG0L (rs2, rs1, rd) <-> "sha512sig0l" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) @@ -246,25 +246,25 @@ union clause ast = AES64DSM : (regidx, regidx, regidx) union clause ast = AES64DS : (regidx, regidx, regidx) mapping clause encdec = AES64KS1I (rnum, rs1, rd) if (haveZkne() | haveZknd()) & (sizeof(xlen) == 64) & (rnum <_u 0xB) - <-> 0b00 @ 0b11000 @ 0b1 @ rnum @ rs1 @ 0b001 @ rd @ 0b0010011 + <-> 0b00 @ 0b11000 @ 0b1 @ rnum @ rs1 @ 0b001 @ rd @ 0b0010011 if (haveZkne() | haveZknd()) & (sizeof(xlen) == 64) & (rnum <_u 0xB) mapping clause encdec = AES64IM (rs1, rd) if haveZknd() & sizeof(xlen) == 64 - <-> 0b00 @ 0b11000 @ 0b00000 @ rs1 @ 0b001 @ rd @ 0b0010011 + <-> 0b00 @ 0b11000 @ 0b00000 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZknd() & sizeof(xlen) == 64 mapping clause encdec = AES64KS2 (rs2, rs1, rd) if (haveZkne() | haveZknd()) & sizeof(xlen) == 64 - <-> 0b01 @ 0b11111 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 + <-> 0b01 @ 0b11111 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if (haveZkne() | haveZknd()) & sizeof(xlen) == 64 mapping clause encdec = AES64ESM (rs2, rs1, rd) if haveZkne() & sizeof(xlen) == 64 - <-> 0b00 @ 0b11011 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 + <-> 0b00 @ 0b11011 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if haveZkne() & sizeof(xlen) == 64 mapping clause encdec = AES64ES (rs2, rs1, rd) if haveZkne() & sizeof(xlen) == 64 - <-> 0b00 @ 0b11001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 + <-> 0b00 @ 0b11001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if haveZkne() & sizeof(xlen) == 64 mapping clause encdec = AES64DSM (rs2, rs1, rd) if haveZknd() & sizeof(xlen) == 64 - <-> 0b00 @ 0b11111 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 + <-> 0b00 @ 0b11111 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if haveZknd() & sizeof(xlen) == 64 mapping clause encdec = AES64DS (rs2, rs1, rd) if haveZknd() & sizeof(xlen) == 64 - <-> 0b00 @ 0b11101 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 + <-> 0b00 @ 0b11101 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if haveZknd() & sizeof(xlen) == 64 mapping clause assembly = AES64KS1I (rnum, rs1, rd) <-> "aes64ks1i" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_4(rnum) @@ -361,16 +361,16 @@ union clause ast = SHA512SUM0 : (regidx, regidx) union clause ast = SHA512SUM1 : (regidx, regidx) mapping clause encdec = SHA512SUM0 (rs1, rd) if haveZknh() & sizeof(xlen) == 64 - <-> 0b00 @ 0b01000 @ 0b00100 @ rs1 @ 0b001 @ rd @ 0b0010011 + <-> 0b00 @ 0b01000 @ 0b00100 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZknh() & sizeof(xlen) == 64 mapping clause encdec = SHA512SUM1 (rs1, rd) if haveZknh() & sizeof(xlen) == 64 - <-> 0b00 @ 0b01000 @ 0b00101 @ rs1 @ 0b001 @ rd @ 0b0010011 + <-> 0b00 @ 0b01000 @ 0b00101 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZknh() & sizeof(xlen) == 64 mapping clause encdec = SHA512SIG0 (rs1, rd) if haveZknh() & sizeof(xlen) == 64 - <-> 0b00 @ 0b01000 @ 0b00110 @ rs1 @ 0b001 @ rd @ 0b0010011 + <-> 0b00 @ 0b01000 @ 0b00110 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZknh() & sizeof(xlen) == 64 mapping clause encdec = SHA512SIG1 (rs1, rd) if haveZknh() & sizeof(xlen) == 64 - <-> 0b00 @ 0b01000 @ 0b00111 @ rs1 @ 0b001 @ rd @ 0b0010011 + <-> 0b00 @ 0b01000 @ 0b00111 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZknh() & sizeof(xlen) == 64 mapping clause assembly = SHA512SIG0 (rs1, rd) <-> "sha512sig0" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) diff --git a/model/riscv_insts_zks.sail b/model/riscv_insts_zks.sail index 002857a..2cb44f1 100644 --- a/model/riscv_insts_zks.sail +++ b/model/riscv_insts_zks.sail @@ -15,10 +15,10 @@ union clause ast = SM3P0 : (regidx, regidx) union clause ast = SM3P1 : (regidx, regidx) mapping clause encdec = SM3P0 (rs1, rd) if haveZksh() - <-> 0b00 @ 0b01000 @ 0b01000 @ rs1 @ 0b001 @ rd @ 0b0010011 + <-> 0b00 @ 0b01000 @ 0b01000 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZksh() mapping clause encdec = SM3P1 (rs1, rd) if haveZksh() - <-> 0b00 @ 0b01000 @ 0b01001 @ rs1 @ 0b001 @ rd @ 0b0010011 + <-> 0b00 @ 0b01000 @ 0b01001 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZksh() mapping clause assembly = SM3P0 (rs1, rd) <-> "sm3p0" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) @@ -49,10 +49,10 @@ union clause ast = SM4ED : (bits(2), regidx, regidx, regidx) union clause ast = SM4KS : (bits(2), regidx, regidx, regidx) mapping clause encdec = SM4ED (bs, rs2, rs1, rd) if haveZksed() - <-> bs @ 0b11000 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 + <-> bs @ 0b11000 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if haveZksed() mapping clause encdec = SM4KS (bs, rs2, rs1, rd) if haveZksed() - <-> bs @ 0b11010 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 + <-> bs @ 0b11010 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if haveZksed() mapping clause assembly = SM4ED (bs, rs2, rs1, rd) <-> "sm4ed" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) ^ sep() ^ hex_bits_2(bs) -- cgit v1.1 From e3c5b0a3016fa52bf1f167b5a918a60f24b634fa Mon Sep 17 00:00:00 2001 From: Shivang Mishra <35092323+ShivangMishra@users.noreply.github.com> Date: Thu, 9 May 2024 23:15:58 +0530 Subject: Replace vmandnot and vmornot with vmandn and vmorn - Issue #421 (#465) Updates the instruction mnemonics for vmandn and vmorn * replace mnemonics "vmandnot" and "vmornot" with "vmandn" and "vmorn" respectively * renamed MM_VMORNOT and MM_VMANDNOT to match mnemonics --- model/riscv_insts_vext_mask.sail | 12 ++++++------ model/riscv_vreg_type.sail | 2 +- 2 files changed, 7 insertions(+), 7 deletions(-) (limited to 'model') diff --git a/model/riscv_insts_vext_mask.sail b/model/riscv_insts_vext_mask.sail index 6528882..f04ae1a 100755 --- a/model/riscv_insts_vext_mask.sail +++ b/model/riscv_insts_vext_mask.sail @@ -17,11 +17,11 @@ union clause ast = MMTYPE : (mmfunct6, regidx, regidx, regidx) mapping encdec_mmfunct6 : mmfunct6 <-> bits(6) = { MM_VMAND <-> 0b011001, MM_VMNAND <-> 0b011101, - MM_VMANDNOT <-> 0b011000, + MM_VMANDN <-> 0b011000, MM_VMXOR <-> 0b011011, MM_VMOR <-> 0b011010, MM_VMNOR <-> 0b011110, - MM_VMORNOT <-> 0b011100, + MM_VMORN <-> 0b011100, MM_VMXNOR <-> 0b011111 } @@ -51,11 +51,11 @@ function clause execute(MMTYPE(funct6, vs2, vs1, vd)) = { result[i] = match funct6 { MM_VMAND => vs2_val[i] & vs1_val[i], MM_VMNAND => not(vs2_val[i] & vs1_val[i]), - MM_VMANDNOT => vs2_val[i] & not(vs1_val[i]), + MM_VMANDN => vs2_val[i] & not(vs1_val[i]), MM_VMXOR => vs2_val[i] != vs1_val[i], MM_VMOR => vs2_val[i] | vs1_val[i], MM_VMNOR => not(vs2_val[i] | vs1_val[i]), - MM_VMORNOT => vs2_val[i] | not(vs1_val[i]), + MM_VMORN => vs2_val[i] | not(vs1_val[i]), MM_VMXNOR => vs2_val[i] == vs1_val[i] } } @@ -69,11 +69,11 @@ function clause execute(MMTYPE(funct6, vs2, vs1, vd)) = { mapping mmtype_mnemonic : mmfunct6 <-> string = { MM_VMAND <-> "vmand.mm", MM_VMNAND <-> "vmnand.mm", - MM_VMANDNOT <-> "vmandnot.mm", + MM_VMANDN <-> "vmandn.mm", MM_VMXOR <-> "vmxor.mm", MM_VMOR <-> "vmor.mm", MM_VMNOR <-> "vmnor.mm", - MM_VMORNOT <-> "vmornot.mm", + MM_VMORN <-> "vmorn.mm", MM_VMXNOR <-> "vmxnor.mm" } diff --git a/model/riscv_vreg_type.sail b/model/riscv_vreg_type.sail index 3f2ddb0..a1f292a 100755 --- a/model/riscv_vreg_type.sail +++ b/model/riscv_vreg_type.sail @@ -53,7 +53,7 @@ enum nxfunct6 = { NX_VNCLIPU, NX_VNCLIP} enum nxsfunct6 = { NXS_VNSRL, NXS_VNSRA } -enum mmfunct6 = { MM_VMAND, MM_VMNAND, MM_VMANDNOT, MM_VMXOR, MM_VMOR, MM_VMNOR, MM_VMORNOT, MM_VMXNOR } +enum mmfunct6 = { MM_VMAND, MM_VMNAND, MM_VMANDN, MM_VMXOR, MM_VMOR, MM_VMNOR, MM_VMORN, MM_VMXNOR } enum nifunct6 = { NI_VNCLIPU, NI_VNCLIP } -- cgit v1.1 From e1242d851d6b27b357bfb31d46c8f08e18fb768b Mon Sep 17 00:00:00 2001 From: Alasdair Date: Thu, 9 May 2024 20:07:30 +0100 Subject: Refactor MUL instruction This instruction had a bit of a case of 'boolean blindness' code smell, where the mul operation was represented as a triple of booleans. This commit refactors the implemention to use a struct with named fields for high, signed_rs1, and signed_rs2. The C_MUL instruction in Zcb also needs to be changed appropriately The mul_op struct was added in riscv_types While there do some housekeeping w.r.t the comment about a workaround for Sail < 0.15.1, as this is no longer needed. --- model/riscv_insts_mext.sail | 39 +++++++++++++++++++-------------------- model/riscv_insts_zcb.sail | 2 +- model/riscv_types.sail | 21 ++++++++------------- 3 files changed, 28 insertions(+), 34 deletions(-) (limited to 'model') diff --git a/model/riscv_insts_mext.sail b/model/riscv_insts_mext.sail index c1da229..6bf94ee 100644 --- a/model/riscv_insts_mext.sail +++ b/model/riscv_insts_mext.sail @@ -11,27 +11,26 @@ /* ****************************************************************** */ -union clause ast = MUL : (regidx, regidx, regidx, bool, bool, bool) +union clause ast = MUL : (regidx, regidx, regidx, mul_op) -mapping encdec_mul_op : (bool, bool, bool) <-> bits(3) = { - (false, true, true) <-> 0b000, - (true, true, true) <-> 0b001, - (true, true, false) <-> 0b010, - (true, false, false) <-> 0b011 +mapping encdec_mul_op : mul_op <-> bits(3) = { + struct { high = false, signed_rs1 = true, signed_rs2 = true } <-> 0b000, + struct { high = true, signed_rs1 = true, signed_rs2 = true } <-> 0b001, + struct { high = true, signed_rs1 = true, signed_rs2 = false } <-> 0b010, + struct { high = true, signed_rs1 = false, signed_rs2 = false } <-> 0b011 } -/* for some reason the : bits(3) here is still necessary - BUG */ -mapping clause encdec = MUL(rs2, rs1, rd, high, signed1, signed2) - <-> 0b0000001 @ rs2 @ rs1 @ encdec_mul_op(high, signed1, signed2) : bits(3) @ rd @ 0b0110011 +mapping clause encdec = MUL(rs2, rs1, rd, mul_op) + <-> 0b0000001 @ rs2 @ rs1 @ encdec_mul_op(mul_op) @ rd @ 0b0110011 -function clause execute (MUL(rs2, rs1, rd, high, signed1, signed2)) = { +function clause execute (MUL(rs2, rs1, rd, mul_op)) = { if haveMulDiv() | haveZmmul() then { let rs1_val = X(rs1); let rs2_val = X(rs2); - let rs1_int : int = if signed1 then signed(rs1_val) else unsigned(rs1_val); - let rs2_int : int = if signed2 then signed(rs2_val) else unsigned(rs2_val); + let rs1_int : int = if mul_op.signed_rs1 then signed(rs1_val) else unsigned(rs1_val); + let rs2_int : int = if mul_op.signed_rs2 then signed(rs2_val) else unsigned(rs2_val); let result_wide = to_bits(2 * sizeof(xlen), rs1_int * rs2_int); - let result = if high + let result = if mul_op.high then result_wide[(2 * sizeof(xlen) - 1) .. sizeof(xlen)] else result_wide[(sizeof(xlen) - 1) .. 0]; X(rd) = result; @@ -42,15 +41,15 @@ function clause execute (MUL(rs2, rs1, rd, high, signed1, signed2)) = { } } -mapping mul_mnemonic : (bool, bool, bool) <-> string = { - (false, true, true) <-> "mul", - (true, true, true) <-> "mulh", - (true, true, false) <-> "mulhsu", - (true, false, false) <-> "mulhu" +mapping mul_mnemonic : mul_op <-> string = { + struct { high = false, signed_rs1 = true, signed_rs2 = true } <-> "mul", + struct { high = true, signed_rs1 = true, signed_rs2 = true } <-> "mulh", + struct { high = true, signed_rs1 = true, signed_rs2 = false } <-> "mulhsu", + struct { high = true, signed_rs1 = false, signed_rs2 = false } <-> "mulhu" } -mapping clause assembly = MUL(rs2, rs1, rd, high, signed1, signed2) - <-> mul_mnemonic(high, signed1, signed2) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) +mapping clause assembly = MUL(rs2, rs1, rd, mul_op) + <-> mul_mnemonic(mul_op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) /* ****************************************************************** */ union clause ast = DIV : (regidx, regidx, regidx, bool) diff --git a/model/riscv_insts_zcb.sail b/model/riscv_insts_zcb.sail index 1320736..86253bf 100644 --- a/model/riscv_insts_zcb.sail +++ b/model/riscv_insts_zcb.sail @@ -206,5 +206,5 @@ mapping clause assembly = C_MUL(rsdc, rs2c) <-> function clause execute C_MUL(rsdc, rs2c) = { let rd = creg2reg_idx(rsdc); let rs = creg2reg_idx(rs2c); - execute(MUL(rs, rd, rd, false, true, true)) + execute(MUL(rs, rd, rd, struct { high = false, signed_rs1 = true, signed_rs2 = true })) } diff --git a/model/riscv_types.sail b/model/riscv_types.sail index e9a5a19..2b1c132 100644 --- a/model/riscv_types.sail +++ b/model/riscv_types.sail @@ -389,6 +389,12 @@ mapping size_bytes : word_width <-> {1, 2, 4, 8} = { DOUBLE <-> 8, } +struct mul_op = { + high : bool, + signed_rs1 : bool, + signed_rs2 : bool +} + /*! * Raise an internal error reporting that width w is invalid for access kind, k, * and current xlen. The file name and line number should be passed in as the @@ -399,17 +405,6 @@ mapping size_bytes : word_width <-> {1, 2, 4, 8} = { */ val report_invalid_width : forall ('a : Type). (string, int, word_width, string) -> 'a function report_invalid_width(f , l, w, k) -> 'a = { - /* - * Ideally we would call internal_error here but this triggers a Sail bug, - * https://github.com/rems-project/sail/issues/203 in versions < 0.15.1, so - * we work around this by manually inlining. - * TODO when we are happy to require Sail >= 0.15.1 uncomment the following - * and remove the rest of the function. - */ - // internal_error(f, l, "Invalid width, " ^ size_mnemonic(w) ^ ", for " ^ k ^ - // " with xlen=" ^ dec_str(sizeof(xlen))); - assert (false, f ^ ":" ^ dec_str(l) ^ ": " ^ "Invalid width, " - ^ size_mnemonic(w) ^ ", for " ^ k ^ " with xlen=" - ^ dec_str(sizeof(xlen))); - throw Error_internal_error() + internal_error(f, l, "Invalid width, " ^ size_mnemonic(w) ^ ", for " ^ k ^ + " with xlen=" ^ dec_str(sizeof(xlen))) } -- cgit v1.1 From a71fee30035e6d504b156cda0802902345766e70 Mon Sep 17 00:00:00 2001 From: Tim Hutt Date: Tue, 14 May 2024 16:14:14 +0100 Subject: Handle 34-bit PMP address overflow The existing PMP code could not handle physical addresses above 32 bits on RV32, which are possible since Sv32 has 34-bit physical addresses, and the PMP registers are in units of 4 bytes, so they can encode 34-bit addresses. This fixes that by delaying the *4 until the comparison where it can be done using `nat` instead of `xlenbits` which it would overflow. --- model/riscv_pmp_control.sail | 43 +++++++++++++++++++++++++------------------ 1 file changed, 25 insertions(+), 18 deletions(-) (limited to 'model') diff --git a/model/riscv_pmp_control.sail b/model/riscv_pmp_control.sail index 1e4cb77..ce53caf 100644 --- a/model/riscv_pmp_control.sail +++ b/model/riscv_pmp_control.sail @@ -8,19 +8,17 @@ /* address ranges */ -// TODO: handle the 34-bit paddr32 on RV32 +// [min, max) of the matching range, in units of 4 bytes. +type pmp_addr_range_in_words = option((xlenbits, xlenbits)) -/* [min, max) of the matching range. */ -type pmp_addr_range = option((xlenbits, xlenbits)) - -function pmpAddrRange(cfg: Pmpcfg_ent, pmpaddr: xlenbits, prev_pmpaddr: xlenbits) -> pmp_addr_range = { +function pmpAddrRange(cfg: Pmpcfg_ent, pmpaddr: xlenbits, prev_pmpaddr: xlenbits) -> pmp_addr_range_in_words = { match pmpAddrMatchType_of_bits(cfg[A]) { OFF => None(), - TOR => { Some ((prev_pmpaddr << 2, pmpaddr << 2)) }, + TOR => { Some ((prev_pmpaddr, pmpaddr)) }, NA4 => { // NA4 is not selectable when the PMP grain G >= 1. See pmpWriteCfg(). assert(sys_pmp_grain() < 1, "NA4 cannot be selected when PMP grain G >= 1."); - let lo = pmpaddr << 2; + let lo = pmpaddr; Some((lo, lo + 4)) }, NAPOT => { @@ -33,7 +31,7 @@ function pmpAddrRange(cfg: Pmpcfg_ent, pmpaddr: xlenbits, prev_pmpaddr: xlenbits let lo = pmpaddr & (~ (mask)); // mask + 1: 0b00000100000 let len = mask + 1; - Some((lo << 2, (lo + len) << 2)) + Some((lo, (lo + len))) } } } @@ -65,18 +63,27 @@ function pmpCheckPerms(ent, acc, priv) = { enum pmpAddrMatch = {PMP_NoMatch, PMP_PartialMatch, PMP_Match} -function pmpMatchAddr(addr: xlenbits, width: xlenbits, rng: pmp_addr_range) -> pmpAddrMatch = { +function pmpMatchAddr(addr: xlenbits, width: xlenbits, rng: pmp_addr_range_in_words) -> pmpAddrMatch = { match rng { None() => PMP_NoMatch, - Some((lo, hi)) => if hi <=_u lo /* to handle mis-configuration */ - then PMP_NoMatch - else { - if (addr + width <=_u lo) | (hi <=_u addr) - then PMP_NoMatch - else if (lo <=_u addr) & (addr + width <=_u hi) - then PMP_Match - else PMP_PartialMatch - } + Some((lo, hi)) => { + // Convert to integers. + let addr = unsigned(addr); + let width = unsigned(width); + // These are in units of 4 bytes. + let lo = unsigned(lo) * 4; + let hi = unsigned(hi) * 4; + + if hi <= lo /* to handle mis-configuration */ + then PMP_NoMatch + else { + if (addr + width <= lo) | (hi <= addr) + then PMP_NoMatch + else if (lo <= addr) & (addr + width <= hi) + then PMP_Match + else PMP_PartialMatch + } + }, } } -- cgit v1.1 From be1e04c00ab6b301c517039a89254b6485d315d4 Mon Sep 17 00:00:00 2001 From: Tim Hutt Date: Tue, 14 May 2024 17:43:59 +0100 Subject: Add some missing explicit var declarations Implicit `var` declarations will eventually be an error. This makes some implicit `var` declarations explicit. --- model/riscv_insts_zbb.sail | 24 ++++++++++++------------ model/riscv_insts_zbc.sail | 6 +++--- model/riscv_insts_zbkb.sail | 6 +++--- model/riscv_insts_zbkx.sail | 4 ++-- 4 files changed, 20 insertions(+), 20 deletions(-) (limited to 'model') diff --git a/model/riscv_insts_zbb.sail b/model/riscv_insts_zbb.sail index c7671a6..d39afc0 100644 --- a/model/riscv_insts_zbb.sail +++ b/model/riscv_insts_zbb.sail @@ -184,7 +184,7 @@ mapping clause assembly = RISCV_REV8(rs1, rd) function clause execute (RISCV_REV8(rs1, rd)) = { let rs1_val = X(rs1); - result : xlenbits = zeros(); + var result : xlenbits = zeros(); foreach (i from 0 to (sizeof(xlen) - 8) by 8) result[(i + 7) .. i] = rs1_val[(sizeof(xlen) - i - 1) .. (sizeof(xlen) - i - 8)]; X(rd) = result; @@ -202,7 +202,7 @@ mapping clause assembly = RISCV_ORCB(rs1, rd) function clause execute (RISCV_ORCB(rs1, rd)) = { let rs1_val = X(rs1); - result : xlenbits = zeros(); + var result : xlenbits = zeros(); foreach (i from 0 to (sizeof(xlen) - 8) by 8) result[(i + 7) .. i] = if rs1_val[(i + 7) .. i] == zeros() then 0x00 @@ -222,7 +222,7 @@ mapping clause assembly = RISCV_CPOP(rs1, rd) function clause execute (RISCV_CPOP(rs1, rd)) = { let rs1_val = X(rs1); - result : nat = 0; + var result : nat = 0; foreach (i from 0 to (xlen_val - 1)) if rs1_val[i] == bitone then result = result + 1; X(rd) = to_bits(sizeof(xlen), result); @@ -240,7 +240,7 @@ mapping clause assembly = RISCV_CPOPW(rs1, rd) function clause execute (RISCV_CPOPW(rs1, rd)) = { let rs1_val = X(rs1); - result : nat = 0; + var result : nat = 0; foreach (i from 0 to 31) if rs1_val[i] == bitone then result = result + 1; X(rd) = to_bits(sizeof(xlen), result); @@ -258,8 +258,8 @@ mapping clause assembly = RISCV_CLZ(rs1, rd) function clause execute (RISCV_CLZ(rs1, rd)) = { let rs1_val = X(rs1); - result : nat = 0; - done : bool = false; + var result : nat = 0; + var done : bool = false; foreach (i from (sizeof(xlen) - 1) downto 0) if not(done) then if rs1_val[i] == bitzero then result = result + 1 @@ -279,8 +279,8 @@ mapping clause assembly = RISCV_CLZW(rs1, rd) function clause execute (RISCV_CLZW(rs1, rd)) = { let rs1_val = X(rs1); - result : nat = 0; - done : bool = false; + var result : nat = 0; + var done : bool = false; foreach (i from 31 downto 0) if not(done) then if rs1_val[i] == bitzero then result = result + 1 @@ -300,8 +300,8 @@ mapping clause assembly = RISCV_CTZ(rs1, rd) function clause execute (RISCV_CTZ(rs1, rd)) = { let rs1_val = X(rs1); - result : nat = 0; - done : bool = false; + var result : nat = 0; + var done : bool = false; foreach (i from 0 to (sizeof(xlen) - 1)) if not(done) then if rs1_val[i] == bitzero then result = result + 1 @@ -321,8 +321,8 @@ mapping clause assembly = RISCV_CTZW(rs1, rd) function clause execute (RISCV_CTZW(rs1, rd)) = { let rs1_val = X(rs1); - result : nat = 0; - done : bool = false; + var result : nat = 0; + var done : bool = false; foreach (i from 0 to 31) if not(done) then if rs1_val[i] == bitzero then result = result + 1 diff --git a/model/riscv_insts_zbc.sail b/model/riscv_insts_zbc.sail index 910db1b..458b9fa 100644 --- a/model/riscv_insts_zbc.sail +++ b/model/riscv_insts_zbc.sail @@ -18,7 +18,7 @@ mapping clause assembly = RISCV_CLMUL(rs2, rs1, rd) function clause execute (RISCV_CLMUL(rs2, rs1, rd)) = { let rs1_val = X(rs1); let rs2_val = X(rs2); - result : xlenbits = zeros(); + var result : xlenbits = zeros(); foreach (i from 0 to (xlen_val - 1)) if rs2_val[i] == bitone then result = result ^ (rs1_val << i); X(rd) = result; @@ -37,7 +37,7 @@ mapping clause assembly = RISCV_CLMULH(rs2, rs1, rd) function clause execute (RISCV_CLMULH(rs2, rs1, rd)) = { let rs1_val = X(rs1); let rs2_val = X(rs2); - result : xlenbits = zeros(); + var result : xlenbits = zeros(); foreach (i from 0 to (xlen_val - 1)) if rs2_val[i] == bitone then result = result ^ (rs1_val >> (xlen_val - i)); X(rd) = result; @@ -56,7 +56,7 @@ mapping clause assembly = RISCV_CLMULR(rs2, rs1, rd) function clause execute (RISCV_CLMULR(rs2, rs1, rd)) = { let rs1_val = X(rs1); let rs2_val = X(rs2); - result : xlenbits = zeros(); + var result : xlenbits = zeros(); foreach (i from 0 to (xlen_val - 1)) if rs2_val[i] == bitone then result = result ^ (rs1_val >> (xlen_val - i - 1)); X(rd) = result; diff --git a/model/riscv_insts_zbkb.sail b/model/riscv_insts_zbkb.sail index 76190f0..f6246d1 100644 --- a/model/riscv_insts_zbkb.sail +++ b/model/riscv_insts_zbkb.sail @@ -64,7 +64,7 @@ mapping clause assembly = RISCV_ZIP(rs1, rd) function clause execute (RISCV_ZIP(rs1, rd)) = { assert(sizeof(xlen) == 32); let rs1_val = X(rs1); - result : xlenbits = zeros(); + var result : xlenbits = zeros(); foreach (i from 0 to (sizeof(xlen_bytes)*4 - 1)) { result[i*2] = rs1_val[i]; result[i*2 + 1] = rs1_val[i + sizeof(xlen_bytes)*4]; @@ -85,7 +85,7 @@ mapping clause assembly = RISCV_UNZIP(rs1, rd) function clause execute (RISCV_UNZIP(rs1, rd)) = { assert(sizeof(xlen) == 32); let rs1_val = X(rs1); - result : xlenbits = zeros(); + var result : xlenbits = zeros(); foreach (i from 0 to (sizeof(xlen_bytes)*4 - 1)) { result[i] = rs1_val[i*2]; result[i + sizeof(xlen_bytes)*4] = rs1_val[i*2 + 1]; @@ -105,7 +105,7 @@ mapping clause assembly = RISCV_BREV8(rs1, rd) function clause execute (RISCV_BREV8(rs1, rd)) = { let rs1_val = X(rs1); - result : xlenbits = zeros(); + var result : xlenbits = zeros(); foreach (i from 0 to (sizeof(xlen) - 8) by 8) result[i+7..i] = reverse(rs1_val[i+7..i]); X(rd) = result; diff --git a/model/riscv_insts_zbkx.sail b/model/riscv_insts_zbkx.sail index 59a90c6..d19a2b1 100644 --- a/model/riscv_insts_zbkx.sail +++ b/model/riscv_insts_zbkx.sail @@ -18,7 +18,7 @@ mapping clause assembly = RISCV_XPERM8(rs2, rs1, rd) function clause execute (RISCV_XPERM8(rs2, rs1, rd)) = { let rs1_val = X(rs1); let rs2_val = X(rs2); - result : xlenbits = zeros(); + var result : xlenbits = zeros(); foreach (i from 0 to (sizeof(xlen) - 8) by 8) { let index = unsigned(rs2_val[i+7..i]); result[i+7..i] = if 8*index < sizeof(xlen) @@ -41,7 +41,7 @@ mapping clause assembly = RISCV_XPERM4(rs2, rs1, rd) function clause execute (RISCV_XPERM4(rs2, rs1, rd)) = { let rs1_val = X(rs1); let rs2_val = X(rs2); - result : xlenbits = zeros(); + var result : xlenbits = zeros(); foreach (i from 0 to (sizeof(xlen) - 4) by 4) { let index = unsigned(rs2_val[i+3..i]); result[i+3..i] = if 4*index < sizeof(xlen) -- cgit v1.1