From 2923e217a9396fa9a4ea2283ed6d398c4181074d Mon Sep 17 00:00:00 2001 From: Pan Li Date: Wed, 7 Feb 2024 13:54:44 +0800 Subject: [PATCH 1/8] Softfloat: Add soft floating-point equals API in sail model This patch would like to introduce the soft floating-point equals API into the sail model. Then the softfloat_interface is able to leverage the new softfloat in sail, instead of the c_emulator. * Add softfloat common for softfloat enter and leave. * Add enum like immutable exception flags. * Add softfloat equals API for half, single and double floating-point. * Replace the extern call of softfloat interface to sail model. * Add helper functions to utils. * Adjust build system for new files. Signed-off-by: Pan Li --- Makefile | 2 + model/riscv_insts_vext_utils.sail | 18 +++ model/riscv_softfloat_interface.sail | 13 +- model/softfloat/riscv_softfloat_common.sail | 123 ++++++++++++++++ model/softfloat/riscv_softfloat_eq.sail | 153 ++++++++++++++++++++ sail-riscv.install | 2 +- 6 files changed, 304 insertions(+), 7 deletions(-) create mode 100644 model/softfloat/riscv_softfloat_common.sail create mode 100644 model/softfloat/riscv_softfloat_eq.sail diff --git a/Makefile b/Makefile index 255224125..123a8ca97 100644 --- a/Makefile +++ b/Makefile @@ -68,6 +68,8 @@ SAIL_SYS_SRCS += riscv_sys_exceptions.sail # default basic helpers for exceptio SAIL_SYS_SRCS += riscv_sync_exception.sail # define the exception structure used in the model SAIL_SYS_SRCS += riscv_next_control.sail # helpers for the 'N' extension SAIL_SYS_SRCS += riscv_softfloat_interface.sail riscv_fdext_regs.sail riscv_fdext_control.sail +SAIL_SYS_SRCS += softfloat/riscv_softfloat_common.sail +SAIL_SYS_SRCS += softfloat/riscv_softfloat_eq.sail SAIL_SYS_SRCS += riscv_csr_ext.sail # access to CSR extensions SAIL_SYS_SRCS += riscv_sys_control.sail # general exception handling diff --git a/model/riscv_insts_vext_utils.sail b/model/riscv_insts_vext_utils.sail index 7b29a0f4f..84ec68119 100755 --- a/model/riscv_insts_vext_utils.sail +++ b/model/riscv_insts_vext_utils.sail @@ -560,6 +560,15 @@ function f_is_SNaN(xf) = { } } +val f_is_at_least_one_SNaN : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool +function f_is_at_least_one_SNaN (op1, op2) = { + match 'm { + 16 => f_is_SNaN_H(op1) | f_is_SNaN_H(op2), + 32 => f_is_SNaN_S(op1) | f_is_SNaN_S(op2), + 64 => f_is_SNaN_D(op1) | f_is_SNaN_D(op2), + } +} + val f_is_QNaN : forall 'm, 'm in {16, 32, 64}. bits('m) -> bool function f_is_QNaN(xf) = { match 'm { @@ -578,6 +587,15 @@ function f_is_NaN(xf) = { } } +val f_is_at_least_one_NaN : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool +function f_is_at_least_one_NaN (op1, op2) = { + match 'm { + 16 => f_is_NaN_H(op1) | f_is_NaN_H(op2), + 32 => f_is_NaN_S(op1) | f_is_NaN_S(op2), + 64 => f_is_NaN_D(op1) | f_is_NaN_D(op2), + } +} + /* Scalar register shaping for floating point operations */ val get_scalar_fp : forall 'n, 'n in {16, 32, 64}. (regidx, int('n)) -> bits('n) function get_scalar_fp(rs1, SEW) = { diff --git a/model/riscv_softfloat_interface.sail b/model/riscv_softfloat_interface.sail index 3e5e7e054..509b03deb 100644 --- a/model/riscv_softfloat_interface.sail +++ b/model/riscv_softfloat_interface.sail @@ -105,6 +105,7 @@ type bits_LU = bits(64) /* Unsigned integer */ */ register float_result : bits(64) register float_fflags : bits(64) +register float_roundingMode : bits_rm /* **************************************************************** */ /* ADD/SUB/MUL/DIV */ @@ -486,10 +487,10 @@ function riscv_f16Le_quiet (v1, v2) = { (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } -val extern_f16Eq = {c: "softfloat_f16eq", ocaml: "Softfloat.f16_eq", lem: "softfloat_f16_eq"} : (bits_H, bits_H) -> unit +val riscv_softfloat_eq : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> unit val riscv_f16Eq : (bits_H, bits_H) -> (bits_fflags, bool) function riscv_f16Eq (v1, v2) = { - extern_f16Eq(v1, v2); + riscv_softfloat_eq (v1, v2); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } @@ -521,10 +522,10 @@ function riscv_f32Le_quiet (v1, v2) = { (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } -val extern_f32Eq = {c: "softfloat_f32eq", ocaml: "Softfloat.f32_eq", lem: "softfloat_f32_eq"} : (bits_S, bits_S) -> unit +val riscv_softfloat_eq : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> unit val riscv_f32Eq : (bits_S, bits_S) -> (bits_fflags, bool) function riscv_f32Eq (v1, v2) = { - extern_f32Eq(v1, v2); + riscv_softfloat_eq (v1, v2); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } @@ -556,10 +557,10 @@ function riscv_f64Le_quiet (v1, v2) = { (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } -val extern_f64Eq = {c: "softfloat_f64eq", ocaml: "Softfloat.f64_eq", lem: "softfloat_f64_eq"} : (bits_D, bits_D) -> unit +val riscv_softfloat_eq : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> unit val riscv_f64Eq : (bits_D, bits_D) -> (bits_fflags, bool) function riscv_f64Eq (v1, v2) = { - extern_f64Eq(v1, v2); + riscv_softfloat_eq (v1, v2); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } diff --git a/model/softfloat/riscv_softfloat_common.sail b/model/softfloat/riscv_softfloat_common.sail new file mode 100644 index 000000000..820ea2f17 --- /dev/null +++ b/model/softfloat/riscv_softfloat_common.sail @@ -0,0 +1,123 @@ +/*=======================================================================================*/ +/* RISCV Sail Model */ +/* */ +/* This Sail RISC-V architecture model, comprising all files and */ +/* directories except for the snapshots of the Lem and Sail libraries */ +/* in the prover_snapshots directory (which include copies of their */ +/* licences), is subject to the BSD two-clause licence below. */ +/* */ +/* Copyright (c) 2017-2023 */ +/* Prashanth Mundkur */ +/* Rishiyur S. Nikhil and Bluespec, Inc. */ +/* Jon French */ +/* Brian Campbell */ +/* Robert Norton-Wright */ +/* Alasdair Armstrong */ +/* Thomas Bauereiss */ +/* Shaked Flur */ +/* Christopher Pulte */ +/* Peter Sewell */ +/* Alexander Richardson */ +/* Hesham Almatary */ +/* Jessica Clarke */ +/* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ +/* Intel, for contributions by Pan Li */ +/* Peter Rugg */ +/* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ +/* */ +/* All rights reserved. */ +/* */ +/* This software was developed by the above within the Rigorous */ +/* Engineering of Mainstream Systems (REMS) project, partly funded by */ +/* EPSRC grant EP/K008528/1, at the Universities of Cambridge and */ +/* Edinburgh. */ +/* */ +/* This software was developed by SRI International and the University of */ +/* Cambridge Computer Laboratory (Department of Computer Science and */ +/* Technology) under DARPA/AFRL contract FA8650-18-C-7809 ("CIFV"), and */ +/* under DARPA contract HR0011-18-C-0016 ("ECATS") as part of the DARPA */ +/* SSITH research programme. */ +/* */ +/* This project has received funding from the European Research Council */ +/* (ERC) under the European Union’s Horizon 2020 research and innovation */ +/* programme (grant agreement 789108, ELVER). */ +/* */ +/* */ +/* Redistribution and use in source and binary forms, with or without */ +/* modification, are permitted provided that the following conditions */ +/* are met: */ +/* 1. Redistributions of source code must retain the above copyright */ +/* notice, this list of conditions and the following disclaimer. */ +/* 2. Redistributions in binary form must reproduce the above copyright */ +/* notice, this list of conditions and the following disclaimer in */ +/* the documentation and/or other materials provided with the */ +/* distribution. */ +/* */ +/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ +/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ +/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ +/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ +/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ +/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ +/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ +/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ +/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ +/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ +/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ +/* SUCH DAMAGE. */ +/*=======================================================================================*/ + +/* **************************************************************** */ +/* This file implements the floating-point for some common helper */ +/* functions. They will be leveraged by other softfloat sail */ +/* implementations. */ +/* */ +/* However, the implementation still need some global variables in */ +/* file riscv_softfloat_interface.sail. It includes: */ +/* 1. float_result. */ +/* 2. float_fflags. */ +/* 3. float_roundingMode. */ +/* **************************************************************** */ + +let softfloat_flag_inexact : bits(64) = 0x0000000000000001 +let softfloat_flag_underflow : bits(64) = 0x0000000000000002 +let softfloat_flag_overflow : bits(64) = 0x0000000000000004 +let softfloat_flag_infinit : bits(64) = 0x0000000000000008 +let softfloat_flag_invalid : bits(64) = 0x0000000000000010 + +val riscv_softfloat_enter : (bits_rm) -> unit +function riscv_softfloat_enter (roundingMode) -> unit = { + float_fflags = zeros(64); + float_roundingMode = roundingMode; +} + +val riscv_softfloat_bits_H_leave : (bits_H) -> unit +function riscv_softfloat_bits_H_leave (result) -> unit = { + float_result[15 .. 0] = result; +} + +val riscv_softfloat_bits_S_leave : (bits_S) -> unit +function riscv_softfloat_bits_S_leave (result) -> unit = { + float_result[31 .. 0] = result; +} + +val riscv_softfloat_bits_D_leave : (bits_D) -> unit +function riscv_softfloat_bits_D_leave (result) -> unit = { + float_result[63 .. 0] = result; +} + +val riscv_softfloat_leave : forall 'm, 'm in {16, 32, 64}. bits('m) -> unit +function riscv_softfloat_leave (op) = { + match 'm { + 16 => riscv_softfloat_bits_H_leave(op), + 32 => riscv_softfloat_bits_S_leave(op), + 64 => riscv_softfloat_bits_D_leave(op), + } +} + +val riscv_softfloat_raise_flags : (bits(64)) -> unit +function riscv_softfloat_raise_flags (flags) -> unit = { + float_fflags = float_fflags | flags +} diff --git a/model/softfloat/riscv_softfloat_eq.sail b/model/softfloat/riscv_softfloat_eq.sail new file mode 100644 index 000000000..4ac5305d6 --- /dev/null +++ b/model/softfloat/riscv_softfloat_eq.sail @@ -0,0 +1,153 @@ +/*=======================================================================================*/ +/* RISCV Sail Model */ +/* */ +/* This Sail RISC-V architecture model, comprising all files and */ +/* directories except for the snapshots of the Lem and Sail libraries */ +/* in the prover_snapshots directory (which include copies of their */ +/* licences), is subject to the BSD two-clause licence below. */ +/* */ +/* Copyright (c) 2017-2023 */ +/* Prashanth Mundkur */ +/* Rishiyur S. Nikhil and Bluespec, Inc. */ +/* Jon French */ +/* Brian Campbell */ +/* Robert Norton-Wright */ +/* Alasdair Armstrong */ +/* Thomas Bauereiss */ +/* Shaked Flur */ +/* Christopher Pulte */ +/* Peter Sewell */ +/* Alexander Richardson */ +/* Hesham Almatary */ +/* Jessica Clarke */ +/* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ +/* Intel, for contributions by Pan Li */ +/* Peter Rugg */ +/* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ +/* */ +/* All rights reserved. */ +/* */ +/* This software was developed by the above within the Rigorous */ +/* Engineering of Mainstream Systems (REMS) project, partly funded by */ +/* EPSRC grant EP/K008528/1, at the Universities of Cambridge and */ +/* Edinburgh. */ +/* */ +/* This software was developed by SRI International and the University of */ +/* Cambridge Computer Laboratory (Department of Computer Science and */ +/* Technology) under DARPA/AFRL contract FA8650-18-C-7809 ("CIFV"), and */ +/* under DARPA contract HR0011-18-C-0016 ("ECATS") as part of the DARPA */ +/* SSITH research programme. */ +/* */ +/* This project has received funding from the European Research Council */ +/* (ERC) under the European Union’s Horizon 2020 research and innovation */ +/* programme (grant agreement 789108, ELVER). */ +/* */ +/* */ +/* Redistribution and use in source and binary forms, with or without */ +/* modification, are permitted provided that the following conditions */ +/* are met: */ +/* 1. Redistributions of source code must retain the above copyright */ +/* notice, this list of conditions and the following disclaimer. */ +/* 2. Redistributions in binary form must reproduce the above copyright */ +/* notice, this list of conditions and the following disclaimer in */ +/* the documentation and/or other materials provided with the */ +/* distribution. */ +/* */ +/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ +/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ +/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ +/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ +/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ +/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ +/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ +/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ +/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ +/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ +/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ +/* SUCH DAMAGE. */ +/*=======================================================================================*/ + +/* **************************************************************** */ +/* This file implements the floating-point for equal and consumes */ +/* by the softfloat API contract, riscv_softfloat_interface.sail. */ +/* */ +/* The below floating-point types are supported. */ +/* 1. Double-precision, aka 64 bits floating-point. */ +/* 2. Single-precision, aka 32 bits floating-point. */ +/* 3. Half-precision, aka 16 bits floating-point. */ +/* */ +/* However, the implementation still need some global variables in */ +/* file riscv_softfloat_interface.sail. It includes: */ +/* 1. float_result. */ +/* 2. float_fflags. */ +/* 3. float_roundingMode. */ +/* **************************************************************** */ + +val operator == : (bits_S, bits_S) -> bool +val operator | : (bool, bool) -> bool +val operator | : (bits_S, bits_S) -> bits_S +val operator << : (bits_S, int) -> bits_S +val f_is_at_least_one_NaN : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool +val f_is_at_least_one_SNaN : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool + +val riscv_softfloat_f16_eq : (bits_H, bits_H) -> unit +function riscv_softfloat_f16_eq (op1, op2) = { + riscv_softfloat_enter (0b000); + + var result : bits_H = zeros(16); + + if f_is_at_least_one_NaN (op1, op2) then { + if f_is_at_least_one_SNaN (op1, op2) then { + riscv_softfloat_raise_flags (softfloat_flag_invalid); + }; + } else if op1 == op2 | ((op1 | op2) << 1) == zeros(16) then { + result[0] = bitone; + }; + + riscv_softfloat_leave (result); +} + +val riscv_softfloat_f32_eq : (bits_S, bits_S) -> unit +function riscv_softfloat_f32_eq (op1, op2) = { + riscv_softfloat_enter (0b000); + + var result : bits_S = zeros(32); + + if f_is_at_least_one_NaN (op1, op2) then { + if f_is_at_least_one_SNaN (op1, op2) then { + riscv_softfloat_raise_flags (softfloat_flag_invalid); + }; + } else if op1 == op2 | ((op1 | op2) << 1) == zeros(32) then { + result[0] = bitone; + }; + + riscv_softfloat_leave (result); +} + +val riscv_softfloat_f64_eq : (bits_D, bits_D) -> unit +function riscv_softfloat_f64_eq (op1, op2) = { + riscv_softfloat_enter (0b000); + + var result : bits_D = zeros(64); + + if f_is_at_least_one_NaN (op1, op2) then { + if f_is_at_least_one_SNaN (op1, op2) then { + riscv_softfloat_raise_flags (softfloat_flag_invalid); + }; + } else if op1 == op2 | ((op1 | op2) & 0x7fffffffffffffff) == zeros(64) then { + result[0] = bitone; + }; + + riscv_softfloat_leave (result); +} + +val riscv_softfloat_eq : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> unit +function riscv_softfloat_eq (op1, op2) = { + match 'm { + 16 => riscv_softfloat_f16_eq(op1, op2), + 32 => riscv_softfloat_f32_eq(op1, op2), + 64 => riscv_softfloat_f64_eq(op1, op2), + } +} diff --git a/sail-riscv.install b/sail-riscv.install index 7a539dfb5..ca2c7519e 100644 --- a/sail-riscv.install +++ b/sail-riscv.install @@ -1,2 +1,2 @@ bin: ["c_emulator/riscv_sim_RV64" "c_emulator/riscv_sim_RV32"] -share: [ "model/main.sail" {"model/main.sail"} "model/prelude.sail" {"model/prelude.sail"} "model/prelude_mem.sail" {"model/prelude_mem.sail"} "model/prelude_mem_metadata.sail" {"model/prelude_mem_metadata.sail"} "model/riscv_addr_checks.sail" {"model/riscv_addr_checks.sail"} "model/riscv_addr_checks_common.sail" {"model/riscv_addr_checks_common.sail"} "model/riscv_analysis.sail" {"model/riscv_analysis.sail"} "model/riscv_csr_ext.sail" {"model/riscv_csr_ext.sail"} "model/riscv_csr_map.sail" {"model/riscv_csr_map.sail"} "model/riscv_decode_ext.sail" {"model/riscv_decode_ext.sail"} "model/riscv_ext_regs.sail" {"model/riscv_ext_regs.sail"} "model/riscv_fdext_control.sail" {"model/riscv_fdext_control.sail"} "model/riscv_fdext_regs.sail" {"model/riscv_fdext_regs.sail"} "model/riscv_fetch.sail" {"model/riscv_fetch.sail"} "model/riscv_fetch_rvfi.sail" {"model/riscv_fetch_rvfi.sail"} "model/riscv_flen_D.sail" {"model/riscv_flen_D.sail"} "model/riscv_flen_F.sail" {"model/riscv_flen_F.sail"} "model/riscv_freg_type.sail" {"model/riscv_freg_type.sail"} "model/riscv_insts_aext.sail" {"model/riscv_insts_aext.sail"} "model/riscv_insts_base.sail" {"model/riscv_insts_base.sail"} "model/riscv_insts_begin.sail" {"model/riscv_insts_begin.sail"} "model/riscv_insts_cdext.sail" {"model/riscv_insts_cdext.sail"} "model/riscv_insts_cext.sail" {"model/riscv_insts_cext.sail"} "model/riscv_insts_cfext.sail" {"model/riscv_insts_cfext.sail"} "model/riscv_insts_dext.sail" {"model/riscv_insts_dext.sail"} "model/riscv_insts_end.sail" {"model/riscv_insts_end.sail"} "model/riscv_insts_fext.sail" {"model/riscv_insts_fext.sail"} "model/riscv_insts_hints.sail" {"model/riscv_insts_hints.sail"} "model/riscv_insts_mext.sail" {"model/riscv_insts_mext.sail"} "model/riscv_insts_next.sail" {"model/riscv_insts_next.sail"} "model/riscv_insts_rmem.sail" {"model/riscv_insts_rmem.sail"} "model/riscv_insts_zba.sail" {"model/riscv_insts_zba.sail"} "model/riscv_insts_zbb.sail" {"model/riscv_insts_zbb.sail"} "model/riscv_insts_zbc.sail" {"model/riscv_insts_zbc.sail"} "model/riscv_insts_zbkb.sail" {"model/riscv_insts_zbkb.sail"} "model/riscv_insts_zbkx.sail" {"model/riscv_insts_zbkx.sail"} "model/riscv_insts_zbs.sail" {"model/riscv_insts_zbs.sail"} "model/riscv_insts_zfh.sail" {"model/riscv_insts_zfh.sail"} "model/riscv_insts_zicsr.sail" {"model/riscv_insts_zicsr.sail"} "model/riscv_insts_zkn.sail" {"model/riscv_insts_zkn.sail"} "model/riscv_insts_zks.sail" {"model/riscv_insts_zks.sail"} "model/riscv_jalr_rmem.sail" {"model/riscv_jalr_rmem.sail"} "model/riscv_jalr_seq.sail" {"model/riscv_jalr_seq.sail"} "model/riscv_mem.sail" {"model/riscv_mem.sail"} "model/riscv_misa_ext.sail" {"model/riscv_misa_ext.sail"} "model/riscv_next_control.sail" {"model/riscv_next_control.sail"} "model/riscv_next_regs.sail" {"model/riscv_next_regs.sail"} "model/riscv_pc_access.sail" {"model/riscv_pc_access.sail"} "model/riscv_platform.sail" {"model/riscv_platform.sail"} "model/riscv_pmp_control.sail" {"model/riscv_pmp_control.sail"} "model/riscv_pmp_regs.sail" {"model/riscv_pmp_regs.sail"} "model/riscv_pte.sail" {"model/riscv_pte.sail"} "model/riscv_ptw.sail" {"model/riscv_ptw.sail"} "model/riscv_reg_type.sail" {"model/riscv_reg_type.sail"} "model/riscv_regs.sail" {"model/riscv_regs.sail"} "model/riscv_softfloat_interface.sail" {"model/riscv_softfloat_interface.sail"} "model/riscv_step.sail" {"model/riscv_step.sail"} "model/riscv_step_common.sail" {"model/riscv_step_common.sail"} "model/riscv_step_ext.sail" {"model/riscv_step_ext.sail"} "model/riscv_step_rvfi.sail" {"model/riscv_step_rvfi.sail"} "model/riscv_sync_exception.sail" {"model/riscv_sync_exception.sail"} "model/riscv_sys_control.sail" {"model/riscv_sys_control.sail"} "model/riscv_sys_exceptions.sail" {"model/riscv_sys_exceptions.sail"} "model/riscv_sys_regs.sail" {"model/riscv_sys_regs.sail"} "model/riscv_termination_common.sail" {"model/riscv_termination_common.sail"} "model/riscv_termination_rv32.sail" {"model/riscv_termination_rv32.sail"} "model/riscv_termination_rv64.sail" {"model/riscv_termination_rv64.sail"} "model/riscv_types.sail" {"model/riscv_types.sail"} "model/riscv_types_common.sail" {"model/riscv_types_common.sail"} "model/riscv_types_ext.sail" {"model/riscv_types_ext.sail"} "model/riscv_types_kext.sail" {"model/riscv_types_kext.sail"} "model/riscv_vmem_common.sail" {"model/riscv_vmem_common.sail"} "model/riscv_vmem_rv32.sail" {"model/riscv_vmem_rv32.sail"} "model/riscv_vmem_rv64.sail" {"model/riscv_vmem_rv64.sail"} "model/riscv_vmem_sv32.sail" {"model/riscv_vmem_sv32.sail"} "model/riscv_vmem_sv39.sail" {"model/riscv_vmem_sv39.sail"} "model/riscv_vmem_sv48.sail" {"model/riscv_vmem_sv48.sail"} "model/riscv_vmem_tlb.sail" {"model/riscv_vmem_tlb.sail"} "model/riscv_vmem_types.sail" {"model/riscv_vmem_types.sail"} "model/riscv_xlen32.sail" {"model/riscv_xlen32.sail"} "model/riscv_xlen64.sail" {"model/riscv_xlen64.sail"} "model/rvfi_dii.sail" {"model/rvfi_dii.sail"} "c_emulator/riscv_platform.c" {"c_emulator/riscv_platform.c"} "c_emulator/riscv_platform_impl.c" {"c_emulator/riscv_platform_impl.c"} "c_emulator/riscv_prelude.c" {"c_emulator/riscv_prelude.c"} "c_emulator/riscv_sim.c" {"c_emulator/riscv_sim.c"} "c_emulator/riscv_softfloat.c" {"c_emulator/riscv_softfloat.c"} "c_emulator/riscv_config.h" {"c_emulator/riscv_config.h"} "c_emulator/riscv_platform.h" {"c_emulator/riscv_platform.h"} "c_emulator/riscv_platform_impl.h" {"c_emulator/riscv_platform_impl.h"} "c_emulator/riscv_prelude.h" {"c_emulator/riscv_prelude.h"} "c_emulator/riscv_sail.h" {"c_emulator/riscv_sail.h"} "c_emulator/riscv_softfloat.h" {"c_emulator/riscv_softfloat.h"} "handwritten_support/mem_metadata.lem" {"handwritten_support/mem_metadata.lem"} "handwritten_support/riscv_extras.lem" {"handwritten_support/riscv_extras.lem"} "handwritten_support/riscv_extras_fdext.lem" {"handwritten_support/riscv_extras_fdext.lem"} "handwritten_support/riscv_extras_sequential.lem" {"handwritten_support/riscv_extras_sequential.lem"} "handwritten_support/hgen/ast.hgen" {"handwritten_support/hgen/ast.hgen"} "handwritten_support/hgen/fold.hgen" {"handwritten_support/hgen/fold.hgen"} "handwritten_support/hgen/herdtools_ast_to_shallow_ast.hgen" {"handwritten_support/hgen/herdtools_ast_to_shallow_ast.hgen"} "handwritten_support/hgen/herdtools_types_to_shallow_types.hgen" {"handwritten_support/hgen/herdtools_types_to_shallow_types.hgen"} "handwritten_support/hgen/lexer.hgen" {"handwritten_support/hgen/lexer.hgen"} "handwritten_support/hgen/lexer_regexps.hgen" {"handwritten_support/hgen/lexer_regexps.hgen"} "handwritten_support/hgen/map.hgen" {"handwritten_support/hgen/map.hgen"} "handwritten_support/hgen/parser.hgen" {"handwritten_support/hgen/parser.hgen"} "handwritten_support/hgen/pretty.hgen" {"handwritten_support/hgen/pretty.hgen"} "handwritten_support/hgen/pretty_xml.hgen" {"handwritten_support/hgen/pretty_xml.hgen"} "handwritten_support/hgen/sail_trans_out.hgen" {"handwritten_support/hgen/sail_trans_out.hgen"} "handwritten_support/hgen/shallow_ast_to_herdtools_ast.hgen" {"handwritten_support/hgen/shallow_ast_to_herdtools_ast.hgen"} "handwritten_support/hgen/shallow_types_to_herdtools_types.hgen" {"handwritten_support/hgen/shallow_types_to_herdtools_types.hgen"} "handwritten_support/hgen/token_types.hgen" {"handwritten_support/hgen/token_types.hgen"} "handwritten_support/hgen/tokens.hgen" {"handwritten_support/hgen/tokens.hgen"} "handwritten_support/hgen/trans_sail.hgen" {"handwritten_support/hgen/trans_sail.hgen"} "handwritten_support/hgen/types.hgen" {"handwritten_support/hgen/types.hgen"} "handwritten_support/hgen/types_sail_trans_out.hgen" {"handwritten_support/hgen/types_sail_trans_out.hgen"} "handwritten_support/hgen/types_trans_sail.hgen" {"handwritten_support/hgen/types_trans_sail.hgen"} "handwritten_support/0.11/mem_metadata.lem" {"handwritten_support/0.11/mem_metadata.lem"} "handwritten_support/0.11/riscv_extras.lem" {"handwritten_support/0.11/riscv_extras.lem"} "handwritten_support/0.11/riscv_extras_fdext.lem" {"handwritten_support/0.11/riscv_extras_fdext.lem"} "handwritten_support/0.11/riscv_extras_sequential.lem" {"handwritten_support/0.11/riscv_extras_sequential.lem"} "generated_definitions/for-rmem/riscv.lem" {"generated_definitions/for-rmem/riscv.lem"} "generated_definitions/for-rmem/riscv_types.lem" {"generated_definitions/for-rmem/riscv_types.lem"} "generated_definitions/for-rmem/riscv_toFromInterp2.ml" {"generated_definitions/for-rmem/riscv_toFromInterp2.ml"} "generated_definitions/for-rmem/riscv.defs" {"generated_definitions/for-rmem/riscv.defs"} ] +share: [ "model/main.sail" {"model/main.sail"} "model/prelude.sail" {"model/prelude.sail"} "model/prelude_mem.sail" {"model/prelude_mem.sail"} "model/prelude_mem_metadata.sail" {"model/prelude_mem_metadata.sail"} "model/riscv_addr_checks.sail" {"model/riscv_addr_checks.sail"} "model/riscv_addr_checks_common.sail" {"model/riscv_addr_checks_common.sail"} "model/riscv_analysis.sail" {"model/riscv_analysis.sail"} "model/riscv_csr_ext.sail" {"model/riscv_csr_ext.sail"} "model/riscv_csr_map.sail" {"model/riscv_csr_map.sail"} "model/riscv_decode_ext.sail" {"model/riscv_decode_ext.sail"} "model/riscv_ext_regs.sail" {"model/riscv_ext_regs.sail"} "model/riscv_fdext_control.sail" {"model/riscv_fdext_control.sail"} "model/riscv_fdext_regs.sail" {"model/riscv_fdext_regs.sail"} "model/riscv_fetch.sail" {"model/riscv_fetch.sail"} "model/riscv_fetch_rvfi.sail" {"model/riscv_fetch_rvfi.sail"} "model/riscv_flen_D.sail" {"model/riscv_flen_D.sail"} "model/riscv_flen_F.sail" {"model/riscv_flen_F.sail"} "model/riscv_freg_type.sail" {"model/riscv_freg_type.sail"} "model/riscv_insts_aext.sail" {"model/riscv_insts_aext.sail"} "model/riscv_insts_base.sail" {"model/riscv_insts_base.sail"} "model/riscv_insts_begin.sail" {"model/riscv_insts_begin.sail"} "model/riscv_insts_cdext.sail" {"model/riscv_insts_cdext.sail"} "model/riscv_insts_cext.sail" {"model/riscv_insts_cext.sail"} "model/riscv_insts_cfext.sail" {"model/riscv_insts_cfext.sail"} "model/riscv_insts_dext.sail" {"model/riscv_insts_dext.sail"} "model/riscv_insts_end.sail" {"model/riscv_insts_end.sail"} "model/riscv_insts_fext.sail" {"model/riscv_insts_fext.sail"} "model/riscv_insts_hints.sail" {"model/riscv_insts_hints.sail"} "model/riscv_insts_mext.sail" {"model/riscv_insts_mext.sail"} "model/riscv_insts_next.sail" {"model/riscv_insts_next.sail"} "model/riscv_insts_rmem.sail" {"model/riscv_insts_rmem.sail"} "model/riscv_insts_zba.sail" {"model/riscv_insts_zba.sail"} "model/riscv_insts_zbb.sail" {"model/riscv_insts_zbb.sail"} "model/riscv_insts_zbc.sail" {"model/riscv_insts_zbc.sail"} "model/riscv_insts_zbkb.sail" {"model/riscv_insts_zbkb.sail"} "model/riscv_insts_zbkx.sail" {"model/riscv_insts_zbkx.sail"} "model/riscv_insts_zbs.sail" {"model/riscv_insts_zbs.sail"} "model/riscv_insts_zfh.sail" {"model/riscv_insts_zfh.sail"} "model/riscv_insts_zicsr.sail" {"model/riscv_insts_zicsr.sail"} "model/riscv_insts_zkn.sail" {"model/riscv_insts_zkn.sail"} "model/riscv_insts_zks.sail" {"model/riscv_insts_zks.sail"} "model/riscv_jalr_rmem.sail" {"model/riscv_jalr_rmem.sail"} "model/riscv_jalr_seq.sail" {"model/riscv_jalr_seq.sail"} "model/riscv_mem.sail" {"model/riscv_mem.sail"} "model/riscv_misa_ext.sail" {"model/riscv_misa_ext.sail"} "model/riscv_next_control.sail" {"model/riscv_next_control.sail"} "model/riscv_next_regs.sail" {"model/riscv_next_regs.sail"} "model/riscv_pc_access.sail" {"model/riscv_pc_access.sail"} "model/riscv_platform.sail" {"model/riscv_platform.sail"} "model/riscv_pmp_control.sail" {"model/riscv_pmp_control.sail"} "model/riscv_pmp_regs.sail" {"model/riscv_pmp_regs.sail"} "model/riscv_pte.sail" {"model/riscv_pte.sail"} "model/riscv_ptw.sail" {"model/riscv_ptw.sail"} "model/riscv_reg_type.sail" {"model/riscv_reg_type.sail"} "model/riscv_regs.sail" {"model/riscv_regs.sail"} "model/softfloat/riscv_softfloat_common.sail" {"model/softfloat/riscv_softfloat_common.sail"} "model/softfloat/riscv_softfloat_eq.sail" {"model/softfloat/riscv_softfloat_eq.sail"} "model/riscv_softfloat_interface.sail" {"model/riscv_softfloat_interface.sail"} "model/riscv_step.sail" {"model/riscv_step.sail"} "model/riscv_step_common.sail" {"model/riscv_step_common.sail"} "model/riscv_step_ext.sail" {"model/riscv_step_ext.sail"} "model/riscv_step_rvfi.sail" {"model/riscv_step_rvfi.sail"} "model/riscv_sync_exception.sail" {"model/riscv_sync_exception.sail"} "model/riscv_sys_control.sail" {"model/riscv_sys_control.sail"} "model/riscv_sys_exceptions.sail" {"model/riscv_sys_exceptions.sail"} "model/riscv_sys_regs.sail" {"model/riscv_sys_regs.sail"} "model/riscv_termination_common.sail" {"model/riscv_termination_common.sail"} "model/riscv_termination_rv32.sail" {"model/riscv_termination_rv32.sail"} "model/riscv_termination_rv64.sail" {"model/riscv_termination_rv64.sail"} "model/riscv_types.sail" {"model/riscv_types.sail"} "model/riscv_types_common.sail" {"model/riscv_types_common.sail"} "model/riscv_types_ext.sail" {"model/riscv_types_ext.sail"} "model/riscv_types_kext.sail" {"model/riscv_types_kext.sail"} "model/riscv_vmem_common.sail" {"model/riscv_vmem_common.sail"} "model/riscv_vmem_rv32.sail" {"model/riscv_vmem_rv32.sail"} "model/riscv_vmem_rv64.sail" {"model/riscv_vmem_rv64.sail"} "model/riscv_vmem_sv32.sail" {"model/riscv_vmem_sv32.sail"} "model/riscv_vmem_sv39.sail" {"model/riscv_vmem_sv39.sail"} "model/riscv_vmem_sv48.sail" {"model/riscv_vmem_sv48.sail"} "model/riscv_vmem_tlb.sail" {"model/riscv_vmem_tlb.sail"} "model/riscv_vmem_types.sail" {"model/riscv_vmem_types.sail"} "model/riscv_xlen32.sail" {"model/riscv_xlen32.sail"} "model/riscv_xlen64.sail" {"model/riscv_xlen64.sail"} "model/rvfi_dii.sail" {"model/rvfi_dii.sail"} "c_emulator/riscv_platform.c" {"c_emulator/riscv_platform.c"} "c_emulator/riscv_platform_impl.c" {"c_emulator/riscv_platform_impl.c"} "c_emulator/riscv_prelude.c" {"c_emulator/riscv_prelude.c"} "c_emulator/riscv_sim.c" {"c_emulator/riscv_sim.c"} "c_emulator/riscv_softfloat.c" {"c_emulator/riscv_softfloat.c"} "c_emulator/riscv_config.h" {"c_emulator/riscv_config.h"} "c_emulator/riscv_platform.h" {"c_emulator/riscv_platform.h"} "c_emulator/riscv_platform_impl.h" {"c_emulator/riscv_platform_impl.h"} "c_emulator/riscv_prelude.h" {"c_emulator/riscv_prelude.h"} "c_emulator/riscv_sail.h" {"c_emulator/riscv_sail.h"} "c_emulator/riscv_softfloat.h" {"c_emulator/riscv_softfloat.h"} "handwritten_support/mem_metadata.lem" {"handwritten_support/mem_metadata.lem"} "handwritten_support/riscv_extras.lem" {"handwritten_support/riscv_extras.lem"} "handwritten_support/riscv_extras_fdext.lem" {"handwritten_support/riscv_extras_fdext.lem"} "handwritten_support/riscv_extras_sequential.lem" {"handwritten_support/riscv_extras_sequential.lem"} "handwritten_support/hgen/ast.hgen" {"handwritten_support/hgen/ast.hgen"} "handwritten_support/hgen/fold.hgen" {"handwritten_support/hgen/fold.hgen"} "handwritten_support/hgen/herdtools_ast_to_shallow_ast.hgen" {"handwritten_support/hgen/herdtools_ast_to_shallow_ast.hgen"} "handwritten_support/hgen/herdtools_types_to_shallow_types.hgen" {"handwritten_support/hgen/herdtools_types_to_shallow_types.hgen"} "handwritten_support/hgen/lexer.hgen" {"handwritten_support/hgen/lexer.hgen"} "handwritten_support/hgen/lexer_regexps.hgen" {"handwritten_support/hgen/lexer_regexps.hgen"} "handwritten_support/hgen/map.hgen" {"handwritten_support/hgen/map.hgen"} "handwritten_support/hgen/parser.hgen" {"handwritten_support/hgen/parser.hgen"} "handwritten_support/hgen/pretty.hgen" {"handwritten_support/hgen/pretty.hgen"} "handwritten_support/hgen/pretty_xml.hgen" {"handwritten_support/hgen/pretty_xml.hgen"} "handwritten_support/hgen/sail_trans_out.hgen" {"handwritten_support/hgen/sail_trans_out.hgen"} "handwritten_support/hgen/shallow_ast_to_herdtools_ast.hgen" {"handwritten_support/hgen/shallow_ast_to_herdtools_ast.hgen"} "handwritten_support/hgen/shallow_types_to_herdtools_types.hgen" {"handwritten_support/hgen/shallow_types_to_herdtools_types.hgen"} "handwritten_support/hgen/token_types.hgen" {"handwritten_support/hgen/token_types.hgen"} "handwritten_support/hgen/tokens.hgen" {"handwritten_support/hgen/tokens.hgen"} "handwritten_support/hgen/trans_sail.hgen" {"handwritten_support/hgen/trans_sail.hgen"} "handwritten_support/hgen/types.hgen" {"handwritten_support/hgen/types.hgen"} "handwritten_support/hgen/types_sail_trans_out.hgen" {"handwritten_support/hgen/types_sail_trans_out.hgen"} "handwritten_support/hgen/types_trans_sail.hgen" {"handwritten_support/hgen/types_trans_sail.hgen"} "handwritten_support/0.11/mem_metadata.lem" {"handwritten_support/0.11/mem_metadata.lem"} "handwritten_support/0.11/riscv_extras.lem" {"handwritten_support/0.11/riscv_extras.lem"} "handwritten_support/0.11/riscv_extras_fdext.lem" {"handwritten_support/0.11/riscv_extras_fdext.lem"} "handwritten_support/0.11/riscv_extras_sequential.lem" {"handwritten_support/0.11/riscv_extras_sequential.lem"} "generated_definitions/for-rmem/riscv.lem" {"generated_definitions/for-rmem/riscv.lem"} "generated_definitions/for-rmem/riscv_types.lem" {"generated_definitions/for-rmem/riscv_types.lem"} "generated_definitions/for-rmem/riscv_toFromInterp2.ml" {"generated_definitions/for-rmem/riscv_toFromInterp2.ml"} "generated_definitions/for-rmem/riscv.defs" {"generated_definitions/for-rmem/riscv.defs"} ] From 679565c7d2827f7eb873d412f48d961f9c4a1782 Mon Sep 17 00:00:00 2001 From: Pan Li Date: Wed, 7 Feb 2024 20:20:53 +0800 Subject: [PATCH 2/8] Rename softfloat to float. Signed-off-by: Pan Li --- Makefile | 4 +- .../riscv_float_common.sail} | 43 +++++++++---------- .../riscv_float_eq.sail} | 40 ++++++++--------- model/riscv_softfloat_interface.sail | 12 +++--- sail-riscv.install | 2 +- 5 files changed, 50 insertions(+), 51 deletions(-) rename model/{softfloat/riscv_softfloat_common.sail => float/riscv_float_common.sail} (85%) rename model/{softfloat/riscv_softfloat_eq.sail => float/riscv_float_eq.sail} (89%) diff --git a/Makefile b/Makefile index 123a8ca97..b730adfcb 100644 --- a/Makefile +++ b/Makefile @@ -68,8 +68,8 @@ SAIL_SYS_SRCS += riscv_sys_exceptions.sail # default basic helpers for exceptio SAIL_SYS_SRCS += riscv_sync_exception.sail # define the exception structure used in the model SAIL_SYS_SRCS += riscv_next_control.sail # helpers for the 'N' extension SAIL_SYS_SRCS += riscv_softfloat_interface.sail riscv_fdext_regs.sail riscv_fdext_control.sail -SAIL_SYS_SRCS += softfloat/riscv_softfloat_common.sail -SAIL_SYS_SRCS += softfloat/riscv_softfloat_eq.sail +SAIL_SYS_SRCS += float/riscv_float_common.sail +SAIL_SYS_SRCS += float/riscv_float_eq.sail SAIL_SYS_SRCS += riscv_csr_ext.sail # access to CSR extensions SAIL_SYS_SRCS += riscv_sys_control.sail # general exception handling diff --git a/model/softfloat/riscv_softfloat_common.sail b/model/float/riscv_float_common.sail similarity index 85% rename from model/softfloat/riscv_softfloat_common.sail rename to model/float/riscv_float_common.sail index 820ea2f17..34690992d 100644 --- a/model/softfloat/riscv_softfloat_common.sail +++ b/model/float/riscv_float_common.sail @@ -71,8 +71,7 @@ /* **************************************************************** */ /* This file implements the floating-point for some common helper */ -/* functions. They will be leveraged by other softfloat sail */ -/* implementations. */ +/* functions. They will be leveraged by other float sail implement */ /* */ /* However, the implementation still need some global variables in */ /* file riscv_softfloat_interface.sail. It includes: */ @@ -81,43 +80,43 @@ /* 3. float_roundingMode. */ /* **************************************************************** */ -let softfloat_flag_inexact : bits(64) = 0x0000000000000001 -let softfloat_flag_underflow : bits(64) = 0x0000000000000002 -let softfloat_flag_overflow : bits(64) = 0x0000000000000004 -let softfloat_flag_infinit : bits(64) = 0x0000000000000008 -let softfloat_flag_invalid : bits(64) = 0x0000000000000010 +let float_flag_inexact : bits(64) = 0x0000000000000001 +let float_flag_underflow : bits(64) = 0x0000000000000002 +let float_flag_overflow : bits(64) = 0x0000000000000004 +let float_flag_infinit : bits(64) = 0x0000000000000008 +let float_flag_invalid : bits(64) = 0x0000000000000010 -val riscv_softfloat_enter : (bits_rm) -> unit -function riscv_softfloat_enter (roundingMode) -> unit = { +val riscv_float_enter : (bits_rm) -> unit +function riscv_float_enter (roundingMode) -> unit = { float_fflags = zeros(64); float_roundingMode = roundingMode; } -val riscv_softfloat_bits_H_leave : (bits_H) -> unit -function riscv_softfloat_bits_H_leave (result) -> unit = { +val riscv_float_bits_H_leave : (bits_H) -> unit +function riscv_float_bits_H_leave (result) -> unit = { float_result[15 .. 0] = result; } -val riscv_softfloat_bits_S_leave : (bits_S) -> unit -function riscv_softfloat_bits_S_leave (result) -> unit = { +val riscv_float_bits_S_leave : (bits_S) -> unit +function riscv_float_bits_S_leave (result) -> unit = { float_result[31 .. 0] = result; } -val riscv_softfloat_bits_D_leave : (bits_D) -> unit -function riscv_softfloat_bits_D_leave (result) -> unit = { +val riscv_float_bits_D_leave : (bits_D) -> unit +function riscv_float_bits_D_leave (result) -> unit = { float_result[63 .. 0] = result; } -val riscv_softfloat_leave : forall 'm, 'm in {16, 32, 64}. bits('m) -> unit -function riscv_softfloat_leave (op) = { +val riscv_float_leave : forall 'm, 'm in {16, 32, 64}. bits('m) -> unit +function riscv_float_leave (op) = { match 'm { - 16 => riscv_softfloat_bits_H_leave(op), - 32 => riscv_softfloat_bits_S_leave(op), - 64 => riscv_softfloat_bits_D_leave(op), + 16 => riscv_float_bits_H_leave(op), + 32 => riscv_float_bits_S_leave(op), + 64 => riscv_float_bits_D_leave(op), } } -val riscv_softfloat_raise_flags : (bits(64)) -> unit -function riscv_softfloat_raise_flags (flags) -> unit = { +val riscv_float_raise_flags : (bits(64)) -> unit +function riscv_float_raise_flags (flags) -> unit = { float_fflags = float_fflags | flags } diff --git a/model/softfloat/riscv_softfloat_eq.sail b/model/float/riscv_float_eq.sail similarity index 89% rename from model/softfloat/riscv_softfloat_eq.sail rename to model/float/riscv_float_eq.sail index 4ac5305d6..9a95413b2 100644 --- a/model/softfloat/riscv_softfloat_eq.sail +++ b/model/float/riscv_float_eq.sail @@ -92,62 +92,62 @@ val operator << : (bits_S, int) -> bits_S val f_is_at_least_one_NaN : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool val f_is_at_least_one_SNaN : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool -val riscv_softfloat_f16_eq : (bits_H, bits_H) -> unit -function riscv_softfloat_f16_eq (op1, op2) = { - riscv_softfloat_enter (0b000); +val riscv_float_f16_eq : (bits_H, bits_H) -> unit +function riscv_float_f16_eq (op1, op2) = { + riscv_float_enter (0b000); var result : bits_H = zeros(16); if f_is_at_least_one_NaN (op1, op2) then { if f_is_at_least_one_SNaN (op1, op2) then { - riscv_softfloat_raise_flags (softfloat_flag_invalid); + riscv_float_raise_flags (float_flag_invalid); }; } else if op1 == op2 | ((op1 | op2) << 1) == zeros(16) then { result[0] = bitone; }; - riscv_softfloat_leave (result); + riscv_float_leave (result); } -val riscv_softfloat_f32_eq : (bits_S, bits_S) -> unit -function riscv_softfloat_f32_eq (op1, op2) = { - riscv_softfloat_enter (0b000); +val riscv_float_f32_eq : (bits_S, bits_S) -> unit +function riscv_float_f32_eq (op1, op2) = { + riscv_float_enter (0b000); var result : bits_S = zeros(32); if f_is_at_least_one_NaN (op1, op2) then { if f_is_at_least_one_SNaN (op1, op2) then { - riscv_softfloat_raise_flags (softfloat_flag_invalid); + riscv_float_raise_flags (float_flag_invalid); }; } else if op1 == op2 | ((op1 | op2) << 1) == zeros(32) then { result[0] = bitone; }; - riscv_softfloat_leave (result); + riscv_float_leave (result); } -val riscv_softfloat_f64_eq : (bits_D, bits_D) -> unit -function riscv_softfloat_f64_eq (op1, op2) = { - riscv_softfloat_enter (0b000); +val riscv_float_f64_eq : (bits_D, bits_D) -> unit +function riscv_float_f64_eq (op1, op2) = { + riscv_float_enter (0b000); var result : bits_D = zeros(64); if f_is_at_least_one_NaN (op1, op2) then { if f_is_at_least_one_SNaN (op1, op2) then { - riscv_softfloat_raise_flags (softfloat_flag_invalid); + riscv_float_raise_flags (float_flag_invalid); }; } else if op1 == op2 | ((op1 | op2) & 0x7fffffffffffffff) == zeros(64) then { result[0] = bitone; }; - riscv_softfloat_leave (result); + riscv_float_leave (result); } -val riscv_softfloat_eq : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> unit -function riscv_softfloat_eq (op1, op2) = { +val riscv_float_eq : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> unit +function riscv_float_eq (op1, op2) = { match 'm { - 16 => riscv_softfloat_f16_eq(op1, op2), - 32 => riscv_softfloat_f32_eq(op1, op2), - 64 => riscv_softfloat_f64_eq(op1, op2), + 16 => riscv_float_f16_eq(op1, op2), + 32 => riscv_float_f32_eq(op1, op2), + 64 => riscv_float_f64_eq(op1, op2), } } diff --git a/model/riscv_softfloat_interface.sail b/model/riscv_softfloat_interface.sail index 509b03deb..81673cd7a 100644 --- a/model/riscv_softfloat_interface.sail +++ b/model/riscv_softfloat_interface.sail @@ -487,10 +487,10 @@ function riscv_f16Le_quiet (v1, v2) = { (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } -val riscv_softfloat_eq : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> unit +val riscv_float_eq : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> unit val riscv_f16Eq : (bits_H, bits_H) -> (bits_fflags, bool) function riscv_f16Eq (v1, v2) = { - riscv_softfloat_eq (v1, v2); + riscv_float_eq (v1, v2); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } @@ -522,10 +522,10 @@ function riscv_f32Le_quiet (v1, v2) = { (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } -val riscv_softfloat_eq : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> unit +val riscv_float_eq : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> unit val riscv_f32Eq : (bits_S, bits_S) -> (bits_fflags, bool) function riscv_f32Eq (v1, v2) = { - riscv_softfloat_eq (v1, v2); + riscv_float_eq (v1, v2); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } @@ -557,10 +557,10 @@ function riscv_f64Le_quiet (v1, v2) = { (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } -val riscv_softfloat_eq : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> unit +val riscv_float_eq : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> unit val riscv_f64Eq : (bits_D, bits_D) -> (bits_fflags, bool) function riscv_f64Eq (v1, v2) = { - riscv_softfloat_eq (v1, v2); + riscv_float_eq (v1, v2); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } diff --git a/sail-riscv.install b/sail-riscv.install index ca2c7519e..99978c4e4 100644 --- a/sail-riscv.install +++ b/sail-riscv.install @@ -1,2 +1,2 @@ bin: ["c_emulator/riscv_sim_RV64" "c_emulator/riscv_sim_RV32"] -share: [ "model/main.sail" {"model/main.sail"} "model/prelude.sail" {"model/prelude.sail"} "model/prelude_mem.sail" {"model/prelude_mem.sail"} "model/prelude_mem_metadata.sail" {"model/prelude_mem_metadata.sail"} "model/riscv_addr_checks.sail" {"model/riscv_addr_checks.sail"} "model/riscv_addr_checks_common.sail" {"model/riscv_addr_checks_common.sail"} "model/riscv_analysis.sail" {"model/riscv_analysis.sail"} "model/riscv_csr_ext.sail" {"model/riscv_csr_ext.sail"} "model/riscv_csr_map.sail" {"model/riscv_csr_map.sail"} "model/riscv_decode_ext.sail" {"model/riscv_decode_ext.sail"} "model/riscv_ext_regs.sail" {"model/riscv_ext_regs.sail"} "model/riscv_fdext_control.sail" {"model/riscv_fdext_control.sail"} "model/riscv_fdext_regs.sail" {"model/riscv_fdext_regs.sail"} "model/riscv_fetch.sail" {"model/riscv_fetch.sail"} "model/riscv_fetch_rvfi.sail" {"model/riscv_fetch_rvfi.sail"} "model/riscv_flen_D.sail" {"model/riscv_flen_D.sail"} "model/riscv_flen_F.sail" {"model/riscv_flen_F.sail"} "model/riscv_freg_type.sail" {"model/riscv_freg_type.sail"} "model/riscv_insts_aext.sail" {"model/riscv_insts_aext.sail"} "model/riscv_insts_base.sail" {"model/riscv_insts_base.sail"} "model/riscv_insts_begin.sail" {"model/riscv_insts_begin.sail"} "model/riscv_insts_cdext.sail" {"model/riscv_insts_cdext.sail"} "model/riscv_insts_cext.sail" {"model/riscv_insts_cext.sail"} "model/riscv_insts_cfext.sail" {"model/riscv_insts_cfext.sail"} "model/riscv_insts_dext.sail" {"model/riscv_insts_dext.sail"} "model/riscv_insts_end.sail" {"model/riscv_insts_end.sail"} "model/riscv_insts_fext.sail" {"model/riscv_insts_fext.sail"} "model/riscv_insts_hints.sail" {"model/riscv_insts_hints.sail"} "model/riscv_insts_mext.sail" {"model/riscv_insts_mext.sail"} "model/riscv_insts_next.sail" {"model/riscv_insts_next.sail"} "model/riscv_insts_rmem.sail" {"model/riscv_insts_rmem.sail"} "model/riscv_insts_zba.sail" {"model/riscv_insts_zba.sail"} "model/riscv_insts_zbb.sail" {"model/riscv_insts_zbb.sail"} "model/riscv_insts_zbc.sail" {"model/riscv_insts_zbc.sail"} "model/riscv_insts_zbkb.sail" {"model/riscv_insts_zbkb.sail"} "model/riscv_insts_zbkx.sail" {"model/riscv_insts_zbkx.sail"} "model/riscv_insts_zbs.sail" {"model/riscv_insts_zbs.sail"} "model/riscv_insts_zfh.sail" {"model/riscv_insts_zfh.sail"} "model/riscv_insts_zicsr.sail" {"model/riscv_insts_zicsr.sail"} "model/riscv_insts_zkn.sail" {"model/riscv_insts_zkn.sail"} "model/riscv_insts_zks.sail" {"model/riscv_insts_zks.sail"} "model/riscv_jalr_rmem.sail" {"model/riscv_jalr_rmem.sail"} "model/riscv_jalr_seq.sail" {"model/riscv_jalr_seq.sail"} "model/riscv_mem.sail" {"model/riscv_mem.sail"} "model/riscv_misa_ext.sail" {"model/riscv_misa_ext.sail"} "model/riscv_next_control.sail" {"model/riscv_next_control.sail"} "model/riscv_next_regs.sail" {"model/riscv_next_regs.sail"} "model/riscv_pc_access.sail" {"model/riscv_pc_access.sail"} "model/riscv_platform.sail" {"model/riscv_platform.sail"} "model/riscv_pmp_control.sail" {"model/riscv_pmp_control.sail"} "model/riscv_pmp_regs.sail" {"model/riscv_pmp_regs.sail"} "model/riscv_pte.sail" {"model/riscv_pte.sail"} "model/riscv_ptw.sail" {"model/riscv_ptw.sail"} "model/riscv_reg_type.sail" {"model/riscv_reg_type.sail"} "model/riscv_regs.sail" {"model/riscv_regs.sail"} "model/softfloat/riscv_softfloat_common.sail" {"model/softfloat/riscv_softfloat_common.sail"} "model/softfloat/riscv_softfloat_eq.sail" {"model/softfloat/riscv_softfloat_eq.sail"} "model/riscv_softfloat_interface.sail" {"model/riscv_softfloat_interface.sail"} "model/riscv_step.sail" {"model/riscv_step.sail"} "model/riscv_step_common.sail" {"model/riscv_step_common.sail"} "model/riscv_step_ext.sail" {"model/riscv_step_ext.sail"} "model/riscv_step_rvfi.sail" {"model/riscv_step_rvfi.sail"} "model/riscv_sync_exception.sail" {"model/riscv_sync_exception.sail"} "model/riscv_sys_control.sail" {"model/riscv_sys_control.sail"} "model/riscv_sys_exceptions.sail" {"model/riscv_sys_exceptions.sail"} "model/riscv_sys_regs.sail" {"model/riscv_sys_regs.sail"} "model/riscv_termination_common.sail" {"model/riscv_termination_common.sail"} "model/riscv_termination_rv32.sail" {"model/riscv_termination_rv32.sail"} "model/riscv_termination_rv64.sail" {"model/riscv_termination_rv64.sail"} "model/riscv_types.sail" {"model/riscv_types.sail"} "model/riscv_types_common.sail" {"model/riscv_types_common.sail"} "model/riscv_types_ext.sail" {"model/riscv_types_ext.sail"} "model/riscv_types_kext.sail" {"model/riscv_types_kext.sail"} "model/riscv_vmem_common.sail" {"model/riscv_vmem_common.sail"} "model/riscv_vmem_rv32.sail" {"model/riscv_vmem_rv32.sail"} "model/riscv_vmem_rv64.sail" {"model/riscv_vmem_rv64.sail"} "model/riscv_vmem_sv32.sail" {"model/riscv_vmem_sv32.sail"} "model/riscv_vmem_sv39.sail" {"model/riscv_vmem_sv39.sail"} "model/riscv_vmem_sv48.sail" {"model/riscv_vmem_sv48.sail"} "model/riscv_vmem_tlb.sail" {"model/riscv_vmem_tlb.sail"} "model/riscv_vmem_types.sail" {"model/riscv_vmem_types.sail"} "model/riscv_xlen32.sail" {"model/riscv_xlen32.sail"} "model/riscv_xlen64.sail" {"model/riscv_xlen64.sail"} "model/rvfi_dii.sail" {"model/rvfi_dii.sail"} "c_emulator/riscv_platform.c" {"c_emulator/riscv_platform.c"} "c_emulator/riscv_platform_impl.c" {"c_emulator/riscv_platform_impl.c"} "c_emulator/riscv_prelude.c" {"c_emulator/riscv_prelude.c"} "c_emulator/riscv_sim.c" {"c_emulator/riscv_sim.c"} "c_emulator/riscv_softfloat.c" {"c_emulator/riscv_softfloat.c"} "c_emulator/riscv_config.h" {"c_emulator/riscv_config.h"} "c_emulator/riscv_platform.h" {"c_emulator/riscv_platform.h"} "c_emulator/riscv_platform_impl.h" {"c_emulator/riscv_platform_impl.h"} "c_emulator/riscv_prelude.h" {"c_emulator/riscv_prelude.h"} "c_emulator/riscv_sail.h" {"c_emulator/riscv_sail.h"} "c_emulator/riscv_softfloat.h" {"c_emulator/riscv_softfloat.h"} "handwritten_support/mem_metadata.lem" {"handwritten_support/mem_metadata.lem"} "handwritten_support/riscv_extras.lem" {"handwritten_support/riscv_extras.lem"} "handwritten_support/riscv_extras_fdext.lem" {"handwritten_support/riscv_extras_fdext.lem"} "handwritten_support/riscv_extras_sequential.lem" {"handwritten_support/riscv_extras_sequential.lem"} "handwritten_support/hgen/ast.hgen" {"handwritten_support/hgen/ast.hgen"} "handwritten_support/hgen/fold.hgen" {"handwritten_support/hgen/fold.hgen"} "handwritten_support/hgen/herdtools_ast_to_shallow_ast.hgen" {"handwritten_support/hgen/herdtools_ast_to_shallow_ast.hgen"} "handwritten_support/hgen/herdtools_types_to_shallow_types.hgen" {"handwritten_support/hgen/herdtools_types_to_shallow_types.hgen"} "handwritten_support/hgen/lexer.hgen" {"handwritten_support/hgen/lexer.hgen"} "handwritten_support/hgen/lexer_regexps.hgen" {"handwritten_support/hgen/lexer_regexps.hgen"} "handwritten_support/hgen/map.hgen" {"handwritten_support/hgen/map.hgen"} "handwritten_support/hgen/parser.hgen" {"handwritten_support/hgen/parser.hgen"} "handwritten_support/hgen/pretty.hgen" {"handwritten_support/hgen/pretty.hgen"} "handwritten_support/hgen/pretty_xml.hgen" {"handwritten_support/hgen/pretty_xml.hgen"} "handwritten_support/hgen/sail_trans_out.hgen" {"handwritten_support/hgen/sail_trans_out.hgen"} "handwritten_support/hgen/shallow_ast_to_herdtools_ast.hgen" {"handwritten_support/hgen/shallow_ast_to_herdtools_ast.hgen"} "handwritten_support/hgen/shallow_types_to_herdtools_types.hgen" {"handwritten_support/hgen/shallow_types_to_herdtools_types.hgen"} "handwritten_support/hgen/token_types.hgen" {"handwritten_support/hgen/token_types.hgen"} "handwritten_support/hgen/tokens.hgen" {"handwritten_support/hgen/tokens.hgen"} "handwritten_support/hgen/trans_sail.hgen" {"handwritten_support/hgen/trans_sail.hgen"} "handwritten_support/hgen/types.hgen" {"handwritten_support/hgen/types.hgen"} "handwritten_support/hgen/types_sail_trans_out.hgen" {"handwritten_support/hgen/types_sail_trans_out.hgen"} "handwritten_support/hgen/types_trans_sail.hgen" {"handwritten_support/hgen/types_trans_sail.hgen"} "handwritten_support/0.11/mem_metadata.lem" {"handwritten_support/0.11/mem_metadata.lem"} "handwritten_support/0.11/riscv_extras.lem" {"handwritten_support/0.11/riscv_extras.lem"} "handwritten_support/0.11/riscv_extras_fdext.lem" {"handwritten_support/0.11/riscv_extras_fdext.lem"} "handwritten_support/0.11/riscv_extras_sequential.lem" {"handwritten_support/0.11/riscv_extras_sequential.lem"} "generated_definitions/for-rmem/riscv.lem" {"generated_definitions/for-rmem/riscv.lem"} "generated_definitions/for-rmem/riscv_types.lem" {"generated_definitions/for-rmem/riscv_types.lem"} "generated_definitions/for-rmem/riscv_toFromInterp2.ml" {"generated_definitions/for-rmem/riscv_toFromInterp2.ml"} "generated_definitions/for-rmem/riscv.defs" {"generated_definitions/for-rmem/riscv.defs"} ] +share: [ "model/main.sail" {"model/main.sail"} "model/prelude.sail" {"model/prelude.sail"} "model/prelude_mem.sail" {"model/prelude_mem.sail"} "model/prelude_mem_metadata.sail" {"model/prelude_mem_metadata.sail"} "model/riscv_addr_checks.sail" {"model/riscv_addr_checks.sail"} "model/riscv_addr_checks_common.sail" {"model/riscv_addr_checks_common.sail"} "model/riscv_analysis.sail" {"model/riscv_analysis.sail"} "model/riscv_csr_ext.sail" {"model/riscv_csr_ext.sail"} "model/riscv_csr_map.sail" {"model/riscv_csr_map.sail"} "model/riscv_decode_ext.sail" {"model/riscv_decode_ext.sail"} "model/riscv_ext_regs.sail" {"model/riscv_ext_regs.sail"} "model/riscv_fdext_control.sail" {"model/riscv_fdext_control.sail"} "model/riscv_fdext_regs.sail" {"model/riscv_fdext_regs.sail"} "model/riscv_fetch.sail" {"model/riscv_fetch.sail"} "model/riscv_fetch_rvfi.sail" {"model/riscv_fetch_rvfi.sail"} "model/riscv_flen_D.sail" {"model/riscv_flen_D.sail"} "model/riscv_flen_F.sail" {"model/riscv_flen_F.sail"} "model/riscv_freg_type.sail" {"model/riscv_freg_type.sail"} "model/riscv_insts_aext.sail" {"model/riscv_insts_aext.sail"} "model/riscv_insts_base.sail" {"model/riscv_insts_base.sail"} "model/riscv_insts_begin.sail" {"model/riscv_insts_begin.sail"} "model/riscv_insts_cdext.sail" {"model/riscv_insts_cdext.sail"} "model/riscv_insts_cext.sail" {"model/riscv_insts_cext.sail"} "model/riscv_insts_cfext.sail" {"model/riscv_insts_cfext.sail"} "model/riscv_insts_dext.sail" {"model/riscv_insts_dext.sail"} "model/riscv_insts_end.sail" {"model/riscv_insts_end.sail"} "model/riscv_insts_fext.sail" {"model/riscv_insts_fext.sail"} "model/riscv_insts_hints.sail" {"model/riscv_insts_hints.sail"} "model/riscv_insts_mext.sail" {"model/riscv_insts_mext.sail"} "model/riscv_insts_next.sail" {"model/riscv_insts_next.sail"} "model/riscv_insts_rmem.sail" {"model/riscv_insts_rmem.sail"} "model/riscv_insts_zba.sail" {"model/riscv_insts_zba.sail"} "model/riscv_insts_zbb.sail" {"model/riscv_insts_zbb.sail"} "model/riscv_insts_zbc.sail" {"model/riscv_insts_zbc.sail"} "model/riscv_insts_zbkb.sail" {"model/riscv_insts_zbkb.sail"} "model/riscv_insts_zbkx.sail" {"model/riscv_insts_zbkx.sail"} "model/riscv_insts_zbs.sail" {"model/riscv_insts_zbs.sail"} "model/riscv_insts_zfh.sail" {"model/riscv_insts_zfh.sail"} "model/riscv_insts_zicsr.sail" {"model/riscv_insts_zicsr.sail"} "model/riscv_insts_zkn.sail" {"model/riscv_insts_zkn.sail"} "model/riscv_insts_zks.sail" {"model/riscv_insts_zks.sail"} "model/riscv_jalr_rmem.sail" {"model/riscv_jalr_rmem.sail"} "model/riscv_jalr_seq.sail" {"model/riscv_jalr_seq.sail"} "model/riscv_mem.sail" {"model/riscv_mem.sail"} "model/riscv_misa_ext.sail" {"model/riscv_misa_ext.sail"} "model/riscv_next_control.sail" {"model/riscv_next_control.sail"} "model/riscv_next_regs.sail" {"model/riscv_next_regs.sail"} "model/riscv_pc_access.sail" {"model/riscv_pc_access.sail"} "model/riscv_platform.sail" {"model/riscv_platform.sail"} "model/riscv_pmp_control.sail" {"model/riscv_pmp_control.sail"} "model/riscv_pmp_regs.sail" {"model/riscv_pmp_regs.sail"} "model/riscv_pte.sail" {"model/riscv_pte.sail"} "model/riscv_ptw.sail" {"model/riscv_ptw.sail"} "model/riscv_reg_type.sail" {"model/riscv_reg_type.sail"} "model/riscv_regs.sail" {"model/riscv_regs.sail"} "model/float/riscv_float_common.sail" {"model/float/riscv_float_common.sail"} "model/float/riscv_float_eq.sail" {"model/float/riscv_float_eq.sail"} "model/riscv_softfloat_interface.sail" {"model/riscv_softfloat_interface.sail"} "model/riscv_step.sail" {"model/riscv_step.sail"} "model/riscv_step_common.sail" {"model/riscv_step_common.sail"} "model/riscv_step_ext.sail" {"model/riscv_step_ext.sail"} "model/riscv_step_rvfi.sail" {"model/riscv_step_rvfi.sail"} "model/riscv_sync_exception.sail" {"model/riscv_sync_exception.sail"} "model/riscv_sys_control.sail" {"model/riscv_sys_control.sail"} "model/riscv_sys_exceptions.sail" {"model/riscv_sys_exceptions.sail"} "model/riscv_sys_regs.sail" {"model/riscv_sys_regs.sail"} "model/riscv_termination_common.sail" {"model/riscv_termination_common.sail"} "model/riscv_termination_rv32.sail" {"model/riscv_termination_rv32.sail"} "model/riscv_termination_rv64.sail" {"model/riscv_termination_rv64.sail"} "model/riscv_types.sail" {"model/riscv_types.sail"} "model/riscv_types_common.sail" {"model/riscv_types_common.sail"} "model/riscv_types_ext.sail" {"model/riscv_types_ext.sail"} "model/riscv_types_kext.sail" {"model/riscv_types_kext.sail"} "model/riscv_vmem_common.sail" {"model/riscv_vmem_common.sail"} "model/riscv_vmem_rv32.sail" {"model/riscv_vmem_rv32.sail"} "model/riscv_vmem_rv64.sail" {"model/riscv_vmem_rv64.sail"} "model/riscv_vmem_sv32.sail" {"model/riscv_vmem_sv32.sail"} "model/riscv_vmem_sv39.sail" {"model/riscv_vmem_sv39.sail"} "model/riscv_vmem_sv48.sail" {"model/riscv_vmem_sv48.sail"} "model/riscv_vmem_tlb.sail" {"model/riscv_vmem_tlb.sail"} "model/riscv_vmem_types.sail" {"model/riscv_vmem_types.sail"} "model/riscv_xlen32.sail" {"model/riscv_xlen32.sail"} "model/riscv_xlen64.sail" {"model/riscv_xlen64.sail"} "model/rvfi_dii.sail" {"model/rvfi_dii.sail"} "c_emulator/riscv_platform.c" {"c_emulator/riscv_platform.c"} "c_emulator/riscv_platform_impl.c" {"c_emulator/riscv_platform_impl.c"} "c_emulator/riscv_prelude.c" {"c_emulator/riscv_prelude.c"} "c_emulator/riscv_sim.c" {"c_emulator/riscv_sim.c"} "c_emulator/riscv_softfloat.c" {"c_emulator/riscv_softfloat.c"} "c_emulator/riscv_config.h" {"c_emulator/riscv_config.h"} "c_emulator/riscv_platform.h" {"c_emulator/riscv_platform.h"} "c_emulator/riscv_platform_impl.h" {"c_emulator/riscv_platform_impl.h"} "c_emulator/riscv_prelude.h" {"c_emulator/riscv_prelude.h"} "c_emulator/riscv_sail.h" {"c_emulator/riscv_sail.h"} "c_emulator/riscv_softfloat.h" {"c_emulator/riscv_softfloat.h"} "handwritten_support/mem_metadata.lem" {"handwritten_support/mem_metadata.lem"} "handwritten_support/riscv_extras.lem" {"handwritten_support/riscv_extras.lem"} "handwritten_support/riscv_extras_fdext.lem" {"handwritten_support/riscv_extras_fdext.lem"} "handwritten_support/riscv_extras_sequential.lem" {"handwritten_support/riscv_extras_sequential.lem"} "handwritten_support/hgen/ast.hgen" {"handwritten_support/hgen/ast.hgen"} "handwritten_support/hgen/fold.hgen" {"handwritten_support/hgen/fold.hgen"} "handwritten_support/hgen/herdtools_ast_to_shallow_ast.hgen" {"handwritten_support/hgen/herdtools_ast_to_shallow_ast.hgen"} "handwritten_support/hgen/herdtools_types_to_shallow_types.hgen" {"handwritten_support/hgen/herdtools_types_to_shallow_types.hgen"} "handwritten_support/hgen/lexer.hgen" {"handwritten_support/hgen/lexer.hgen"} "handwritten_support/hgen/lexer_regexps.hgen" {"handwritten_support/hgen/lexer_regexps.hgen"} "handwritten_support/hgen/map.hgen" {"handwritten_support/hgen/map.hgen"} "handwritten_support/hgen/parser.hgen" {"handwritten_support/hgen/parser.hgen"} "handwritten_support/hgen/pretty.hgen" {"handwritten_support/hgen/pretty.hgen"} "handwritten_support/hgen/pretty_xml.hgen" {"handwritten_support/hgen/pretty_xml.hgen"} "handwritten_support/hgen/sail_trans_out.hgen" {"handwritten_support/hgen/sail_trans_out.hgen"} "handwritten_support/hgen/shallow_ast_to_herdtools_ast.hgen" {"handwritten_support/hgen/shallow_ast_to_herdtools_ast.hgen"} "handwritten_support/hgen/shallow_types_to_herdtools_types.hgen" {"handwritten_support/hgen/shallow_types_to_herdtools_types.hgen"} "handwritten_support/hgen/token_types.hgen" {"handwritten_support/hgen/token_types.hgen"} "handwritten_support/hgen/tokens.hgen" {"handwritten_support/hgen/tokens.hgen"} "handwritten_support/hgen/trans_sail.hgen" {"handwritten_support/hgen/trans_sail.hgen"} "handwritten_support/hgen/types.hgen" {"handwritten_support/hgen/types.hgen"} "handwritten_support/hgen/types_sail_trans_out.hgen" {"handwritten_support/hgen/types_sail_trans_out.hgen"} "handwritten_support/hgen/types_trans_sail.hgen" {"handwritten_support/hgen/types_trans_sail.hgen"} "handwritten_support/0.11/mem_metadata.lem" {"handwritten_support/0.11/mem_metadata.lem"} "handwritten_support/0.11/riscv_extras.lem" {"handwritten_support/0.11/riscv_extras.lem"} "handwritten_support/0.11/riscv_extras_fdext.lem" {"handwritten_support/0.11/riscv_extras_fdext.lem"} "handwritten_support/0.11/riscv_extras_sequential.lem" {"handwritten_support/0.11/riscv_extras_sequential.lem"} "generated_definitions/for-rmem/riscv.lem" {"generated_definitions/for-rmem/riscv.lem"} "generated_definitions/for-rmem/riscv_types.lem" {"generated_definitions/for-rmem/riscv_types.lem"} "generated_definitions/for-rmem/riscv_toFromInterp2.ml" {"generated_definitions/for-rmem/riscv_toFromInterp2.ml"} "generated_definitions/for-rmem/riscv.defs" {"generated_definitions/for-rmem/riscv.defs"} ] From 7aac8002529ad3f82abcf8fa9e9ac53fd3f304aa Mon Sep 17 00:00:00 2001 From: Pan Li Date: Thu, 8 Feb 2024 10:10:35 +0800 Subject: [PATCH 3/8] Address comments. Signed-off-by: Pan Li --- Makefile | 2 +- model/float/riscv_float_common.sail | 44 +++++++---------- model/float/riscv_float_eq.sail | 72 +++++----------------------- model/riscv_insts_vext_utils.sail | 18 ------- model/riscv_softfloat_interface.sail | 12 ----- 5 files changed, 31 insertions(+), 117 deletions(-) diff --git a/Makefile b/Makefile index b730adfcb..24e97fe45 100644 --- a/Makefile +++ b/Makefile @@ -67,9 +67,9 @@ SAIL_SYS_SRCS += riscv_next_regs.sail SAIL_SYS_SRCS += riscv_sys_exceptions.sail # default basic helpers for exception handling SAIL_SYS_SRCS += riscv_sync_exception.sail # define the exception structure used in the model SAIL_SYS_SRCS += riscv_next_control.sail # helpers for the 'N' extension -SAIL_SYS_SRCS += riscv_softfloat_interface.sail riscv_fdext_regs.sail riscv_fdext_control.sail SAIL_SYS_SRCS += float/riscv_float_common.sail SAIL_SYS_SRCS += float/riscv_float_eq.sail +SAIL_SYS_SRCS += riscv_softfloat_interface.sail riscv_fdext_regs.sail riscv_fdext_control.sail SAIL_SYS_SRCS += riscv_csr_ext.sail # access to CSR extensions SAIL_SYS_SRCS += riscv_sys_control.sail # general exception handling diff --git a/model/float/riscv_float_common.sail b/model/float/riscv_float_common.sail index 34690992d..d55fd74a2 100644 --- a/model/float/riscv_float_common.sail +++ b/model/float/riscv_float_common.sail @@ -73,18 +73,25 @@ /* This file implements the floating-point for some common helper */ /* functions. They will be leveraged by other float sail implement */ /* */ -/* However, the implementation still need some global variables in */ -/* file riscv_softfloat_interface.sail. It includes: */ +/* However, the implementation still need some global variables: */ /* 1. float_result. */ /* 2. float_fflags. */ /* 3. float_roundingMode. */ /* **************************************************************** */ -let float_flag_inexact : bits(64) = 0x0000000000000001 -let float_flag_underflow : bits(64) = 0x0000000000000002 -let float_flag_overflow : bits(64) = 0x0000000000000004 -let float_flag_infinit : bits(64) = 0x0000000000000008 -let float_flag_invalid : bits(64) = 0x0000000000000010 +type bits_rm = bits(3) /* Rounding mode */ + +/* ***************************************************************** */ +/* Internal registers to pass results across the softfloat interface */ +/* to avoid return types involving structures. */ +/* */ +/* Todo: we will consider return the float_result directly in sail. */ +/* ***************************************************************** */ +register float_result : bits(64) +register float_fflags : bits(64) +register float_roundingMode : bits_rm + +let float_flag_invalid : bits(64) = zero_extend (64, 0x10) val riscv_float_enter : (bits_rm) -> unit function riscv_float_enter (roundingMode) -> unit = { @@ -92,27 +99,12 @@ function riscv_float_enter (roundingMode) -> unit = { float_roundingMode = roundingMode; } -val riscv_float_bits_H_leave : (bits_H) -> unit -function riscv_float_bits_H_leave (result) -> unit = { - float_result[15 .. 0] = result; -} - -val riscv_float_bits_S_leave : (bits_S) -> unit -function riscv_float_bits_S_leave (result) -> unit = { - float_result[31 .. 0] = result; -} - -val riscv_float_bits_D_leave : (bits_D) -> unit -function riscv_float_bits_D_leave (result) -> unit = { - float_result[63 .. 0] = result; -} - val riscv_float_leave : forall 'm, 'm in {16, 32, 64}. bits('m) -> unit -function riscv_float_leave (op) = { +function riscv_float_leave (result) -> unit = { match 'm { - 16 => riscv_float_bits_H_leave(op), - 32 => riscv_float_bits_S_leave(op), - 64 => riscv_float_bits_D_leave(op), + 16 => float_result[15 .. 0] = result, + 32 => float_result[31 .. 0] = result, + 64 => float_result[63 .. 0] = result, } } diff --git a/model/float/riscv_float_eq.sail b/model/float/riscv_float_eq.sail index 9a95413b2..03da4b0d3 100644 --- a/model/float/riscv_float_eq.sail +++ b/model/float/riscv_float_eq.sail @@ -79,75 +79,27 @@ /* 3. Half-precision, aka 16 bits floating-point. */ /* */ /* However, the implementation still need some global variables in */ -/* file riscv_softfloat_interface.sail. It includes: */ +/* file riscv_float_common.sail. It includes: */ /* 1. float_result. */ /* 2. float_fflags. */ /* 3. float_roundingMode. */ /* **************************************************************** */ -val operator == : (bits_S, bits_S) -> bool -val operator | : (bool, bool) -> bool -val operator | : (bits_S, bits_S) -> bits_S -val operator << : (bits_S, int) -> bits_S -val f_is_at_least_one_NaN : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool -val f_is_at_least_one_SNaN : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool +val f_is_NaN : forall 'm, 'm in {16, 32, 64}. bits('m) -> bool +val f_is_SNaN : forall 'm, 'm in {16, 32, 64}. bits('m) -> bool -val riscv_float_f16_eq : (bits_H, bits_H) -> unit -function riscv_float_f16_eq (op1, op2) = { - riscv_float_enter (0b000); - - var result : bits_H = zeros(16); - - if f_is_at_least_one_NaN (op1, op2) then { - if f_is_at_least_one_SNaN (op1, op2) then { - riscv_float_raise_flags (float_flag_invalid); - }; - } else if op1 == op2 | ((op1 | op2) << 1) == zeros(16) then { - result[0] = bitone; - }; - - riscv_float_leave (result); -} - -val riscv_float_f32_eq : (bits_S, bits_S) -> unit -function riscv_float_f32_eq (op1, op2) = { - riscv_float_enter (0b000); - - var result : bits_S = zeros(32); - - if f_is_at_least_one_NaN (op1, op2) then { - if f_is_at_least_one_SNaN (op1, op2) then { - riscv_float_raise_flags (float_flag_invalid); - }; - } else if op1 == op2 | ((op1 | op2) << 1) == zeros(32) then { - result[0] = bitone; - }; - - riscv_float_leave (result); -} - -val riscv_float_f64_eq : (bits_D, bits_D) -> unit -function riscv_float_f64_eq (op1, op2) = { +val riscv_float_eq : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> unit +function riscv_float_eq (op1, op2) -> unit = { riscv_float_enter (0b000); - var result : bits_D = zeros(64); + let is_nan : bool = f_is_NaN (op1) | f_is_NaN (op2); + let is_snan : bool = f_is_SNaN (op1) | f_is_SNaN (op2); - if f_is_at_least_one_NaN (op1, op2) then { - if f_is_at_least_one_SNaN (op1, op2) then { - riscv_float_raise_flags (float_flag_invalid); - }; - } else if op1 == op2 | ((op1 | op2) & 0x7fffffffffffffff) == zeros(64) then { - result[0] = bitone; - }; + if is_nan & is_snan then riscv_float_raise_flags (float_flag_invalid); - riscv_float_leave (result); -} + let is_equal : bool = if not(is_nan) + then op1 == op2 | ((op1 | op2) << 1) == zeros() + else false; -val riscv_float_eq : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> unit -function riscv_float_eq (op1, op2) = { - match 'm { - 16 => riscv_float_f16_eq(op1, op2), - 32 => riscv_float_f32_eq(op1, op2), - 64 => riscv_float_f64_eq(op1, op2), - } + riscv_float_leave (zero_extend('m, bool_bits(is_equal))); } diff --git a/model/riscv_insts_vext_utils.sail b/model/riscv_insts_vext_utils.sail index 84ec68119..7b29a0f4f 100755 --- a/model/riscv_insts_vext_utils.sail +++ b/model/riscv_insts_vext_utils.sail @@ -560,15 +560,6 @@ function f_is_SNaN(xf) = { } } -val f_is_at_least_one_SNaN : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool -function f_is_at_least_one_SNaN (op1, op2) = { - match 'm { - 16 => f_is_SNaN_H(op1) | f_is_SNaN_H(op2), - 32 => f_is_SNaN_S(op1) | f_is_SNaN_S(op2), - 64 => f_is_SNaN_D(op1) | f_is_SNaN_D(op2), - } -} - val f_is_QNaN : forall 'm, 'm in {16, 32, 64}. bits('m) -> bool function f_is_QNaN(xf) = { match 'm { @@ -587,15 +578,6 @@ function f_is_NaN(xf) = { } } -val f_is_at_least_one_NaN : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool -function f_is_at_least_one_NaN (op1, op2) = { - match 'm { - 16 => f_is_NaN_H(op1) | f_is_NaN_H(op2), - 32 => f_is_NaN_S(op1) | f_is_NaN_S(op2), - 64 => f_is_NaN_D(op1) | f_is_NaN_D(op2), - } -} - /* Scalar register shaping for floating point operations */ val get_scalar_fp : forall 'n, 'n in {16, 32, 64}. (regidx, int('n)) -> bits('n) function get_scalar_fp(rs1, SEW) = { diff --git a/model/riscv_softfloat_interface.sail b/model/riscv_softfloat_interface.sail index 81673cd7a..fedb5ffb1 100644 --- a/model/riscv_softfloat_interface.sail +++ b/model/riscv_softfloat_interface.sail @@ -87,7 +87,6 @@ /* **************************************************************** */ /* 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_H = bits(16) /* Half-precision float value */ type bits_S = bits(32) /* Single-precision float value */ @@ -99,14 +98,6 @@ 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) -register float_roundingMode : bits_rm - /* **************************************************************** */ /* ADD/SUB/MUL/DIV */ @@ -487,7 +478,6 @@ function riscv_f16Le_quiet (v1, v2) = { (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } -val riscv_float_eq : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> unit val riscv_f16Eq : (bits_H, bits_H) -> (bits_fflags, bool) function riscv_f16Eq (v1, v2) = { riscv_float_eq (v1, v2); @@ -522,7 +512,6 @@ function riscv_f32Le_quiet (v1, v2) = { (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } -val riscv_float_eq : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> unit val riscv_f32Eq : (bits_S, bits_S) -> (bits_fflags, bool) function riscv_f32Eq (v1, v2) = { riscv_float_eq (v1, v2); @@ -557,7 +546,6 @@ function riscv_f64Le_quiet (v1, v2) = { (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } -val riscv_float_eq : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> unit val riscv_f64Eq : (bits_D, bits_D) -> (bits_fflags, bool) function riscv_f64Eq (v1, v2) = { riscv_float_eq (v1, v2); From 4c147153baa600340391eec3702ea6dfc41e80ef Mon Sep 17 00:00:00 2001 From: Pan Li Date: Mon, 12 Feb 2024 20:01:37 +0800 Subject: [PATCH 4/8] Remove the depends on softfloat_interface Signed-off-by: Pan Li --- model/float/riscv_float_common.sail | 38 ++-------------------------- model/float/riscv_float_eq.sail | 31 +++++++++++++---------- model/riscv_insts_dext.sail | 2 +- model/riscv_insts_fext.sail | 2 +- model/riscv_insts_vext_utils.sail | 11 -------- model/riscv_insts_vext_vm.sail | 8 +++--- model/riscv_insts_zfh.sail | 2 +- model/riscv_softfloat_interface.sail | 29 ++++++++------------- 8 files changed, 36 insertions(+), 87 deletions(-) diff --git a/model/float/riscv_float_common.sail b/model/float/riscv_float_common.sail index d55fd74a2..9b6575607 100644 --- a/model/float/riscv_float_common.sail +++ b/model/float/riscv_float_common.sail @@ -73,42 +73,8 @@ /* This file implements the floating-point for some common helper */ /* functions. They will be leveraged by other float sail implement */ /* */ -/* However, the implementation still need some global variables: */ -/* 1. float_result. */ -/* 2. float_fflags. */ -/* 3. float_roundingMode. */ /* **************************************************************** */ -type bits_rm = bits(3) /* Rounding mode */ +type bits_fflags = bits(5) /* Accrued exceptions: NV,DZ,OF,UF,NX */ -/* ***************************************************************** */ -/* Internal registers to pass results across the softfloat interface */ -/* to avoid return types involving structures. */ -/* */ -/* Todo: we will consider return the float_result directly in sail. */ -/* ***************************************************************** */ -register float_result : bits(64) -register float_fflags : bits(64) -register float_roundingMode : bits_rm - -let float_flag_invalid : bits(64) = zero_extend (64, 0x10) - -val riscv_float_enter : (bits_rm) -> unit -function riscv_float_enter (roundingMode) -> unit = { - float_fflags = zeros(64); - float_roundingMode = roundingMode; -} - -val riscv_float_leave : forall 'm, 'm in {16, 32, 64}. bits('m) -> unit -function riscv_float_leave (result) -> unit = { - match 'm { - 16 => float_result[15 .. 0] = result, - 32 => float_result[31 .. 0] = result, - 64 => float_result[63 .. 0] = result, - } -} - -val riscv_float_raise_flags : (bits(64)) -> unit -function riscv_float_raise_flags (flags) -> unit = { - float_fflags = float_fflags | flags -} +let float_flag_invalid : bits_fflags = 0b10000 diff --git a/model/float/riscv_float_eq.sail b/model/float/riscv_float_eq.sail index 03da4b0d3..7158ecf38 100644 --- a/model/float/riscv_float_eq.sail +++ b/model/float/riscv_float_eq.sail @@ -78,28 +78,31 @@ /* 2. Single-precision, aka 32 bits floating-point. */ /* 3. Half-precision, aka 16 bits floating-point. */ /* */ -/* However, the implementation still need some global variables in */ -/* file riscv_float_common.sail. It includes: */ -/* 1. float_result. */ -/* 2. float_fflags. */ -/* 3. float_roundingMode. */ /* **************************************************************** */ -val f_is_NaN : forall 'm, 'm in {16, 32, 64}. bits('m) -> bool -val f_is_SNaN : forall 'm, 'm in {16, 32, 64}. bits('m) -> bool - -val riscv_float_eq : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> unit -function riscv_float_eq (op1, op2) -> unit = { - riscv_float_enter (0b000); +val f_is_NaN : forall 'm, 'm in {16, 32, 64}. bits('m) -> bool +val f_is_SNaN : forall 'm, 'm in {16, 32, 64}. bits('m) -> bool +val accrue_fflags : (bits_fflags) -> unit +val riscv_float_eq : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> (bits_fflags, bool) +function riscv_float_eq (op1, op2) -> (bits_fflags, bool) = { let is_nan : bool = f_is_NaN (op1) | f_is_NaN (op2); let is_snan : bool = f_is_SNaN (op1) | f_is_SNaN (op2); - - if is_nan & is_snan then riscv_float_raise_flags (float_flag_invalid); + let fflags : bits_fflags = if is_nan & is_snan then float_flag_invalid else zeros (); let is_equal : bool = if not(is_nan) then op1 == op2 | ((op1 | op2) << 1) == zeros() else false; + let result : bits('m) = zero_extend('m, bool_bits(is_equal)); + + (fflags, is_equal) +} + +val riscv_float_raise_flags_eq : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool +function riscv_float_raise_flags_eq (op1, op2) -> bool = { + let (fflags, is_equal) = riscv_float_eq (op1, op2); + + accrue_fflags(fflags); - riscv_float_leave (zero_extend('m, bool_bits(is_equal))); + is_equal } diff --git a/model/riscv_insts_dext.sail b/model/riscv_insts_dext.sail index 58c5d5d96..998898c1f 100644 --- a/model/riscv_insts_dext.sail +++ b/model/riscv_insts_dext.sail @@ -798,7 +798,7 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FEQ_D)) = { let rs2_val_D = F_or_X_D(rs2); let (fflags, rd_val) : (bits_fflags, bool) = - riscv_f64Eq (rs1_val_D, rs2_val_D); + riscv_float_eq (rs1_val_D, rs2_val_D); accrue_fflags(fflags); X(rd) = zero_extend(bool_to_bits(rd_val)); diff --git a/model/riscv_insts_fext.sail b/model/riscv_insts_fext.sail index e4afb30d5..d3f3ea1b1 100644 --- a/model/riscv_insts_fext.sail +++ b/model/riscv_insts_fext.sail @@ -922,7 +922,7 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FEQ_S)) = { let rs2_val_S = F_or_X_S(rs2); let (fflags, rd_val) : (bits_fflags, bool) = - riscv_f32Eq (rs1_val_S, rs2_val_S); + riscv_float_eq(rs1_val_S, rs2_val_S); accrue_fflags(fflags); X(rd) = zero_extend(bool_to_bits(rd_val)); diff --git a/model/riscv_insts_vext_utils.sail b/model/riscv_insts_vext_utils.sail index 52b7c647e..cf28df71f 100755 --- a/model/riscv_insts_vext_utils.sail +++ b/model/riscv_insts_vext_utils.sail @@ -685,17 +685,6 @@ function fp_max(op1, op2) = { result_val } -val fp_eq : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool -function fp_eq(op1, op2) = { - let (fflags, result_val) : (bits_fflags, bool) = match 'm { - 16 => riscv_f16Eq(op1, op2), - 32 => riscv_f32Eq(op1, op2), - 64 => riscv_f64Eq(op1, op2) - }; - accrue_fflags(fflags); - result_val -} - val fp_gt : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool function fp_gt(op1, op2) = { let (fflags, temp_val) : (bits_fflags, bool) = match 'm { diff --git a/model/riscv_insts_vext_vm.sail b/model/riscv_insts_vext_vm.sail index 1f963e771..6eddf33eb 100755 --- a/model/riscv_insts_vext_vm.sail +++ b/model/riscv_insts_vext_vm.sail @@ -760,8 +760,8 @@ function clause execute(FVVMTYPE(funct6, vm, vs2, vs1, vd)) = { foreach (i from 0 to (num_elem - 1)) { if mask[i] then { let res : bool = match funct6 { - FVVM_VMFEQ => fp_eq(vs2_val[i], vs1_val[i]), - FVVM_VMFNE => ~(fp_eq(vs2_val[i], vs1_val[i])), + FVVM_VMFEQ => riscv_float_raise_flags_eq(vs2_val[i], vs1_val[i]), + FVVM_VMFNE => ~(riscv_float_raise_flags_eq(vs2_val[i], vs1_val[i])), FVVM_VMFLE => fp_le(vs2_val[i], vs1_val[i]), FVVM_VMFLT => fp_lt(vs2_val[i], vs1_val[i]) }; @@ -824,8 +824,8 @@ function clause execute(FVFMTYPE(funct6, vm, vs2, rs1, vd)) = { foreach (i from 0 to (num_elem - 1)) { if mask[i] then { let res : bool = match funct6 { - VFM_VMFEQ => fp_eq(vs2_val[i], rs1_val), - VFM_VMFNE => ~(fp_eq(vs2_val[i], rs1_val)), + VFM_VMFEQ => riscv_float_raise_flags_eq(vs2_val[i], rs1_val), + VFM_VMFNE => ~(riscv_float_raise_flags_eq(vs2_val[i], rs1_val)), VFM_VMFLE => fp_le(vs2_val[i], rs1_val), VFM_VMFLT => fp_lt(vs2_val[i], rs1_val), VFM_VMFGE => fp_ge(vs2_val[i], rs1_val), diff --git a/model/riscv_insts_zfh.sail b/model/riscv_insts_zfh.sail index 5522bad22..31485f72d 100644 --- a/model/riscv_insts_zfh.sail +++ b/model/riscv_insts_zfh.sail @@ -413,7 +413,7 @@ function clause execute (F_BIN_TYPE_H(rs2, rs1, rd, FEQ_H)) = { let rs2_val_H = F_or_X_H(rs2); let (fflags, rd_val) : (bits_fflags, bool) = - riscv_f16Eq (rs1_val_H, rs2_val_H); + riscv_float_eq (rs1_val_H, rs2_val_H); accrue_fflags(fflags); X(rd) = zero_extend(bool_to_bits(rd_val)); diff --git a/model/riscv_softfloat_interface.sail b/model/riscv_softfloat_interface.sail index 703243794..793d0cc6a 100644 --- a/model/riscv_softfloat_interface.sail +++ b/model/riscv_softfloat_interface.sail @@ -25,7 +25,7 @@ /* **************************************************************** */ /* All arguments and results have one of these types */ -type bits_fflags = bits(5) /* Accrued exceptions: NV,DZ,OF,UF,NX */ +type bits_rm = bits(3) /* Rounding mode */ type bits_H = bits(16) /* Half-precision float value */ type bits_S = bits(32) /* Single-precision float value */ type bits_D = bits(64) /* Double-precision float value */ @@ -36,6 +36,15 @@ 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. */ +/* */ +/* Todo: we will consider return the float_result directly in sail. */ +/* ***************************************************************** */ +register float_result : bits(64) +register float_fflags : bits(64) + /* **************************************************************** */ /* ADD/SUB/MUL/DIV */ @@ -416,12 +425,6 @@ function riscv_f16Le_quiet (v1, v2) = { (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } -val riscv_f16Eq : (bits_H, bits_H) -> (bits_fflags, bool) -function riscv_f16Eq (v1, v2) = { - riscv_float_eq (v1, v2); - (float_fflags[4 .. 0], bit_to_bool(float_result[0])) -} - val extern_f32Lt = {c: "softfloat_f32lt", ocaml: "Softfloat.f32_lt", lem: "softfloat_f32_lt"} : (bits_S, bits_S) -> unit val riscv_f32Lt : (bits_S, bits_S) -> (bits_fflags, bool) function riscv_f32Lt (v1, v2) = { @@ -450,12 +453,6 @@ function riscv_f32Le_quiet (v1, v2) = { (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } -val riscv_f32Eq : (bits_S, bits_S) -> (bits_fflags, bool) -function riscv_f32Eq (v1, v2) = { - riscv_float_eq (v1, v2); - (float_fflags[4 .. 0], bit_to_bool(float_result[0])) -} - val extern_f64Lt = {c: "softfloat_f64lt", ocaml: "Softfloat.f64_lt", lem: "softfloat_f64_lt"} : (bits_D, bits_D) -> unit val riscv_f64Lt : (bits_D, bits_D) -> (bits_fflags, bool) function riscv_f64Lt (v1, v2) = { @@ -484,12 +481,6 @@ function riscv_f64Le_quiet (v1, v2) = { (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } -val riscv_f64Eq : (bits_D, bits_D) -> (bits_fflags, bool) -function riscv_f64Eq (v1, v2) = { - riscv_float_eq (v1, v2); - (float_fflags[4 .. 0], bit_to_bool(float_result[0])) -} - val extern_f16roundToInt = {c: "softfloat_f16roundToInt", ocaml: "Softfloat.f16_round_to_int", lem: "softfloat_f16_round_to_int"} : (bits_rm, bits_H, bool) -> unit val riscv_f16roundToInt : (bits_rm, bits_H, bool) -> (bits_fflags, bits_H) function riscv_f16roundToInt (rm, v, exact) = { From d756053ca86784cfb69e88ae7008e0af3a3618ff Mon Sep 17 00:00:00 2001 From: Pan Li Date: Mon, 12 Feb 2024 20:20:05 +0800 Subject: [PATCH 5/8] Cleanup format. Signed-off-by: Pan Li --- model/float/riscv_float_eq.sail | 10 ++++------ model/riscv_insts_dext.sail | 2 +- model/riscv_insts_zfh.sail | 2 +- model/riscv_softfloat_interface.sail | 4 ++-- 4 files changed, 8 insertions(+), 10 deletions(-) diff --git a/model/float/riscv_float_eq.sail b/model/float/riscv_float_eq.sail index 7158ecf38..1f20f453b 100644 --- a/model/float/riscv_float_eq.sail +++ b/model/float/riscv_float_eq.sail @@ -86,21 +86,19 @@ val accrue_fflags : (bits_fflags) -> unit val riscv_float_eq : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> (bits_fflags, bool) function riscv_float_eq (op1, op2) -> (bits_fflags, bool) = { - let is_nan : bool = f_is_NaN (op1) | f_is_NaN (op2); - let is_snan : bool = f_is_SNaN (op1) | f_is_SNaN (op2); - let fflags : bits_fflags = if is_nan & is_snan then float_flag_invalid else zeros (); - + let is_nan : bool = f_is_NaN(op1) | f_is_NaN(op2); + let is_snan : bool = f_is_SNaN(op1) | f_is_SNaN(op2); + let fflags : bits_fflags = if is_nan & is_snan then float_flag_invalid else zeros(); let is_equal : bool = if not(is_nan) then op1 == op2 | ((op1 | op2) << 1) == zeros() else false; - let result : bits('m) = zero_extend('m, bool_bits(is_equal)); (fflags, is_equal) } val riscv_float_raise_flags_eq : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool function riscv_float_raise_flags_eq (op1, op2) -> bool = { - let (fflags, is_equal) = riscv_float_eq (op1, op2); + let (fflags, is_equal) = riscv_float_eq(op1, op2); accrue_fflags(fflags); diff --git a/model/riscv_insts_dext.sail b/model/riscv_insts_dext.sail index 998898c1f..bf2761004 100644 --- a/model/riscv_insts_dext.sail +++ b/model/riscv_insts_dext.sail @@ -798,7 +798,7 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FEQ_D)) = { let rs2_val_D = F_or_X_D(rs2); let (fflags, rd_val) : (bits_fflags, bool) = - riscv_float_eq (rs1_val_D, rs2_val_D); + riscv_float_eq(rs1_val_D, rs2_val_D); accrue_fflags(fflags); X(rd) = zero_extend(bool_to_bits(rd_val)); diff --git a/model/riscv_insts_zfh.sail b/model/riscv_insts_zfh.sail index 31485f72d..9479dd112 100644 --- a/model/riscv_insts_zfh.sail +++ b/model/riscv_insts_zfh.sail @@ -413,7 +413,7 @@ function clause execute (F_BIN_TYPE_H(rs2, rs1, rd, FEQ_H)) = { let rs2_val_H = F_or_X_H(rs2); let (fflags, rd_val) : (bits_fflags, bool) = - riscv_float_eq (rs1_val_H, rs2_val_H); + riscv_float_eq(rs1_val_H, rs2_val_H); accrue_fflags(fflags); X(rd) = zero_extend(bool_to_bits(rd_val)); diff --git a/model/riscv_softfloat_interface.sail b/model/riscv_softfloat_interface.sail index 793d0cc6a..245ddece2 100644 --- a/model/riscv_softfloat_interface.sail +++ b/model/riscv_softfloat_interface.sail @@ -42,8 +42,8 @@ type bits_LU = bits(64) /* Unsigned integer */ /* */ /* Todo: we will consider return the float_result directly in sail. */ /* ***************************************************************** */ -register float_result : bits(64) -register float_fflags : bits(64) +register float_result : bits(64) +register float_fflags : bits(64) /* **************************************************************** */ /* ADD/SUB/MUL/DIV */ From a05b202d97be401034b7e0c5852c89d62e3f6950 Mon Sep 17 00:00:00 2001 From: Pan Li Date: Tue, 13 Feb 2024 10:04:53 +0800 Subject: [PATCH 6/8] Address comments. Signed-off-by: Pan Li --- model/float/riscv_float_common.sail | 71 ++------------------- model/float/riscv_float_eq.sail | 95 +++++----------------------- model/riscv_insts_dext.sail | 3 +- model/riscv_insts_fext.sail | 3 +- model/riscv_insts_vext_vm.sail | 8 +-- model/riscv_insts_zfh.sail | 3 +- model/riscv_softfloat_interface.sail | 2 +- 7 files changed, 28 insertions(+), 157 deletions(-) diff --git a/model/float/riscv_float_common.sail b/model/float/riscv_float_common.sail index 9b6575607..62324a096 100644 --- a/model/float/riscv_float_common.sail +++ b/model/float/riscv_float_common.sail @@ -1,77 +1,14 @@ /*=======================================================================================*/ -/* RISCV Sail Model */ -/* */ /* This Sail RISC-V architecture model, comprising all files and */ -/* directories except for the snapshots of the Lem and Sail libraries */ -/* in the prover_snapshots directory (which include copies of their */ -/* licences), is subject to the BSD two-clause licence below. */ -/* */ -/* Copyright (c) 2017-2023 */ -/* Prashanth Mundkur */ -/* Rishiyur S. Nikhil and Bluespec, Inc. */ -/* Jon French */ -/* Brian Campbell */ -/* Robert Norton-Wright */ -/* Alasdair Armstrong */ -/* Thomas Bauereiss */ -/* Shaked Flur */ -/* Christopher Pulte */ -/* Peter Sewell */ -/* Alexander Richardson */ -/* Hesham Almatary */ -/* Jessica Clarke */ -/* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ -/* Intel, for contributions by Pan Li */ -/* Peter Rugg */ -/* Aril Computer Corp., for contributions by Scott Johnson */ -/* Philipp Tomsich */ -/* VRULL GmbH, for contributions by its employees */ -/* */ -/* All rights reserved. */ -/* */ -/* This software was developed by the above within the Rigorous */ -/* Engineering of Mainstream Systems (REMS) project, partly funded by */ -/* EPSRC grant EP/K008528/1, at the Universities of Cambridge and */ -/* Edinburgh. */ -/* */ -/* This software was developed by SRI International and the University of */ -/* Cambridge Computer Laboratory (Department of Computer Science and */ -/* Technology) under DARPA/AFRL contract FA8650-18-C-7809 ("CIFV"), and */ -/* under DARPA contract HR0011-18-C-0016 ("ECATS") as part of the DARPA */ -/* SSITH research programme. */ -/* */ -/* This project has received funding from the European Research Council */ -/* (ERC) under the European Union’s Horizon 2020 research and innovation */ -/* programme (grant agreement 789108, ELVER). */ -/* */ -/* */ -/* Redistribution and use in source and binary forms, with or without */ -/* modification, are permitted provided that the following conditions */ -/* are met: */ -/* 1. Redistributions of source code must retain the above copyright */ -/* notice, this list of conditions and the following disclaimer. */ -/* 2. Redistributions in binary form must reproduce the above copyright */ -/* notice, this list of conditions and the following disclaimer in */ -/* the documentation and/or other materials provided with the */ -/* distribution. */ +/* directories except where otherwise noted is subject the BSD */ +/* two-clause license in the LICENSE file. */ /* */ -/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ -/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ -/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ -/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ -/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ -/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ -/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ -/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ -/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ -/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ -/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ -/* SUCH DAMAGE. */ +/* SPDX-License-Identifier: BSD-2-Clause */ /*=======================================================================================*/ /* **************************************************************** */ /* This file implements the floating-point for some common helper */ -/* functions. They will be leveraged by other float sail implement */ +/* functions. They will be leveraged by other float sail implement. */ /* */ /* **************************************************************** */ diff --git a/model/float/riscv_float_eq.sail b/model/float/riscv_float_eq.sail index 1f20f453b..bbe51722c 100644 --- a/model/float/riscv_float_eq.sail +++ b/model/float/riscv_float_eq.sail @@ -1,104 +1,41 @@ /*=======================================================================================*/ -/* RISCV Sail Model */ -/* */ /* This Sail RISC-V architecture model, comprising all files and */ -/* directories except for the snapshots of the Lem and Sail libraries */ -/* in the prover_snapshots directory (which include copies of their */ -/* licences), is subject to the BSD two-clause licence below. */ -/* */ -/* Copyright (c) 2017-2023 */ -/* Prashanth Mundkur */ -/* Rishiyur S. Nikhil and Bluespec, Inc. */ -/* Jon French */ -/* Brian Campbell */ -/* Robert Norton-Wright */ -/* Alasdair Armstrong */ -/* Thomas Bauereiss */ -/* Shaked Flur */ -/* Christopher Pulte */ -/* Peter Sewell */ -/* Alexander Richardson */ -/* Hesham Almatary */ -/* Jessica Clarke */ -/* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ -/* Intel, for contributions by Pan Li */ -/* Peter Rugg */ -/* Aril Computer Corp., for contributions by Scott Johnson */ -/* Philipp Tomsich */ -/* VRULL GmbH, for contributions by its employees */ -/* */ -/* All rights reserved. */ -/* */ -/* This software was developed by the above within the Rigorous */ -/* Engineering of Mainstream Systems (REMS) project, partly funded by */ -/* EPSRC grant EP/K008528/1, at the Universities of Cambridge and */ -/* Edinburgh. */ -/* */ -/* This software was developed by SRI International and the University of */ -/* Cambridge Computer Laboratory (Department of Computer Science and */ -/* Technology) under DARPA/AFRL contract FA8650-18-C-7809 ("CIFV"), and */ -/* under DARPA contract HR0011-18-C-0016 ("ECATS") as part of the DARPA */ -/* SSITH research programme. */ +/* directories except where otherwise noted is subject the BSD */ +/* two-clause license in the LICENSE file. */ /* */ -/* This project has received funding from the European Research Council */ -/* (ERC) under the European Union’s Horizon 2020 research and innovation */ -/* programme (grant agreement 789108, ELVER). */ -/* */ -/* */ -/* Redistribution and use in source and binary forms, with or without */ -/* modification, are permitted provided that the following conditions */ -/* are met: */ -/* 1. Redistributions of source code must retain the above copyright */ -/* notice, this list of conditions and the following disclaimer. */ -/* 2. Redistributions in binary form must reproduce the above copyright */ -/* notice, this list of conditions and the following disclaimer in */ -/* the documentation and/or other materials provided with the */ -/* distribution. */ -/* */ -/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ -/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ -/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ -/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ -/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ -/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ -/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ -/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ -/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ -/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ -/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ -/* SUCH DAMAGE. */ +/* SPDX-License-Identifier: BSD-2-Clause */ /*=======================================================================================*/ /* **************************************************************** */ -/* This file implements the floating-point for equal and consumes */ -/* by the softfloat API contract, riscv_softfloat_interface.sail. */ +/* This file implements the floating-point for equal. The below */ +/* floating-point types are supported. */ /* */ -/* The below floating-point types are supported. */ /* 1. Double-precision, aka 64 bits floating-point. */ /* 2. Single-precision, aka 32 bits floating-point. */ /* 3. Half-precision, aka 16 bits floating-point. */ -/* */ /* **************************************************************** */ val f_is_NaN : forall 'm, 'm in {16, 32, 64}. bits('m) -> bool val f_is_SNaN : forall 'm, 'm in {16, 32, 64}. bits('m) -> bool val accrue_fflags : (bits_fflags) -> unit -val riscv_float_eq : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> (bits_fflags, bool) -function riscv_float_eq (op1, op2) -> (bits_fflags, bool) = { - let is_nan : bool = f_is_NaN(op1) | f_is_NaN(op2); - let is_snan : bool = f_is_SNaN(op1) | f_is_SNaN(op2); - let fflags : bits_fflags = if is_nan & is_snan then float_flag_invalid else zeros(); - let is_equal : bool = if not(is_nan) +val float_eq : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> (bits_fflags, bool) +function float_eq (op1, op2) = { + let is_nan = f_is_NaN(op1) | f_is_NaN(op2); + let is_snan = f_is_SNaN(op1) | f_is_SNaN(op2); + let fflags = if is_nan & is_snan + then float_flag_invalid + else zeros(); + let is_equal : bool = if not(is_nan) then op1 == op2 | ((op1 | op2) << 1) == zeros() else false; (fflags, is_equal) } -val riscv_float_raise_flags_eq : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool -function riscv_float_raise_flags_eq (op1, op2) -> bool = { - let (fflags, is_equal) = riscv_float_eq(op1, op2); +val float_raise_flags_eq : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool +function float_raise_flags_eq (op1, op2) = { + let (fflags, is_equal) = float_eq(op1, op2); accrue_fflags(fflags); diff --git a/model/riscv_insts_dext.sail b/model/riscv_insts_dext.sail index bf2761004..77569ae9d 100644 --- a/model/riscv_insts_dext.sail +++ b/model/riscv_insts_dext.sail @@ -797,8 +797,7 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FEQ_D)) = { let rs1_val_D = F_or_X_D(rs1); let rs2_val_D = F_or_X_D(rs2); - let (fflags, rd_val) : (bits_fflags, bool) = - riscv_float_eq(rs1_val_D, rs2_val_D); + let (fflags, rd_val) = float_eq(rs1_val_D, rs2_val_D); accrue_fflags(fflags); X(rd) = zero_extend(bool_to_bits(rd_val)); diff --git a/model/riscv_insts_fext.sail b/model/riscv_insts_fext.sail index d3f3ea1b1..af55c50c7 100644 --- a/model/riscv_insts_fext.sail +++ b/model/riscv_insts_fext.sail @@ -921,8 +921,7 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FEQ_S)) = { let rs1_val_S = F_or_X_S(rs1); let rs2_val_S = F_or_X_S(rs2); - let (fflags, rd_val) : (bits_fflags, bool) = - riscv_float_eq(rs1_val_S, rs2_val_S); + let (fflags, rd_val) = float_eq(rs1_val_S, rs2_val_S); accrue_fflags(fflags); X(rd) = zero_extend(bool_to_bits(rd_val)); diff --git a/model/riscv_insts_vext_vm.sail b/model/riscv_insts_vext_vm.sail index 6eddf33eb..99607441d 100755 --- a/model/riscv_insts_vext_vm.sail +++ b/model/riscv_insts_vext_vm.sail @@ -760,8 +760,8 @@ function clause execute(FVVMTYPE(funct6, vm, vs2, vs1, vd)) = { foreach (i from 0 to (num_elem - 1)) { if mask[i] then { let res : bool = match funct6 { - FVVM_VMFEQ => riscv_float_raise_flags_eq(vs2_val[i], vs1_val[i]), - FVVM_VMFNE => ~(riscv_float_raise_flags_eq(vs2_val[i], vs1_val[i])), + FVVM_VMFEQ => float_raise_flags_eq(vs2_val[i], vs1_val[i]), + FVVM_VMFNE => ~(float_raise_flags_eq(vs2_val[i], vs1_val[i])), FVVM_VMFLE => fp_le(vs2_val[i], vs1_val[i]), FVVM_VMFLT => fp_lt(vs2_val[i], vs1_val[i]) }; @@ -824,8 +824,8 @@ function clause execute(FVFMTYPE(funct6, vm, vs2, rs1, vd)) = { foreach (i from 0 to (num_elem - 1)) { if mask[i] then { let res : bool = match funct6 { - VFM_VMFEQ => riscv_float_raise_flags_eq(vs2_val[i], rs1_val), - VFM_VMFNE => ~(riscv_float_raise_flags_eq(vs2_val[i], rs1_val)), + VFM_VMFEQ => float_raise_flags_eq(vs2_val[i], rs1_val), + VFM_VMFNE => ~(float_raise_flags_eq(vs2_val[i], rs1_val)), VFM_VMFLE => fp_le(vs2_val[i], rs1_val), VFM_VMFLT => fp_lt(vs2_val[i], rs1_val), VFM_VMFGE => fp_ge(vs2_val[i], rs1_val), diff --git a/model/riscv_insts_zfh.sail b/model/riscv_insts_zfh.sail index 9479dd112..dbccdd27b 100644 --- a/model/riscv_insts_zfh.sail +++ b/model/riscv_insts_zfh.sail @@ -412,8 +412,7 @@ function clause execute (F_BIN_TYPE_H(rs2, rs1, rd, FEQ_H)) = { let rs1_val_H = F_or_X_H(rs1); let rs2_val_H = F_or_X_H(rs2); - let (fflags, rd_val) : (bits_fflags, bool) = - riscv_float_eq(rs1_val_H, rs2_val_H); + let (fflags, rd_val) = float_eq(rs1_val_H, rs2_val_H); accrue_fflags(fflags); X(rd) = zero_extend(bool_to_bits(rd_val)); diff --git a/model/riscv_softfloat_interface.sail b/model/riscv_softfloat_interface.sail index 245ddece2..b35e4e374 100644 --- a/model/riscv_softfloat_interface.sail +++ b/model/riscv_softfloat_interface.sail @@ -40,7 +40,7 @@ type bits_LU = bits(64) /* Unsigned integer */ /* Internal registers to pass results across the softfloat interface */ /* to avoid return types involving structures. */ /* */ -/* Todo: we will consider return the float_result directly in sail. */ +/* Todo: Return the float_result directly in Sail. */ /* ***************************************************************** */ register float_result : bits(64) register float_fflags : bits(64) From 320004964ac2dfd589d1d2e76c1cb228d6a2a364 Mon Sep 17 00:00:00 2001 From: Pan Li Date: Fri, 16 Feb 2024 13:09:24 +0800 Subject: [PATCH 7/8] Address comments. Signed-off-by: Pan Li --- model/float/riscv_float_common.sail | 1 + model/riscv_softfloat_interface.sail | 9 +++------ 2 files changed, 4 insertions(+), 6 deletions(-) diff --git a/model/float/riscv_float_common.sail b/model/float/riscv_float_common.sail index 62324a096..f3e991d18 100644 --- a/model/float/riscv_float_common.sail +++ b/model/float/riscv_float_common.sail @@ -12,6 +12,7 @@ /* */ /* **************************************************************** */ +type bits_rm = bits(3) /* Rounding mode */ type bits_fflags = bits(5) /* Accrued exceptions: NV,DZ,OF,UF,NX */ let float_flag_invalid : bits_fflags = 0b10000 diff --git a/model/riscv_softfloat_interface.sail b/model/riscv_softfloat_interface.sail index b35e4e374..68d41a212 100644 --- a/model/riscv_softfloat_interface.sail +++ b/model/riscv_softfloat_interface.sail @@ -25,7 +25,6 @@ /* **************************************************************** */ /* All arguments and results have one of these types */ -type bits_rm = bits(3) /* Rounding mode */ type bits_H = bits(16) /* Half-precision float value */ type bits_S = bits(32) /* Single-precision float value */ type bits_D = bits(64) /* Double-precision float value */ @@ -37,11 +36,9 @@ 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. */ -/* */ -/* Todo: Return the float_result directly in Sail. */ -/* ***************************************************************** */ +/* 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) From 88568f817916f96699929675430b0c858e28bb7e Mon Sep 17 00:00:00 2001 From: Pan Li Date: Thu, 4 Apr 2024 08:36:54 +0800 Subject: [PATCH 8/8] Address comments for code simplify. Signed-off-by: Pan Li --- model/float/riscv_float_eq.sail | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) diff --git a/model/float/riscv_float_eq.sail b/model/float/riscv_float_eq.sail index bbe51722c..54128ce8b 100644 --- a/model/float/riscv_float_eq.sail +++ b/model/float/riscv_float_eq.sail @@ -21,14 +21,12 @@ val accrue_fflags : (bits_fflags) -> unit val float_eq : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> (bits_fflags, bool) function float_eq (op1, op2) = { - let is_nan = f_is_NaN(op1) | f_is_NaN(op2); - let is_snan = f_is_SNaN(op1) | f_is_SNaN(op2); - let fflags = if is_nan & is_snan - then float_flag_invalid - else zeros(); - let is_equal : bool = if not(is_nan) - then op1 == op2 | ((op1 | op2) << 1) == zeros() - else false; + let is_nan = f_is_NaN(op1) | f_is_NaN(op2); + let is_snan = f_is_SNaN(op1) | f_is_SNaN(op2); + let fflags = if is_snan + then float_flag_invalid + else zeros(); + let is_equal = not(is_nan) & (op1 == op2) | ((op1 | op2) << 1) == zeros(); (fflags, is_equal) }