Skip to content

Commit

Permalink
Address comments.
Browse files Browse the repository at this point in the history 
Signed-off-by: Pan Li <[email protected]>
  • Loading branch information
@Incarnation-p-lee
Incarnation-p-lee committed Feb 13, 2024
1 parent d756053 commit a05b202
Show file tree
Hide file tree
Showing 7 changed files with 28 additions and 157 deletions.
71 changes: 4 additions & 67 deletions model/float/riscv_float_common.sail
View file
Original file line number Diff line number Diff line change
@@ -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. */
/* */
/* **************************************************************** */

Expand Down
95 changes: 16 additions & 79 deletions model/float/riscv_float_eq.sail
View file
Original file line number Diff line number Diff line change
@@ -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);

Expand Down
3 changes: 1 addition & 2 deletions model/riscv_insts_dext.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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));
Expand Down
3 changes: 1 addition & 2 deletions model/riscv_insts_fext.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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));
Expand Down
8 changes: 4 additions & 4 deletions model/riscv_insts_vext_vm.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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])
};
Expand Down Expand Up @@ -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),
Expand Down
3 changes: 1 addition & 2 deletions model/riscv_insts_zfh.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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));
Expand Down
2 changes: 1 addition & 1 deletion model/riscv_softfloat_interface.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down

0 comments on commit a05b202

Please sign in to comment.