Float: Add floating-point equals API in sail model

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
 

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) = {

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]))
 }
 

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
+}