diff options
29 files changed, 223 insertions, 138 deletions
@@ -27,6 +27,8 @@ SAIL_DEFAULT_INST = riscv_insts_base.sail riscv_insts_aext.sail riscv_insts_cext SAIL_DEFAULT_INST += riscv_insts_fext.sail riscv_insts_cfext.sail SAIL_DEFAULT_INST += riscv_insts_dext.sail riscv_insts_cdext.sail +SAIL_DEFAULT_INST += riscv_insts_svinval.sail + SAIL_DEFAULT_INST += riscv_insts_zba.sail SAIL_DEFAULT_INST += riscv_insts_zbb.sail SAIL_DEFAULT_INST += riscv_insts_zbc.sail @@ -136,14 +138,16 @@ export SAIL_DIR EXPLICIT_COQ_SAIL=yes else # Use sail from opam package -SAIL_DIR:=$(shell opam config var sail:share) +SAIL_DIR:=$(shell OPAMCLI=$(OPAMCLI) opam config var sail:share) SAIL:=sail endif SAIL_LIB_DIR:=$(SAIL_DIR)/lib export SAIL_LIB_DIR SAIL_SRC_DIR:=$(SAIL_DIR)/src -LEM_DIR?=$(shell opam config var lem:share) +ifndef LEM_DIR +LEM_DIR:=$(shell OPAMCLI=$(OPAMCLI) opam config var lem:share) +endif export LEM_DIR C_WARNINGS ?= @@ -199,7 +203,7 @@ RISCV_EXTRAS_LEM = $(addprefix handwritten_support/,$(RISCV_EXTRAS_LEM_FILES)) .PHONY: -all: ocaml_emulator/riscv_ocaml_sim_$(ARCH) c_emulator/riscv_sim_$(ARCH) riscv_isa riscv_coq riscv_hol riscv_rmem +all: ocaml_emulator/riscv_ocaml_sim_$(ARCH) c_emulator/riscv_sim_$(ARCH) .PHONY: all # the following ensures empty sail-generated .c files don't hang around and @@ -368,9 +372,9 @@ riscv_hol_build: generated_definitions/hol4/$(ARCH)/riscvTheory.uo .PHONY: riscv_hol riscv_hol_build ifdef BBV_DIR - EXPLICIT_COQ_BBV = yes + EXPLICIT_COQ_BBV := yes else - EXPLICIT_COQ_BBV = $(shell if opam config var coq-bbv:share >/dev/null 2>/dev/null; then echo no; else echo yes; fi) + EXPLICIT_COQ_BBV := $(shell if OPAMCLI=$(OPAMCLI) opam config var coq-bbv:share >/dev/null 2>/dev/null; then echo no; else echo yes; fi) ifeq ($(EXPLICIT_COQ_BBV),yes) #Coq BBV library hopefully checked out in directory above us BBV_DIR = ../bbv @@ -378,7 +382,7 @@ else endif ifndef EXPLICIT_COQ_SAIL - EXPLICIT_COQ_SAIL = $(shell if opam config var coq-sail:share >/dev/null 2>/dev/null; then echo no; else echo yes; fi) + EXPLICIT_COQ_SAIL := $(shell if OPAMCLI=$(OPAMCLI) opam config var coq-sail:share >/dev/null 2>/dev/null; then echo no; else echo yes; fi) endif COQ_LIBS = -R generated_definitions/coq Riscv -R generated_definitions/coq/$(ARCH) $(ARCH) -R handwritten_support Riscv_common @@ -2,7 +2,7 @@ RISCV Sail Model ================ This repository contains a formal specification of the RISC-V architecture, written in -[Sail](https://www.cl.cam.ac.uk/~pes20/sail/) ([repo](https://github.com/rems-project/sail)). It has been adopted by the RISC-V Foundation. As of 2021-08-24, the repo has been moved from <https://github.com/rems-project/sail-riscv> to <https://github.com/riscv/sail-riscv>. +[Sail](https://github.com/rems-project/sail). It has been adopted by the RISC-V Foundation. As of 2021-08-24, the repo has been moved from <https://github.com/rems-project/sail-riscv> to <https://github.com/riscv/sail-riscv>. The model specifies assembly language formats of the instructions, the corresponding @@ -15,48 +15,41 @@ A [reading guide](doc/ReadingGuide.md) to the model is provided in the extend](doc/ExtendingGuide.md) the model. -Latex definitions can be generated from the model that are suitable +Latex or AsciiDoc definitions can be generated from the model that are suitable for inclusion in reference documentation. Drafts of the RISC-V [unprivileged](https://github.com/rems-project/riscv-isa-manual/blob/sail/release/riscv-spec-sail-draft.pdf) and [privileged](https://github.com/rems-project/riscv-isa-manual/blob/sail/release/riscv-privileged-sail-draft.pdf) specifications that include the Sail formal definitions are available in the sail branch of this [risc-v-isa-manual repository](https://github.com/rems-project/riscv-isa-manual/tree/sail). The process to perform this inclusion is explained [here](https://github.com/rems-project/riscv-isa-manual/blob/sail/README.SAIL). +There is also the newer [Sail AsciiDoctor documentation support for RISC-V](https://github.com/Alasdair/asciidoctor-sail/blob/master/doc/built/sail_to_asciidoc.pdf). -This is one of [several formal models](https://github.com/riscv/ISA_Formal_Spec_Public_Review/blob/master/comparison_table.md) that were compared within the +This is one of [several formal models](https://github.com/riscv/ISA_Formal_Spec_Public_Review/blob/master/comparison_table.md) that were compared within the 2019 [RISC-V ISA Formal Spec Public Review](https://github.com/riscv/ISA_Formal_Spec_Public_Review). What is Sail? ------------- -[Sail](https://www.cl.cam.ac.uk/~pes20/sail/) ([repo](https://github.com/rems-project/sail)) is a language for describing the instruction-set architecture -(ISA) semantics of processors. Sail aims to provide a -engineer-friendly, vendor-pseudocode-like language for describing -instruction semantics. It is essentially a first-order imperative -language, but with lightweight dependent typing for numeric types and -bitvector lengths, which are automatically checked using Z3. +[Sail](https://github.com/rems-project/sail) is a language for describing the instruction-set architecture +(ISA) semantics of processors: the architectural specification of the behaviour of machine instructions. Sail is an +engineer-friendly language, much like earlier vendor pseudocode, but more precisely defined and with tooling to support a wide range of use-cases. <p> -Given a Sail definition, the tool will type-check it and generate -LaTeX snippets to use in documentation, executable emulators (in C and OCaml), theorem-prover definitions for -Isabelle, HOL4, and Coq, and definitions to integrate with our -<a href="http://www.cl.cam.ac.uk/users/pes20/rmem">RMEM</a> -and -<a href="isla-axiomatic.cl.cam.ac.uk/">isla-axiomatic</a> tools for -concurrency semantics. +Given a Sail specification, the tool can type-check it, generate documentation snippets (in LaTeX or AsciiDoc), generate executable emulators (in C or OCaml), show specification coverage, generate versions of the ISA for relaxed memory model tools, support automated instruction-sequence test generation, generate theorem-prover definitions for +interactive proof (in Isabelle, HOL4, and Coq), support proof about binary code (in Islaris), and (in progress) generate a reference ISA model in SystemVerilog that can be used for formal hardware verification. <p> <img width="800" src="https://www.cl.cam.ac.uk/~pes20/sail/overview-sail.png?"> <p> Sail is being used for multiple ISA descriptions, including -essentially complete versions of the sequential behaviour of Armv8-A +essentially complete versions of the sequential behaviour of Arm-A (automatically derived from the authoritative Arm-internal specification, and released under a BSD Clear licence with Arm's -permission), RISC-V, MIPS, CHERI-RISC-V, and CHERI-MIPS; all these are complete +permission), RISC-V, CHERI-RISC-V, CHERIoT, MIPS, and CHERI-MIPS; all these are complete enough to boot various operating systems. There are also Sail models -for smaller fragments of IBM POWER and x86. +for smaller fragments of IBM POWER and x86, including a version of the ACL2 x86 model automatically translated from that. diff --git a/c_emulator/riscv_platform.c b/c_emulator/riscv_platform.c index 6544de6..5b98528 100644 --- a/c_emulator/riscv_platform.c +++ b/c_emulator/riscv_platform.c @@ -32,6 +32,11 @@ bool sys_enable_fdext(unit u) return rv_enable_fdext; } +bool sys_enable_svinval(unit u) +{ + return rv_enable_svinval; +} + bool sys_enable_zcb(unit u) { return rv_enable_zcb; diff --git a/c_emulator/riscv_platform.h b/c_emulator/riscv_platform.h index 4a53d12..3cc6f02 100644 --- a/c_emulator/riscv_platform.h +++ b/c_emulator/riscv_platform.h @@ -4,6 +4,7 @@ bool sys_enable_rvc(unit); bool sys_enable_next(unit); bool sys_enable_fdext(unit); +bool sys_enable_svinval(unit); bool sys_enable_zcb(unit); bool sys_enable_zfinx(unit); bool sys_enable_writable_misa(unit); diff --git a/c_emulator/riscv_platform_impl.c b/c_emulator/riscv_platform_impl.c index 449bb1d..077fc50 100644 --- a/c_emulator/riscv_platform_impl.c +++ b/c_emulator/riscv_platform_impl.c @@ -6,6 +6,7 @@ uint64_t rv_pmp_count = 0; uint64_t rv_pmp_grain = 0; +bool rv_enable_svinval = false; bool rv_enable_zcb = false; bool rv_enable_zfinx = false; bool rv_enable_rvc = true; diff --git a/c_emulator/riscv_platform_impl.h b/c_emulator/riscv_platform_impl.h index d377c9c..c4289e6 100644 --- a/c_emulator/riscv_platform_impl.h +++ b/c_emulator/riscv_platform_impl.h @@ -11,6 +11,7 @@ extern uint64_t rv_pmp_count; extern uint64_t rv_pmp_grain; +extern bool rv_enable_svinval; extern bool rv_enable_zcb; extern bool rv_enable_zfinx; extern bool rv_enable_rvc; diff --git a/c_emulator/riscv_sim.c b/c_emulator/riscv_sim.c index bf68da2..3a9bfc0 100644 --- a/c_emulator/riscv_sim.c +++ b/c_emulator/riscv_sim.c @@ -53,6 +53,7 @@ const char *RV32ISA = "RV32IMAC"; #define OPT_ENABLE_WRITABLE_FIOM 1001 #define OPT_PMP_COUNT 1002 #define OPT_PMP_GRAIN 1003 +#define OPT_ENABLE_SVINVAL 1004 #define OPT_ENABLE_ZCB 10014 static bool do_dump_dts = false; @@ -146,6 +147,7 @@ static struct option options[] = { {"inst-limit", required_argument, 0, 'l' }, {"enable-zfinx", no_argument, 0, 'x' }, {"enable-writable-fiom", no_argument, 0, OPT_ENABLE_WRITABLE_FIOM}, + {"enable-svinval", no_argument, 0, OPT_ENABLE_SVINVAL }, {"enable-zcb", no_argument, 0, OPT_ENABLE_ZCB }, #ifdef SAILCOV {"sailcov-file", required_argument, 0, 'c' }, diff --git a/handwritten_support/riscv_extras.lem b/handwritten_support/riscv_extras.lem index 27e8ee5..4bc3300 100644 --- a/handwritten_support/riscv_extras.lem +++ b/handwritten_support/riscv_extras.lem @@ -169,6 +169,14 @@ val sys_enable_writable_fiom : unit -> bool let sys_enable_writable_fiom () = true declare ocaml target_rep function sys_enable_writable_fiom = `Platform.enable_writable_fiom` +val sys_pmp_grain : unit -> integer +let sys_pmp_grain () = 0 +declare ocaml target_rep function sys_pmp_grain = `Platform.sys_pmp_grain` + +val sys_pmp_count : unit -> integer +let sys_pmp_count () = 0 +declare ocaml target_rep function sys_pmp_count = `Platform.sys_pmp_count` + val plat_ram_base : unit -> bitvector let plat_ram_base () = [] declare ocaml target_rep function plat_ram_base = `Platform.dram_base` 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_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 ================================ */ 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_svinval.sail b/model/riscv_insts_svinval.sail new file mode 100644 index 0000000..168fb17 --- /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 } // Implemented as no-op as all memory operations are visible immediately the current Sail model +} + +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 } // Implemented as no-op as all memory operations are visible immediately in current Sail model +} + +mapping clause assembly = SFENCE_INVAL_IR() <-> "sfence.inval.ir" 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_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) 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_insts_zfa.sail b/model/riscv_insts_zfa.sail index 9f1e199..1443daf 100644 --- a/model/riscv_insts_zfa.sail +++ b/model/riscv_insts_zfa.sail @@ -745,7 +745,10 @@ 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 then nvFlag() + else if unsigned(integer) > max_integer then nvFlag() else if (fractional != zeros()) then nxFlag() else zeros(); 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_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) 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 + } + }, } } 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..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() @@ -515,6 +519,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 */ 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))) } diff --git a/model/riscv_vreg_type.sail b/model/riscv_vreg_type.sail index baed7fa..2ab211b 100755 --- a/model/riscv_vreg_type.sail +++ b/model/riscv_vreg_type.sail @@ -52,7 +52,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 } diff --git a/ocaml_emulator/platform.ml b/ocaml_emulator/platform.ml index 2f0aaaf..69f2714 100644 --- a/ocaml_emulator/platform.ml +++ b/ocaml_emulator/platform.ml @@ -10,6 +10,7 @@ let config_enable_writable_misa = ref true let config_enable_dirty_update = ref false let config_enable_misaligned_access = ref false let config_mtval_has_illegal_inst_bits = ref false +let config_enable_svinval = ref false let config_enable_zcb = ref false let config_enable_writable_fiom = ref true let config_enable_vext = ref true @@ -89,6 +90,7 @@ let enable_vext () = !config_enable_vext let enable_dirty_update () = !config_enable_dirty_update let enable_misaligned_access () = !config_enable_misaligned_access let mtval_has_illegal_inst_bits () = !config_mtval_has_illegal_inst_bits +let enable_svinval () = !config_enable_svinval let enable_zcb () = !config_enable_zcb let enable_zfinx () = false let enable_writable_fiom () = !config_enable_writable_fiom diff --git a/ocaml_emulator/riscv_ocaml_sim.ml b/ocaml_emulator/riscv_ocaml_sim.ml index 8dad8a4..56be8d8 100644 --- a/ocaml_emulator/riscv_ocaml_sim.ml +++ b/ocaml_emulator/riscv_ocaml_sim.ml @@ -53,6 +53,9 @@ let options = Arg.align ([("-dump-dts", ("-mtval-has-illegal-inst-bits", Arg.Set P.config_mtval_has_illegal_inst_bits, " mtval stores instruction bits on an illegal instruction exception"); + ("-enable-svinval", + Arg.Set P.config_enable_svinval, + " enable Svinval extension"); ("-enable-zcb", Arg.Set P.config_enable_zcb, " enable Zcb (simple code size) extension"); |