From ea09b9a1e8724b5c41138fe352ea84227aa892e2 Mon Sep 17 00:00:00 2001 From: Prashanth Mundkur Date: Tue, 7 Apr 2020 21:20:03 -0700 Subject: Switch floating-point comparisons to using softfloat to avoid missed corner-cases in hand-rolled helpers. --- c_emulator/riscv_softfloat.c | 78 +++++++++++++++++++++++++ c_emulator/riscv_softfloat.h | 7 +++ handwritten_support/0.11/riscv_extras_fdext.lem | 16 +++++ handwritten_support/riscv_extras_fdext.lem | 16 +++++ model/riscv_insts_dext.sail | 35 +++-------- model/riscv_insts_fext.sail | 41 ++++--------- model/riscv_softfloat_interface.sail | 44 ++++++++++++++ ocaml_emulator/softfloat.ml | 17 ++++++ 8 files changed, 199 insertions(+), 55 deletions(-) diff --git a/c_emulator/riscv_softfloat.c b/c_emulator/riscv_softfloat.c index d0f8069..3556616 100644 --- a/c_emulator/riscv_softfloat.c +++ b/c_emulator/riscv_softfloat.c @@ -397,3 +397,81 @@ unit softfloat_f64tof32(mach_bits rm, mach_bits v) { return UNIT; } + +unit softfloat_f32lt(mach_bits v1, mach_bits v2) { + SOFTFLOAT_PRELUDE(0); + + float32_t a, b, res; + a.v = v1; + b.v = v2; + res.v = f32_lt(a, b); + + SOFTFLOAT_POSTLUDE(res); + + return UNIT; +} + +unit softfloat_f32le(mach_bits v1, mach_bits v2) { + SOFTFLOAT_PRELUDE(0); + + float32_t a, b, res; + a.v = v1; + b.v = v2; + res.v = f32_le(a, b); + + SOFTFLOAT_POSTLUDE(res); + + return UNIT; +} + +unit softfloat_f32eq(mach_bits v1, mach_bits v2) { + SOFTFLOAT_PRELUDE(0); + + float32_t a, b, res; + a.v = v1; + b.v = v2; + res.v = f32_eq(a, b); + + SOFTFLOAT_POSTLUDE(res); + + return UNIT; +} + +unit softfloat_f64lt(mach_bits v1, mach_bits v2) { + SOFTFLOAT_PRELUDE(0); + + float64_t a, b, res; + a.v = v1; + b.v = v2; + res.v = f64_lt(a, b); + + SOFTFLOAT_POSTLUDE(res); + + return UNIT; +} + +unit softfloat_f64le(mach_bits v1, mach_bits v2) { + SOFTFLOAT_PRELUDE(0); + + float64_t a, b, res; + a.v = v1; + b.v = v2; + res.v = f64_le(a, b); + + SOFTFLOAT_POSTLUDE(res); + + return UNIT; +} + +unit softfloat_f64eq(mach_bits v1, mach_bits v2) { + SOFTFLOAT_PRELUDE(0); + + float64_t a, b, res; + a.v = v1; + b.v = v2; + res.v = f64_eq(a, b); + + SOFTFLOAT_POSTLUDE(res); + + return UNIT; +} diff --git a/c_emulator/riscv_softfloat.h b/c_emulator/riscv_softfloat.h index bd7edf0..57ae0f2 100644 --- a/c_emulator/riscv_softfloat.h +++ b/c_emulator/riscv_softfloat.h @@ -38,3 +38,10 @@ unit softfloat_ui64tof64(mach_bits rm, mach_bits v); unit softfloat_f32tof64(mach_bits rm, mach_bits v); unit softfloat_f64tof32(mach_bits rm, mach_bits v); + +unit softfloat_f32lt(mach_bits v1, mach_bits v2); +unit softfloat_f32le(mach_bits v1, mach_bits v2); +unit softfloat_f32eq(mach_bits v1, mach_bits v2); +unit softfloat_f64lt(mach_bits v1, mach_bits v2); +unit softfloat_f64le(mach_bits v1, mach_bits v2); +unit softfloat_f64eq(mach_bits v1, mach_bits v2); diff --git a/handwritten_support/0.11/riscv_extras_fdext.lem b/handwritten_support/0.11/riscv_extras_fdext.lem index 3c79089..12cfe00 100644 --- a/handwritten_support/0.11/riscv_extras_fdext.lem +++ b/handwritten_support/0.11/riscv_extras_fdext.lem @@ -106,4 +106,20 @@ val softfloat_f64_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> b let softfloat_f64_to_f32 _ _ = () +val softfloat_f32_lt : forall 's. Size 's => bitvector 's -> bitvector 's -> unit +let softfloat_f32_lt _ _ = () +val softfloat_f32_le : forall 's. Size 's => bitvector 's -> bitvector 's -> unit +let softfloat_f32_le _ _ = () + +val softfloat_f32_eq : forall 's. Size 's => bitvector 's -> bitvector 's -> unit +let softfloat_f32_eq _ _ = () + +val softfloat_f64_lt : forall 's. Size 's => bitvector 's -> bitvector 's -> unit +let softfloat_f64_lt _ _ = () + +val softfloat_f64_le : forall 's. Size 's => bitvector 's -> bitvector 's -> unit +let softfloat_f64_le _ _ = () + +val softfloat_f64_eq : forall 's. Size 's => bitvector 's -> bitvector 's -> unit +let softfloat_f64_eq _ _ = () diff --git a/handwritten_support/riscv_extras_fdext.lem b/handwritten_support/riscv_extras_fdext.lem index 3c79089..12cfe00 100644 --- a/handwritten_support/riscv_extras_fdext.lem +++ b/handwritten_support/riscv_extras_fdext.lem @@ -106,4 +106,20 @@ val softfloat_f64_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> b let softfloat_f64_to_f32 _ _ = () +val softfloat_f32_lt : forall 's. Size 's => bitvector 's -> bitvector 's -> unit +let softfloat_f32_lt _ _ = () +val softfloat_f32_le : forall 's. Size 's => bitvector 's -> bitvector 's -> unit +let softfloat_f32_le _ _ = () + +val softfloat_f32_eq : forall 's. Size 's => bitvector 's -> bitvector 's -> unit +let softfloat_f32_eq _ _ = () + +val softfloat_f64_lt : forall 's. Size 's => bitvector 's -> bitvector 's -> unit +let softfloat_f64_lt _ _ = () + +val softfloat_f64_le : forall 's. Size 's => bitvector 's -> bitvector 's -> unit +let softfloat_f64_le _ _ = () + +val softfloat_f64_eq : forall 's. Size 's => bitvector 's -> bitvector 's -> unit +let softfloat_f64_eq _ _ = () diff --git a/model/riscv_insts_dext.sail b/model/riscv_insts_dext.sail index 4fcf7b1..d1d1fca 100644 --- a/model/riscv_insts_dext.sail +++ b/model/riscv_insts_dext.sail @@ -720,15 +720,10 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FEQ_D)) = { let rs1_val_D = F(rs1); let rs2_val_D = F(rs2); - let (rs1_eq_rs2, fflags) = feq_quiet_D (rs1_val_D, rs2_val_D); + let (fflags, rd_val) : (bits_fflags, bits_LU) = + riscv_f64Eq (rs1_val_D, rs2_val_D); - let rd_val : xlenbits = - if (f_is_SNaN_D(rs1_val_D) | f_is_SNaN_D(rs2_val_D)) then zeros() - else if (f_is_QNaN_D(rs1_val_D) | f_is_QNaN_D(rs2_val_D)) then zeros() - else if rs1_eq_rs2 then EXTZ(0b1) - else zeros(); - - accrue_fflags(fflags); + write_fflags(fflags); X(rd) = rd_val; RETIRE_SUCCESS } @@ -737,16 +732,10 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FLT_D)) = { let rs1_val_D = F(rs1); let rs2_val_D = F(rs2); - let is_quiet = false; - let (rs1_lt_rs2, fflags) = flt_D (rs1_val_D, rs2_val_D, is_quiet); + let (fflags, rd_val) : (bits_fflags, bits_LU) = + riscv_f64Lt (rs1_val_D, rs2_val_D); - let rd_val : xlenbits = - if (f_is_SNaN_D(rs1_val_D) | f_is_SNaN_D(rs2_val_D)) then zeros() - else if (f_is_QNaN_D(rs1_val_D) | f_is_QNaN_D(rs2_val_D)) then zeros() - else if rs1_lt_rs2 then EXTZ(0b1) - else zeros(); - - accrue_fflags(fflags); + write_fflags(fflags); X(rd) = rd_val; RETIRE_SUCCESS } @@ -755,16 +744,10 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FLE_D)) = { let rs1_val_D = F(rs1); let rs2_val_D = F(rs2); - let is_quiet = false; - let (rs1_le_rs2, fflags) = fle_D (rs1_val_D, rs2_val_D, is_quiet); - - let rd_val : xlenbits = - if (f_is_SNaN_D(rs1_val_D) | f_is_SNaN_D(rs2_val_D)) then zeros() - else if (f_is_QNaN_D(rs1_val_D) | f_is_QNaN_D(rs2_val_D)) then zeros() - else if rs1_le_rs2 then EXTZ(0b1) - else zeros(); + let (fflags, rd_val) : (bits_fflags, bits_LU) = + riscv_f64Le (rs1_val_D, rs2_val_D); - accrue_fflags(fflags); + write_fflags(fflags); X(rd) = rd_val; RETIRE_SUCCESS } diff --git a/model/riscv_insts_fext.sail b/model/riscv_insts_fext.sail index 280389a..34b6c91 100644 --- a/model/riscv_insts_fext.sail +++ b/model/riscv_insts_fext.sail @@ -896,16 +896,11 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FEQ_S)) = { let rs1_val_S = nan_unbox (F(rs1)); let rs2_val_S = nan_unbox (F(rs2)); - let (rs1_eq_rs2, fflags) = feq_quiet_S (rs1_val_S, rs2_val_S); + let (fflags, rd_val) : (bits_fflags, bits_WU) = + riscv_f32Eq (rs1_val_S, rs2_val_S); - let rd_val : xlenbits = - if (f_is_SNaN_S(rs1_val_S) | f_is_SNaN_S(rs2_val_S)) then zeros() - else if (f_is_QNaN_S(rs1_val_S) | f_is_QNaN_S(rs2_val_S)) then zeros() - else if rs1_eq_rs2 then EXTZ(0b1) - else zeros(); - - accrue_fflags(fflags); - X(rd) = rd_val; + write_fflags(fflags); + X(rd) = EXTZ(rd_val); RETIRE_SUCCESS } @@ -913,17 +908,11 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FLT_S)) = { let rs1_val_S = nan_unbox (F(rs1)); let rs2_val_S = nan_unbox (F(rs2)); - let is_quiet = false; - let (rs1_lt_rs2, fflags) = flt_S (rs1_val_S, rs2_val_S, is_quiet); + let (fflags, rd_val) : (bits_fflags, bits_WU) = + riscv_f32Lt (rs1_val_S, rs2_val_S); - let rd_val : xlenbits = - if (f_is_SNaN_S(rs1_val_S) | f_is_SNaN_S(rs2_val_S)) then zeros() - else if (f_is_QNaN_S(rs1_val_S) | f_is_QNaN_S(rs2_val_S)) then zeros() - else if rs1_lt_rs2 then EXTZ(0b1) - else zeros(); - - accrue_fflags(fflags); - X(rd) = rd_val; + write_fflags(fflags); + X(rd) = EXTZ(rd_val); RETIRE_SUCCESS } @@ -931,17 +920,11 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FLE_S)) = { let rs1_val_S = nan_unbox (F(rs1)); let rs2_val_S = nan_unbox (F(rs2)); - let is_quiet = false; - let (rs1_le_rs2, fflags) = fle_S (rs1_val_S, rs2_val_S, is_quiet); - - let rd_val : xlenbits = - if (f_is_SNaN_S(rs1_val_S) | f_is_SNaN_S(rs2_val_S)) then zeros() - else if (f_is_QNaN_S(rs1_val_S) | f_is_QNaN_S(rs2_val_S)) then zeros() - else if rs1_le_rs2 then EXTZ(0b1) - else zeros(); + let (fflags, rd_val) : (bits_fflags, bits_WU) = + riscv_f32Le (rs1_val_S, rs2_val_S); - accrue_fflags(fflags); - X(rd) = rd_val; + write_fflags(fflags); + X(rd) = EXTZ(rd_val); RETIRE_SUCCESS } diff --git a/model/riscv_softfloat_interface.sail b/model/riscv_softfloat_interface.sail index 88bbdc6..8c3653b 100644 --- a/model/riscv_softfloat_interface.sail +++ b/model/riscv_softfloat_interface.sail @@ -264,3 +264,47 @@ function riscv_f64ToF32 (rm, v) = { } /* **************************************************************** */ +/* COMPARISONS */ + +val extern_f32Lt = {c: "softfloat_f32lt", ocaml: "Softfloat.f32_lt", lem: "softfloat_f32_lt"} : (bits_S, bits_S) -> unit +val riscv_f32Lt : (bits_S, bits_S) -> (bits_fflags, bits_WU) effect {rreg} +function riscv_f32Lt (v1, v2) = { + extern_f32Lt(v1, v2); + (float_fflags[4 .. 0], float_result[31 .. 0]) +} + +val extern_f32Le = {c: "softfloat_f32le", ocaml: "Softfloat.f32_le", lem: "softfloat_f32_le"} : (bits_S, bits_S) -> unit +val riscv_f32Le : (bits_S, bits_S) -> (bits_fflags, bits_WU) effect {rreg} +function riscv_f32Le (v1, v2) = { + extern_f32Le(v1, v2); + (float_fflags[4 .. 0], float_result[31 .. 0]) +} + +val extern_f32Eq = {c: "softfloat_f32eq", ocaml: "Softfloat.f32_eq", lem: "softfloat_f32_eq"} : (bits_S, bits_S) -> unit +val riscv_f32Eq : (bits_S, bits_S) -> (bits_fflags, bits_WU) effect {rreg} +function riscv_f32Eq (v1, v2) = { + extern_f32Eq(v1, v2); + (float_fflags[4 .. 0], float_result[31 .. 0]) +} + +val extern_f64Lt = {c: "softfloat_f64lt", ocaml: "Softfloat.f64_lt", lem: "softfloat_f64_lt"} : (bits_D, bits_D) -> unit +val riscv_f64Lt : (bits_D, bits_D) -> (bits_fflags, bits_LU) effect {rreg} +function riscv_f64Lt (v1, v2) = { + extern_f64Lt(v1, v2); + (float_fflags[4 .. 0], float_result) +} + +val extern_f64Le = {c: "softfloat_f64le", ocaml: "Softfloat.f64_le", lem: "softfloat_f64_le"} : (bits_D, bits_D) -> unit +val riscv_f64Le : (bits_D, bits_D) -> (bits_fflags, bits_LU) effect {rreg} +function riscv_f64Le (v1, v2) = { + extern_f64Le(v1, v2); + (float_fflags[4 .. 0], float_result) +} + +val extern_f64Eq = {c: "softfloat_f64eq", ocaml: "Softfloat.f64_eq", lem: "softfloat_f64_eq"} : (bits_D, bits_D) -> unit +val riscv_f64Eq : (bits_D, bits_D) -> (bits_fflags, bits_LU) effect {rreg} +function riscv_f64Eq (v1, v2) = { + extern_f64Eq(v1, v2); + (float_fflags[4 .. 0], float_result) +} +/* **************************************************************** */ diff --git a/ocaml_emulator/softfloat.ml b/ocaml_emulator/softfloat.ml index ef84185..0de5e09 100644 --- a/ocaml_emulator/softfloat.ml +++ b/ocaml_emulator/softfloat.ml @@ -89,3 +89,20 @@ let f32_to_f64 rm v = let f64_to_f32 rm v = () +let f32_lt v1 v2 = + () + +let f32_le v1 v2 = + () + +let f32_eq v1 v2 = + () + +let f64_lt v1 v2 = + () + +let f64_le v1 v2 = + () + +let f64_eq v1 v2 = + () -- cgit v1.1