(*=======================================================================================*) (* 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 *) (* 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. *) (*=======================================================================================*) open import Pervasives open import Pervasives_extra open import Sail2_instr_kinds open import Sail2_values open import Sail2_operators_mwords open import Sail2_prompt_monad open import Sail2_prompt type bitvector = list Sail2_values.bitU (* stub functions emulating the C softfloat interface *) val softfloat_f16_round_to_int : bitvector -> bitvector -> bool -> unit let softfloat_f16_round_to_int _ _ _ = () val softfloat_f32_round_to_int : bitvector -> bitvector -> bool -> unit let softfloat_f32_round_to_int _ _ _ = () val softfloat_f64_round_to_int : bitvector -> bitvector -> bool -> unit let softfloat_f64_round_to_int _ _ _ = () val softfloat_f16_add : bitvector -> bitvector -> bitvector -> unit let softfloat_f16_add _ _ _ = () val softfloat_f16_sub : bitvector -> bitvector -> bitvector -> unit let softfloat_f16_sub _ _ _ = () val softfloat_f16_mul : bitvector -> bitvector -> bitvector -> unit let softfloat_f16_mul _ _ _ = () val softfloat_f16_div : bitvector -> bitvector -> bitvector -> unit let softfloat_f16_div _ _ _ = () val softfloat_f32_add : bitvector -> bitvector -> bitvector -> unit let softfloat_f32_add _ _ _ = () val softfloat_f32_sub : bitvector -> bitvector -> bitvector -> unit let softfloat_f32_sub _ _ _ = () val softfloat_f32_mul : bitvector -> bitvector -> bitvector -> unit let softfloat_f32_mul _ _ _ = () val softfloat_f32_div : bitvector -> bitvector -> bitvector -> unit let softfloat_f32_div _ _ _ = () val softfloat_f64_add : bitvector -> bitvector -> bitvector -> unit let softfloat_f64_add _ _ _ = () val softfloat_f64_sub : bitvector -> bitvector -> bitvector -> unit let softfloat_f64_sub _ _ _ = () val softfloat_f64_mul : bitvector -> bitvector -> bitvector -> unit let softfloat_f64_mul _ _ _ = () val softfloat_f64_div : bitvector -> bitvector -> bitvector -> unit let softfloat_f64_div _ _ _ = () val softfloat_f16_muladd : bitvector -> bitvector -> bitvector -> bitvector -> unit let softfloat_f16_muladd _ _ _ _ = () val softfloat_f32_muladd : bitvector -> bitvector -> bitvector -> bitvector -> unit let softfloat_f32_muladd _ _ _ _ = () val softfloat_f64_muladd : bitvector -> bitvector -> bitvector -> bitvector -> unit let softfloat_f64_muladd _ _ _ _ = () val softfloat_f16_sqrt : bitvector -> bitvector -> unit let softfloat_f16_sqrt _ _ = () val softfloat_f32_sqrt : bitvector -> bitvector -> unit let softfloat_f32_sqrt _ _ = () val softfloat_f64_sqrt : bitvector -> bitvector -> unit let softfloat_f64_sqrt _ _ = () val softfloat_f16_to_i32: bitvector -> bitvector -> unit let softfloat_f16_to_i32 _ _ = () val softfloat_f16_to_ui32: bitvector -> bitvector -> unit let softfloat_f16_to_ui32 _ _ = () val softfloat_i32_to_f16: bitvector -> bitvector -> unit let softfloat_i32_to_f16 _ _ = () val softfloat_ui32_to_f16: bitvector -> bitvector -> unit let softfloat_ui32_to_f16 _ _ = () val softfloat_f16_to_i64: bitvector -> bitvector -> unit let softfloat_f16_to_i64 _ _ = () val softfloat_f16_to_ui64: bitvector -> bitvector -> unit let softfloat_f16_to_ui64 _ _ = () val softfloat_i64_to_f16: bitvector -> bitvector -> unit let softfloat_i64_to_f16 _ _ = () val softfloat_ui64_to_f16: bitvector -> bitvector -> unit let softfloat_ui64_to_f16 _ _ = () val softfloat_f32_to_i32: bitvector -> bitvector -> unit let softfloat_f32_to_i32 _ _ = () val softfloat_f32_to_ui32: bitvector -> bitvector -> unit let softfloat_f32_to_ui32 _ _ = () val softfloat_i32_to_f32: bitvector -> bitvector -> unit let softfloat_i32_to_f32 _ _ = () val softfloat_ui32_to_f32: bitvector -> bitvector -> unit let softfloat_ui32_to_f32 _ _ = () val softfloat_f32_to_i64: bitvector -> bitvector -> unit let softfloat_f32_to_i64 _ _ = () val softfloat_f32_to_ui64: bitvector -> bitvector -> unit let softfloat_f32_to_ui64 _ _ = () val softfloat_i64_to_f32: bitvector -> bitvector -> unit let softfloat_i64_to_f32 _ _ = () val softfloat_ui64_to_f32: bitvector -> bitvector -> unit let softfloat_ui64_to_f32 _ _ = () val softfloat_f64_to_i32: bitvector -> bitvector -> unit let softfloat_f64_to_i32 _ _ = () val softfloat_f64_to_ui32: bitvector -> bitvector -> unit let softfloat_f64_to_ui32 _ _ = () val softfloat_i32_to_f64: bitvector -> bitvector -> unit let softfloat_i32_to_f64 _ _ = () val softfloat_ui32_to_f64: bitvector -> bitvector -> unit let softfloat_ui32_to_f64 _ _ = () val softfloat_f64_to_i64: bitvector -> bitvector -> unit let softfloat_f64_to_i64 _ _ = () val softfloat_f64_to_ui64: bitvector -> bitvector -> unit let softfloat_f64_to_ui64 _ _ = () val softfloat_i64_to_f64: bitvector -> bitvector -> unit let softfloat_i64_to_f64 _ _ = () val softfloat_ui64_to_f64: bitvector -> bitvector -> unit let softfloat_ui64_to_f64 _ _ = () val softfloat_f16_to_f32: bitvector -> bitvector -> unit let softfloat_f16_to_f32 _ _ = () val softfloat_f16_to_f64: bitvector -> bitvector -> unit let softfloat_f16_to_f64 _ _ = () val softfloat_f32_to_f64: bitvector -> bitvector -> unit let softfloat_f32_to_f64 _ _ = () val softfloat_f32_to_f16: bitvector -> bitvector -> unit let softfloat_f32_to_f16 _ _ = () val softfloat_f64_to_f16: bitvector -> bitvector -> unit let softfloat_f64_to_f16 _ _ = () val softfloat_f64_to_f32: bitvector -> bitvector -> unit let softfloat_f64_to_f32 _ _ = () val softfloat_f16_lt : bitvector -> bitvector -> unit let softfloat_f16_lt _ _ = () val softfloat_f16_lt_quiet : bitvector -> bitvector -> unit let softfloat_f16_lt_quiet _ _ = () val softfloat_f16_le : bitvector -> bitvector -> unit let softfloat_f16_le _ _ = () val softfloat_f16_le_quiet : bitvector -> bitvector -> unit let softfloat_f16_le_quiet _ _ = () val softfloat_f16_eq : bitvector -> bitvector -> unit let softfloat_f16_eq _ _ = () val softfloat_f32_lt : bitvector -> bitvector -> unit let softfloat_f32_lt _ _ = () val softfloat_f32_lt_quiet : bitvector -> bitvector -> unit let softfloat_f32_lt_quiet _ _ = () val softfloat_f32_le : bitvector -> bitvector -> unit let softfloat_f32_le _ _ = () val softfloat_f32_le_quiet : bitvector -> bitvector -> unit let softfloat_f32_le_quiet _ _ = () val softfloat_f32_eq : bitvector -> bitvector -> unit let softfloat_f32_eq _ _ = () val softfloat_f64_lt : bitvector -> bitvector -> unit let softfloat_f64_lt _ _ = () val softfloat_f64_lt_quiet : bitvector -> bitvector -> unit let softfloat_f64_lt_quiet _ _ = () val softfloat_f64_le : bitvector -> bitvector -> unit let softfloat_f64_le _ _ = () val softfloat_f64_le_quiet : bitvector -> bitvector -> unit let softfloat_f64_le_quiet _ _ = () val softfloat_f64_eq : bitvector -> bitvector -> unit let softfloat_f64_eq _ _ = ()