diff options
| -rw-r--r-- | Makefile | 20 | ||||
| -rw-r--r-- | c_emulator/riscv_prelude.h | 1 | ||||
| -rw-r--r-- | c_emulator/riscv_sail.h | 2 | ||||
| -rw-r--r-- | c_emulator/riscv_softfloat.c | 169 | ||||
| -rw-r--r-- | c_emulator/riscv_softfloat.h | 17 | ||||
| -rw-r--r-- | model/riscv_softfloat_interface.sail | 119 |
6 files changed, 291 insertions, 37 deletions
@@ -106,15 +106,21 @@ BBV_DIR?=../bbv C_WARNINGS ?= #-Wall -Wextra -Wno-unused-label -Wno-unused-parameter -Wno-unused-but-set-variable -Wno-unused-function -C_INCS = $(addprefix c_emulator/,riscv_prelude.h riscv_platform_impl.h riscv_platform.h) -C_SRCS = $(addprefix c_emulator/,riscv_prelude.c riscv_platform_impl.c riscv_platform.c riscv_sim.c) +C_INCS = $(addprefix c_emulator/,riscv_prelude.h riscv_platform_impl.h riscv_platform.h riscv_softfloat.h) +C_SRCS = $(addprefix c_emulator/,riscv_prelude.c riscv_platform_impl.c riscv_platform.c riscv_softfloat.c riscv_sim.c) # portability for MacPorts/MacOS C_SYS_INCLUDES = -I /opt/local/include C_SYS_LIBDIRS = -L /opt/local/lib -C_FLAGS = $(C_SYS_INCLUDES) -I $(SAIL_LIB_DIR) -I c_emulator -C_LIBS = $(C_SYS_LIBDIRS) -lgmp -lz +SOFTFLOAT_DIR = c_emulator/SoftFloat-3e +SOFTFLOAT_INCDIR = $(SOFTFLOAT_DIR)/source/include +SOFTFLOAT_LIBDIR = $(SOFTFLOAT_DIR)/build/Linux-x86_64-GCC +SOFTFLOAT_FLAGS = -I $(SOFTFLOAT_INCDIR) +SOFTFLOAT_LIBS = $(SOFTFLOAT_LIBDIR)/softfloat.a + +C_FLAGS = $(C_SYS_INCLUDES) -I $(SAIL_LIB_DIR) -I c_emulator $(SOFTFLOAT_FLAGS) +C_LIBS = $(C_SYS_LIBDIRS) -lgmp -lz $(SOFTFLOAT_LIBS) # The C simulator can be built to be linked against Spike for tandem-verification. # This needs the C bindings to Spike from https://github.com/SRI-CSL/l3riscv @@ -213,7 +219,10 @@ generated_definitions/c/riscv_model_$(ARCH).c: $(SAIL_SRCS) model/main.sail Make mkdir -p generated_definitions/c $(SAIL) $(SAIL_FLAGS) -O -Oconstant_fold -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_SRCS) model/main.sail -o $(basename $@) -c_emulator/riscv_sim_$(ARCH): generated_definitions/c/riscv_model_$(ARCH).c $(C_INCS) $(C_SRCS) Makefile +$(SOFTFLOAT_LIBS): + make -C $(SOFTFLOAT_LIBDIR) + +c_emulator/riscv_sim_$(ARCH): generated_definitions/c/riscv_model_$(ARCH).c $(C_INCS) $(C_SRCS) $(SOFTFLOAT_LIBS) Makefile gcc -g $(C_WARNINGS) $(C_FLAGS) $< $(C_SRCS) $(SAIL_LIB_DIR)/*.c $(C_LIBS) -o $@ generated_definitions/c/riscv_rvfi_model.c: $(SAIL_RVFI_SRCS) model/main.sail Makefile @@ -374,6 +383,7 @@ clean: -rm -rf generated_definitions/ocaml/* generated_definitions/c/* generated_definitions/latex/* -rm -rf generated_definitions/lem/* generated_definitions/isabelle/* generated_definitions/hol4/* generated_definitions/coq/* -rm -rf generated_definitions/for-rmem/* + -make -C $(SOFTFLOAT_LIBDIR) clean -rm -f c_emulator/riscv_sim_RV32 c_emulator/riscv_sim_RV64 c_emulator/riscv_rvfi -rm -rf ocaml_emulator/_sbuild ocaml_emulator/_build ocaml_emulator/riscv_ocaml_sim_RV32 ocaml_emulator/riscv_ocaml_sim_RV64 ocaml_emulator/tracecmp -rm -f *.gcno *.gcda diff --git a/c_emulator/riscv_prelude.h b/c_emulator/riscv_prelude.h index da292fe..9ac33aa 100644 --- a/c_emulator/riscv_prelude.h +++ b/c_emulator/riscv_prelude.h @@ -1,6 +1,7 @@ #pragma once #include "sail.h" #include "rts.h" +#include "riscv_softfloat.h" unit print_string(sail_string prefix, sail_string msg); diff --git a/c_emulator/riscv_sail.h b/c_emulator/riscv_sail.h index f177c57..67555c0 100644 --- a/c_emulator/riscv_sail.h +++ b/c_emulator/riscv_sail.h @@ -49,6 +49,8 @@ extern mach_bits zmstatus; extern mach_bits zmepc, zmtval; extern mach_bits zsepc, zstval; +extern mach_bits zfloat_result, zfloat_fflags; + struct zMcause {mach_bits zMcause_chunk_0;}; struct zMcause zmcause, zscause; diff --git a/c_emulator/riscv_softfloat.c b/c_emulator/riscv_softfloat.c new file mode 100644 index 0000000..a926d42 --- /dev/null +++ b/c_emulator/riscv_softfloat.c @@ -0,0 +1,169 @@ +#include "sail.h" +#include "rts.h" +#include "riscv_sail.h" +#include "riscv_softfloat.h" +#include "softfloat.h" + +#define SOFTFLOAT_PRELUDE(rm) \ + softfloat_exceptionFlags = 0; \ + softfloat_roundingMode = (uint_fast8_t) rm + +#define SOFTFLOAT_POSTLUDE(res) \ + zfloat_result = res.v; \ + zfloat_fflags = (mach_bits) softfloat_exceptionFlags + +unit softfloat_f32add(mach_bits rm, mach_bits v1, mach_bits v2) { + SOFTFLOAT_PRELUDE(rm); + + float32_t a, b, res; + a.v = v1; + b.v = v2; + res = f32_add(a, b); + + SOFTFLOAT_POSTLUDE(res); + + return UNIT; +} + +unit softfloat_f32sub(mach_bits rm, mach_bits v1, mach_bits v2) { + SOFTFLOAT_PRELUDE(rm); + + float32_t a, b, res; + a.v = v1; + b.v = v2; + res = f32_sub(a, b); + + SOFTFLOAT_POSTLUDE(res); + + return UNIT; +} + +unit softfloat_f32mul(mach_bits rm, mach_bits v1, mach_bits v2) { + SOFTFLOAT_PRELUDE(rm); + + float32_t a, b, res; + a.v = v1; + b.v = v2; + res = f32_mul(a, b); + + SOFTFLOAT_POSTLUDE(res); + + return UNIT; +} + +unit softfloat_f32div(mach_bits rm, mach_bits v1, mach_bits v2) { + SOFTFLOAT_PRELUDE(rm); + + float32_t a, b, res; + a.v = v1; + b.v = v2; + res = f32_div(a, b); + + SOFTFLOAT_POSTLUDE(res); + + return UNIT; +} + +unit softfloat_f64add(mach_bits rm, mach_bits v1, mach_bits v2) { + SOFTFLOAT_PRELUDE(rm); + + float64_t a, b, res; + a.v = v1; + b.v = v2; + res = f64_add(a, b); + + SOFTFLOAT_POSTLUDE(res); + + return UNIT; +} + +unit softfloat_f64sub(mach_bits rm, mach_bits v1, mach_bits v2) { + SOFTFLOAT_PRELUDE(rm); + + float64_t a, b, res; + a.v = v1; + b.v = v2; + res = f64_sub(a, b); + + SOFTFLOAT_POSTLUDE(res); + + return UNIT; +} + +unit softfloat_f64mul(mach_bits rm, mach_bits v1, mach_bits v2) { + SOFTFLOAT_PRELUDE(rm); + + float64_t a, b, res; + a.v = v1; + b.v = v2; + res = f64_mul(a, b); + + SOFTFLOAT_POSTLUDE(res); + + return UNIT; +} + +unit softfloat_f64div(mach_bits rm, mach_bits v1, mach_bits v2) { + SOFTFLOAT_PRELUDE(rm); + + float64_t a, b, res; + a.v = v1; + b.v = v2; + res = f64_div(a, b); + + SOFTFLOAT_POSTLUDE(res); + + return UNIT; +} + +unit softfloat_f32muladd(mach_bits rm, mach_bits v1, mach_bits v2, mach_bits v3) { + SOFTFLOAT_PRELUDE(rm); + + float32_t a, b, c, res; + a.v = v1; + b.v = v2; + c.v = v3; + res = f32_mulAdd(a, b, c); + + SOFTFLOAT_POSTLUDE(res); + + return UNIT; +} + +unit softfloat_f64muladd(mach_bits rm, mach_bits v1, mach_bits v2, mach_bits v3) { + SOFTFLOAT_PRELUDE(rm); + + float64_t a, b, c, res; + a.v = v1; + b.v = v2; + c.v = v3; + res = f64_mulAdd(a, b, c); + + SOFTFLOAT_POSTLUDE(res); + + return UNIT; +} + +unit softfloat_f32sqrt(mach_bits rm, mach_bits v) { + SOFTFLOAT_PRELUDE(rm); + + float32_t a, res; + a.v = v; + res = f32_sqrt(a); + + SOFTFLOAT_POSTLUDE(res); + + return UNIT; +} + +unit softfloat_f64sqrt(mach_bits rm, mach_bits v) { + SOFTFLOAT_PRELUDE(rm); + + float64_t a, res; + a.v = v; + res = f64_sqrt(a); + + SOFTFLOAT_POSTLUDE(res); + + return UNIT; +} diff --git a/c_emulator/riscv_softfloat.h b/c_emulator/riscv_softfloat.h new file mode 100644 index 0000000..eb68ce6 --- /dev/null +++ b/c_emulator/riscv_softfloat.h @@ -0,0 +1,17 @@ +#pragma once + +unit softfloat_f32add(mach_bits rm, mach_bits v1, mach_bits v2); +unit softfloat_f32sub(mach_bits rm, mach_bits v1, mach_bits v2); +unit softfloat_f32mul(mach_bits rm, mach_bits v1, mach_bits v2); +unit softfloat_f32div(mach_bits rm, mach_bits v1, mach_bits v2); + +unit softfloat_f64add(mach_bits rm, mach_bits v1, mach_bits v2); +unit softfloat_f64sub(mach_bits rm, mach_bits v1, mach_bits v2); +unit softfloat_f64mul(mach_bits rm, mach_bits v1, mach_bits v2); +unit softfloat_f64div(mach_bits rm, mach_bits v1, mach_bits v2); + +unit softfloat_f32muladd(mach_bits rm, mach_bits v1, mach_bits v2, mach_bits v3); +unit softfloat_f64muladd(mach_bits rm, mach_bits v1, mach_bits v2, mach_bits v3); + +unit softfloat_f32sqrt(mach_bits rm, mach_bits v); +unit softfloat_f64sqrt(mach_bits rm, mach_bits v); diff --git a/model/riscv_softfloat_interface.sail b/model/riscv_softfloat_interface.sail index 8c017dd..0a055cb 100644 --- a/model/riscv_softfloat_interface.sail +++ b/model/riscv_softfloat_interface.sail @@ -28,50 +28,105 @@ 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) + /* **************************************************************** */ /* ADD/SUB/MUL/DIV */ -val riscv_f32Add : (bits_rm, bits_S, bits_S) -> (bits_fflags, bits_S) -function riscv_f32Add (rm, v1, v2) = (0b_00000, 0x_0000_0000) - -val riscv_f32Sub : (bits_rm, bits_S, bits_S) -> (bits_fflags, bits_S) -function riscv_f32Sub (rm, v1, v2) = (0b_00000, 0x_0000_0000) - -val riscv_f32Mul : (bits_rm, bits_S, bits_S) -> (bits_fflags, bits_S) -function riscv_f32Mul (rm, v1, v2) = (0b_00000, 0x_0000_0000) - -val riscv_f32Div : (bits_rm, bits_S, bits_S) -> (bits_fflags, bits_S) -function riscv_f32Div (rm, v1, v2) = (0b_00000, 0x_0000_0000) - -val riscv_f64Add : (bits_rm, bits_D, bits_D) -> (bits_fflags, bits_D) -function riscv_f64Add (rm, v1, v2) = (0b_00000, 0x_0000_0000_0000_0000) - -val riscv_f64Sub : (bits_rm, bits_D, bits_D) -> (bits_fflags, bits_D) -function riscv_f64Sub (rm, v1, v2) = (0b_00000, 0x_0000_0000_0000_0000) - -val riscv_f64Mul : (bits_rm, bits_D, bits_D) -> (bits_fflags, bits_D) -function riscv_f64Mul (rm, v1, v2) = (0b_00000, 0x_0000_0000_0000_0000) - -val riscv_f64Div : (bits_rm, bits_D, bits_D) -> (bits_fflags, bits_D) -function riscv_f64Div (rm, v1, v2) = (0b_00000, 0x_0000_0000_0000_0000) +val extern_f32Add = {c: "softfloat_f32add"} : (bits_rm, bits_S, bits_S) -> unit +val riscv_f32Add : (bits_rm, bits_S, bits_S) -> (bits_fflags, bits_S) effect {rreg} +function riscv_f32Add (rm, v1, v2) = { + extern_f32Add(rm, v1, v2); + (float_fflags[4 .. 0], float_result[31 .. 0]) +} + +val extern_f32Sub = {c: "softfloat_f32sub"} : (bits_rm, bits_S, bits_S) -> unit +val riscv_f32Sub : (bits_rm, bits_S, bits_S) -> (bits_fflags, bits_S) effect {rreg} +function riscv_f32Sub (rm, v1, v2) = { + extern_f32Sub(rm, v1, v2); + (float_fflags[4 .. 0], float_result[31 .. 0]) +} + +val extern_f32Mul = {c: "softfloat_f32mul"} : (bits_rm, bits_S, bits_S) -> unit +val riscv_f32Mul : (bits_rm, bits_S, bits_S) -> (bits_fflags, bits_S) effect {rreg} +function riscv_f32Mul (rm, v1, v2) = { + extern_f32Mul(rm, v1, v2); + (float_fflags[4 .. 0], float_result[31 .. 0]) +} + +val extern_f32Div = {c: "softfloat_f32div"} : (bits_rm, bits_S, bits_S) -> unit +val riscv_f32Div : (bits_rm, bits_S, bits_S) -> (bits_fflags, bits_S) effect {rreg} +function riscv_f32Div (rm, v1, v2) = { + extern_f32Div(rm, v1, v2); + (float_fflags[4 .. 0], float_result[31 .. 0]) +} + +val extern_f64Add = {c: "softfloat_f64add"} : (bits_rm, bits_D, bits_D) -> unit +val riscv_f64Add : (bits_rm, bits_D, bits_D) -> (bits_fflags, bits_D) effect {rreg} +function riscv_f64Add (rm, v1, v2) = { + extern_f64Add(rm, v1, v2); + (float_fflags[4 .. 0], float_result) +} + +val extern_f64Sub = {c: "softfloat_f64sub"} : (bits_rm, bits_D, bits_D) -> unit +val riscv_f64Sub : (bits_rm, bits_D, bits_D) -> (bits_fflags, bits_D) effect {rreg} +function riscv_f64Sub (rm, v1, v2) = { + extern_f64Sub(rm, v1, v2); + (float_fflags[4 .. 0], float_result) +} + +val extern_f64Mul = {c: "softfloat_f64mul"} : (bits_rm, bits_D, bits_D) -> unit +val riscv_f64Mul : (bits_rm, bits_D, bits_D) -> (bits_fflags, bits_D) effect {rreg} +function riscv_f64Mul (rm, v1, v2) = { + extern_f64Mul(rm, v1, v2); + (float_fflags[4 .. 0], float_result) +} + +val extern_f64Div = {c: "softfloat_f64div"} : (bits_rm, bits_D, bits_D) -> unit +val riscv_f64Div : (bits_rm, bits_D, bits_D) -> (bits_fflags, bits_D) effect {rreg} +function riscv_f64Div (rm, v1, v2) = { + extern_f64Div(rm, v1, v2); + (float_fflags[4 .. 0], float_result) +} /* **************************************************************** */ /* MULTIPLY-ADD */ -val riscv_f32MulAdd : (bits_rm, bits_S, bits_S, bits_S) -> (bits_fflags, bits_S) -function riscv_f32MulAdd (rm, v1, v2, v3) = (0b_00000, 0x_0000_0000) +val extern_f32MulAdd = {c: "softfloat_f32muladd"} : (bits_rm, bits_S, bits_S, bits_S) -> unit +val riscv_f32MulAdd : (bits_rm, bits_S, bits_S, bits_S) -> (bits_fflags, bits_S) effect {rreg} +function riscv_f32MulAdd (rm, v1, v2, v3) = { + extern_f32MulAdd(rm, v1, v2, v3); + (float_fflags[4 .. 0], float_result[31 .. 0]) +} -val riscv_f64MulAdd : (bits_rm, bits_D, bits_D, bits_D) -> (bits_fflags, bits_D) -function riscv_f64MulAdd (rm, v1, v2, v3) = (0b_00000, 0x_0000_0000_0000_0000) +val extern_f64MulAdd = {c: "softfloat_f64muladd"} : (bits_rm, bits_D, bits_D, bits_D) -> unit +val riscv_f64MulAdd : (bits_rm, bits_D, bits_D, bits_D) -> (bits_fflags, bits_D) effect {rreg} +function riscv_f64MulAdd (rm, v1, v2, v3) = { + extern_f64MulAdd(rm, v1, v2, v3); + (float_fflags[4 .. 0], float_result) +} /* **************************************************************** */ /* SQUARE ROOT */ -val riscv_f32Sqrt : (bits_rm, bits_S) -> (bits_fflags, bits_S) -function riscv_f32Sqrt (rm, v) = (0b_00000, 0x_0000_0000) - -val riscv_f64Sqrt : (bits_rm, bits_D) -> (bits_fflags, bits_D) -function riscv_f64Sqrt (rm, v) = (0b_00000, 0x_0000_0000_0000_0000) +val extern_f32Sqrt = {c: "softfloat_f32sqrt"} : (bits_rm, bits_S) -> unit +val riscv_f32Sqrt : (bits_rm, bits_S) -> (bits_fflags, bits_S) effect {rreg} +function riscv_f32Sqrt (rm, v) = { + extern_f32Sqrt(rm, v); + (float_fflags[4 .. 0], float_result[31 .. 0]) +} + +val extern_f64Sqrt = {c: "softfloat_f64sqrt"} : (bits_rm, bits_D) -> unit +val riscv_f64Sqrt : (bits_rm, bits_D) -> (bits_fflags, bits_D) effect {rreg} +function riscv_f64Sqrt (rm, v) = { + extern_f64Sqrt(rm, v); + (float_fflags[4 .. 0], float_result) +} /* **************************************************************** */ /* CONVERSIONS */ |