Skip to content

Commit

Permalink
Softfloat: Add soft floating-point equals API in sail model
Browse files Browse the repository at this point in the history
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 <[email protected]>
  • Loading branch information
Incarnation-p-lee committed Feb 7, 2024
1 parent 4de2bff commit 2923e21
Show file tree
Hide file tree
Showing 6 changed files with 304 additions and 7 deletions.
2 changes: 2 additions & 0 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
18 changes: 18 additions & 0 deletions model/riscv_insts_vext_utils.sail
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand All @@ -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) = {
Expand Down
13 changes: 7 additions & 6 deletions model/riscv_softfloat_interface.sail
Original file line number Diff line number Diff line change
Expand Up @@ -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 */
Expand Down Expand Up @@ -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]))
}

Expand Down Expand Up @@ -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]))
}

Expand Down Expand Up @@ -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]))
}

Expand Down
123 changes: 123 additions & 0 deletions model/softfloat/riscv_softfloat_common.sail
Original file line number Diff line number Diff line change
@@ -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
}
Loading

0 comments on commit 2923e21

Please sign in to comment.