diff --git a/Makefile b/Makefile index c71278189..3184c54a0 100644 --- a/Makefile +++ b/Makefile @@ -67,7 +67,7 @@ SAIL_SYS_SRCS += riscv_next_regs.sail SAIL_SYS_SRCS += riscv_sys_exceptions.sail # default basic helpers for exception handling 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_float.sail riscv_softfloat_interface.sail riscv_fdext_regs.sail riscv_fdext_control.sail +SAIL_SYS_SRCS += riscv_softfloat_interface.sail riscv_float.sail riscv_fdext_regs.sail riscv_fdext_control.sail SAIL_SYS_SRCS += riscv_csr_ext.sail # access to CSR extensions SAIL_SYS_SRCS += riscv_sys_control.sail # general exception handling diff --git a/model/riscv_float.sail b/model/riscv_float.sail index 4f0468369..b52cf1248 100644 --- a/model/riscv_float.sail +++ b/model/riscv_float.sail @@ -109,3 +109,97 @@ function f_is_NaN(x : fbits) -> bool = { // Negation (invert the sign bit which is always the top bit). val f_negate : forall 'n, 'n in {16, 32, 64}. bits('n) -> bits('n) function f_negate(x) = ~(x['n - 1 .. 'n - 1]) @ x['n - 2 .. 0] + +// --------------------------------------------------------------------------- +// Help functions used in the semantic functions. + +// Exception flags. +let nxFlag = 0b00001 +let ufFlag = 0b00010 +let ofFlag = 0b00100 +let dzFlag = 0b01000 +let nvFlag = 0b10000 + +// Note: this is currently unused. +val feq_quiet : forall 'n, 'n in {16, 32, 64}. (bits('n), bits('n)) -> (bool, bits_fflags) +function feq_quiet(v1, v2) = { + let (s1, e1, m1) = fsplit(v1); + let (s2, e2, m2) = fsplit(v2); + + let v1Is0 = f_is_neg_zero(v1) | f_is_pos_zero(v1); + let v2Is0 = f_is_neg_zero(v2) | f_is_pos_zero(v2); + + let result = ((v1 == v2) | (v1Is0 & v2Is0)); + + let fflags = if (f_is_SNaN(v1) | f_is_SNaN(v2)) + then nvFlag + else zeros(); + + (result, fflags) +} + +// Note: this is currently unused. +val flt : forall 'n, 'n in {16, 32, 64}. (bits('n), bits('n), bool) -> (bool, bits_fflags) +function flt(v1, v2, is_quiet) = { + let (s1, e1, m1) = fsplit(v1); + let (s2, e2, m2) = fsplit(v2); + + let result : bool = + if (s1 == 0b0) & (s2 == 0b0) then + if (e1 == e2) + then unsigned (m1) < unsigned (m2) + else unsigned (e1) < unsigned (e2) + else if (s1 == 0b0) & (s2 == 0b1) + then false + else if (s1 == 0b1) & (s2 == 0b0) + then true + else + if (e1 == e2) + then unsigned (m1) > unsigned (m2) + else unsigned (e1) > unsigned (e2); + + let fflags = if is_quiet then + if (f_is_SNaN(v1) | f_is_SNaN(v2)) + then nvFlag + else zeros() + else + if (f_is_NaN(v1) | f_is_NaN(v2)) + then nvFlag + else zeros(); + + (result, fflags) +} + +val fle : forall 'n, 'n in {16, 32, 64}. (bits('n), bits('n), bool) -> (bool, bits_fflags) +function fle(v1, v2, is_quiet) = { + let (s1, e1, m1) = fsplit(v1); + let (s2, e2, m2) = fsplit(v2); + + let v1Is0 = f_is_neg_zero(v1) | f_is_pos_zero(v1); + let v2Is0 = f_is_neg_zero(v2) | f_is_pos_zero(v2); + + let result : bool = + if (s1 == 0b0) & (s2 == 0b0) then + if (e1 == e2) + then unsigned (m1) <= unsigned (m2) + else unsigned (e1) < unsigned (e2) + else if (s1 == 0b0) & (s2 == 0b1) + then (v1Is0 & v2Is0) /* Equal in this case (+0=-0) */ + else if (s1 == 0b1) & (s2 == 0b0) + then true + else + if (e1 == e2) + then unsigned (m1) >= unsigned (m2) + else unsigned (e1) > unsigned (e2); + + let fflags = if is_quiet then + if (f_is_SNaN(v1) | f_is_SNaN(v2)) + then nvFlag + else zeros() + else + if (f_is_NaN(v1) | f_is_NaN(v2)) + then nvFlag + else zeros(); + + (result, fflags) +} diff --git a/model/riscv_insts_dext.sail b/model/riscv_insts_dext.sail index 81e29e7aa..1ddc51288 100644 --- a/model/riscv_insts_dext.sail +++ b/model/riscv_insts_dext.sail @@ -29,93 +29,6 @@ /* In RISC-V, the D extension requires the F extension, so that */ /* should have been processed before this one. */ - - -/* **************************************************************** */ -/* Help functions used in the semantic functions */ - -val feq_quiet_D : (bits(64), bits (64)) -> (bool, bits(5)) -function feq_quiet_D (v1, v2) = { - let (s1, e1, m1) = fsplit (v1); - let (s2, e2, m2) = fsplit (v2); - - let v1Is0 = f_is_neg_zero(v1) | f_is_pos_zero(v1); - let v2Is0 = f_is_neg_zero(v2) | f_is_pos_zero(v2); - - let result = ((v1 == v2) | (v1Is0 & v2Is0)); - - let fflags = if (f_is_SNaN(v1) | f_is_SNaN(v2)) - then nvFlag() - else zeros(); - - (result, fflags) -} - -val flt_D : (bits(64), bits (64), bool) -> (bool, bits(5)) -function flt_D (v1, v2, is_quiet) = { - let (s1, e1, m1) = fsplit (v1); - let (s2, e2, m2) = fsplit (v2); - - let result : bool = - if (s1 == 0b0) & (s2 == 0b0) then - if (e1 == e2) - then unsigned (m1) < unsigned (m2) - else unsigned (e1) < unsigned (e2) - else if (s1 == 0b0) & (s2 == 0b1) then - false - else if (s1 == 0b1) & (s2 == 0b0) then - true - else - if (e1 == e2) - then unsigned (m1) > unsigned (m2) - else unsigned (e1) > unsigned (e2); - - let fflags = if is_quiet then - if (f_is_SNaN(v1) | f_is_SNaN(v2)) - then nvFlag() - else zeros() - else - if (f_is_NaN(v1) | f_is_NaN(v2)) - then nvFlag() - else zeros(); - - (result, fflags) -} - -val fle_D : (bits(64), bits (64), bool) -> (bool, bits(5)) -function fle_D (v1, v2, is_quiet) = { - let (s1, e1, m1) = fsplit (v1); - let (s2, e2, m2) = fsplit (v2); - - let v1Is0 = f_is_neg_zero(v1) | f_is_pos_zero(v1); - let v2Is0 = f_is_neg_zero(v2) | f_is_pos_zero(v2); - - let result : bool = - if (s1 == 0b0) & (s2 == 0b0) then - if (e1 == e2) - then unsigned (m1) <= unsigned (m2) - else unsigned (e1) < unsigned (e2) - else if (s1 == 0b0) & (s2 == 0b1) then - (v1Is0 & v2Is0) /* Equal in this case (+0=-0) */ - else if (s1 == 0b1) & (s2 == 0b0) then - true - else - if (e1 == e2) - then unsigned (m1) >= unsigned (m2) - else unsigned (e1) > unsigned (e2); - - let fflags = if is_quiet then - if (f_is_SNaN(v1) | f_is_SNaN(v2)) - then nvFlag() - else zeros() - else - if (f_is_NaN(v1) | f_is_NaN(v2)) - then nvFlag() - else zeros(); - - (result, fflags) -} - /* **************************************************************** */ /* Helper functions for 'encdec()' */ @@ -653,7 +566,7 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FMIN_D)) = { let rs2_val_D = F_or_X_D(rs2); let is_quiet = true; - let (rs1_lt_rs2, fflags) = fle_D (rs1_val_D, rs2_val_D, is_quiet); + let (rs1_lt_rs2, fflags) = fle(rs1_val_D, rs2_val_D, is_quiet); let rd_val_D = if (f_is_NaN(rs1_val_D) & f_is_NaN(rs2_val_D)) then canonical_NaN(64) else if f_is_NaN(rs1_val_D) then rs2_val_D @@ -673,7 +586,7 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FMAX_D)) = { let rs2_val_D = F_or_X_D(rs2); let is_quiet = true; - let (rs2_lt_rs1, fflags) = fle_D (rs2_val_D, rs1_val_D, is_quiet); + let (rs2_lt_rs1, fflags) = fle(rs2_val_D, rs1_val_D, is_quiet); let rd_val_D = if (f_is_NaN(rs1_val_D) & f_is_NaN(rs2_val_D)) then canonical_NaN(64) else if f_is_NaN(rs1_val_D) then rs2_val_D diff --git a/model/riscv_insts_fext.sail b/model/riscv_insts_fext.sail index 2e15fa033..0888811f1 100644 --- a/model/riscv_insts_fext.sail +++ b/model/riscv_insts_fext.sail @@ -56,100 +56,6 @@ function select_instr_or_fcsr_rm instr_rm = } else Some(instr_rm) -/* **************************************************************** */ -/* Floating point accrued exception flags */ - -function nxFlag() -> bits(5) = 0b_00001 -function ufFlag() -> bits(5) = 0b_00010 -function ofFlag() -> bits(5) = 0b_00100 -function dzFlag() -> bits(5) = 0b_01000 -function nvFlag() -> bits(5) = 0b_10000 - -/* **************************************************************** */ -/* Help functions used in the semantic functions */ - -val feq_quiet_S : (bits(32), bits (32)) -> (bool, bits(5)) -function feq_quiet_S (v1, v2) = { - let (s1, e1, m1) = fsplit (v1); - let (s2, e2, m2) = fsplit (v2); - - let v1Is0 = f_is_neg_zero(v1) | f_is_pos_zero(v1); - let v2Is0 = f_is_neg_zero(v2) | f_is_pos_zero(v2); - - let result = ((v1 == v2) | (v1Is0 & v2Is0)); - - let fflags = if (f_is_SNaN(v1) | f_is_SNaN(v2)) - then nvFlag() - else zeros(); - - (result, fflags) -} - -val flt_S : (bits(32), bits (32), bool) -> (bool, bits(5)) -function flt_S (v1, v2, is_quiet) = { - let (s1, e1, m1) = fsplit (v1); - let (s2, e2, m2) = fsplit (v2); - - let result : bool = - if (s1 == 0b0) & (s2 == 0b0) then - if (e1 == e2) - then unsigned (m1) < unsigned (m2) - else unsigned (e1) < unsigned (e2) - else if (s1 == 0b0) & (s2 == 0b1) - then false - else if (s1 == 0b1) & (s2 == 0b0) - then true - else - if (e1 == e2) - then unsigned (m1) > unsigned (m2) - else unsigned (e1) > unsigned (e2); - - let fflags = if is_quiet then - if (f_is_SNaN(v1) | f_is_SNaN(v2)) - then nvFlag() - else zeros() - else - if (f_is_NaN(v1) | f_is_NaN(v2)) - then nvFlag() - else zeros(); - - (result, fflags) -} - -val fle_S : (bits(32), bits (32), bool) -> (bool, bits(5)) -function fle_S (v1, v2, is_quiet) = { - let (s1, e1, m1) = fsplit (v1); - let (s2, e2, m2) = fsplit (v2); - - let v1Is0 = f_is_neg_zero(v1) | f_is_pos_zero(v1); - let v2Is0 = f_is_neg_zero(v2) | f_is_pos_zero(v2); - - let result : bool = - if (s1 == 0b0) & (s2 == 0b0) then - if (e1 == e2) - then unsigned (m1) <= unsigned (m2) - else unsigned (e1) < unsigned (e2) - else if (s1 == 0b0) & (s2 == 0b1) - then (v1Is0 & v2Is0) /* Equal in this case (+0=-0) */ - else if (s1 == 0b1) & (s2 == 0b0) - then true - else - if (e1 == e2) - then unsigned (m1) >= unsigned (m2) - else unsigned (e1) > unsigned (e2); - - let fflags = if is_quiet then - if (f_is_SNaN(v1) | f_is_SNaN(v2)) - then nvFlag() - else zeros() - else - if (f_is_NaN(v1) | f_is_NaN(v2)) - then nvFlag() - else zeros(); - - (result, fflags) -} - /* **************************************************************** */ /* Helper functions for 'encdec()' */ @@ -776,7 +682,7 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FMIN_S)) = { let rs2_val_S = F_or_X_S(rs2); let is_quiet = true; - let (rs1_lt_rs2, fflags) = fle_S (rs1_val_S, rs2_val_S, is_quiet); + let (rs1_lt_rs2, fflags) = fle(rs1_val_S, rs2_val_S, is_quiet); let rd_val_S = if (f_is_NaN(rs1_val_S) & f_is_NaN(rs2_val_S)) then canonical_NaN(32) else if f_is_NaN(rs1_val_S) then rs2_val_S @@ -796,7 +702,7 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FMAX_S)) = { let rs2_val_S = F_or_X_S(rs2); let is_quiet = true; - let (rs2_lt_rs1, fflags) = fle_S (rs2_val_S, rs1_val_S, is_quiet); + let (rs2_lt_rs1, fflags) = fle(rs2_val_S, rs1_val_S, is_quiet); let rd_val_S = if (f_is_NaN(rs1_val_S) & f_is_NaN(rs2_val_S)) then canonical_NaN(32) else if f_is_NaN(rs1_val_S) then rs2_val_S diff --git a/model/riscv_insts_vext_utils.sail b/model/riscv_insts_vext_utils.sail index 12e29aa38..5b6d28de0 100755 --- a/model/riscv_insts_vext_utils.sail +++ b/model/riscv_insts_vext_utils.sail @@ -725,45 +725,45 @@ function fp_widen(nval) = { val riscv_f16ToI16 : (bits_rm, bits_H) -> (bits_fflags, bits(16)) function riscv_f16ToI16 (rm, v) = { let (_, sig32) = riscv_f16ToI32(rm, v); - if signed(sig32) > signed(0b0 @ ones(15)) then (nvFlag(), 0b0 @ ones(15)) - else if signed(sig32) < signed(0b1 @ zeros(15)) then (nvFlag(), 0b1 @ zeros(15)) + if signed(sig32) > signed(0b0 @ ones(15)) then (nvFlag, 0b0 @ ones(15)) + else if signed(sig32) < signed(0b1 @ zeros(15)) then (nvFlag, 0b1 @ zeros(15)) else (zeros(5), sig32[15 .. 0]); } val riscv_f16ToI8 : (bits_rm, bits_H) -> (bits_fflags, bits(8)) function riscv_f16ToI8 (rm, v) = { let (_, sig32) = riscv_f16ToI32(rm, v); - if signed(sig32) > signed(0b0 @ ones(7)) then (nvFlag(), 0b0 @ ones(7)) - else if signed(sig32) < signed(0b1 @ zeros(7)) then (nvFlag(), 0b1 @ zeros(7)) + if signed(sig32) > signed(0b0 @ ones(7)) then (nvFlag, 0b0 @ ones(7)) + else if signed(sig32) < signed(0b1 @ zeros(7)) then (nvFlag, 0b1 @ zeros(7)) else (zeros(5), sig32[7 .. 0]); } val riscv_f32ToI16 : (bits_rm, bits_S) -> (bits_fflags, bits(16)) function riscv_f32ToI16 (rm, v) = { let (_, sig32) = riscv_f32ToI32(rm, v); - if signed(sig32) > signed(0b0 @ ones(15)) then (nvFlag(), 0b0 @ ones(15)) - else if signed(sig32) < signed(0b1 @ zeros(15)) then (nvFlag(), 0b1 @ zeros(15)) + if signed(sig32) > signed(0b0 @ ones(15)) then (nvFlag, 0b0 @ ones(15)) + else if signed(sig32) < signed(0b1 @ zeros(15)) then (nvFlag, 0b1 @ zeros(15)) else (zeros(5), sig32[15 .. 0]); } val riscv_f16ToUi16 : (bits_rm, bits_H) -> (bits_fflags, bits(16)) function riscv_f16ToUi16 (rm, v) = { let (_, sig32) = riscv_f16ToUi32(rm, v); - if unsigned(sig32) > unsigned(ones(16)) then (nvFlag(), ones(16)) + if unsigned(sig32) > unsigned(ones(16)) then (nvFlag, ones(16)) else (zeros(5), sig32[15 .. 0]); } val riscv_f16ToUi8 : (bits_rm, bits_H) -> (bits_fflags, bits(8)) function riscv_f16ToUi8 (rm, v) = { let (_, sig32) = riscv_f16ToUi32(rm, v); - if unsigned(sig32) > unsigned(ones(8)) then (nvFlag(), ones(8)) + if unsigned(sig32) > unsigned(ones(8)) then (nvFlag, ones(8)) else (zeros(5), sig32[7 .. 0]); } val riscv_f32ToUi16 : (bits_rm, bits_S) -> (bits_fflags, bits(16)) function riscv_f32ToUi16 (rm, v) = { let (_, sig32) = riscv_f32ToUi32(rm, v); - if unsigned(sig32) > unsigned(ones(16)) then (nvFlag(), ones(16)) + if unsigned(sig32) > unsigned(ones(16)) then (nvFlag, ones(16)) else (zeros(5), sig32[15 .. 0]); } @@ -826,13 +826,13 @@ function rsqrt7 (v, sub) = { val riscv_f16Rsqrte7 : (bits_rm, bits_H) -> (bits_fflags, bits_H) function riscv_f16Rsqrte7 (rm, v) = { match fp_class(v) { - 0x0001 => (nvFlag(), 0x7e00), - 0x0002 => (nvFlag(), 0x7e00), - 0x0004 => (nvFlag(), 0x7e00), - 0x0100 => (nvFlag(), 0x7e00), + 0x0001 => (nvFlag, 0x7e00), + 0x0002 => (nvFlag, 0x7e00), + 0x0004 => (nvFlag, 0x7e00), + 0x0100 => (nvFlag, 0x7e00), 0x0200 => (zeros(5), 0x7e00), - 0x0008 => (dzFlag(), 0xfc00), - 0x0010 => (dzFlag(), 0x7c00), + 0x0008 => (dzFlag, 0xfc00), + 0x0010 => (dzFlag, 0x7c00), 0x0080 => (zeros(5), 0x0000), 0x0020 => (zeros(5), rsqrt7(v, true)[15 .. 0]), _ => (zeros(5), rsqrt7(v, false)[15 .. 0]) @@ -842,13 +842,13 @@ function riscv_f16Rsqrte7 (rm, v) = { val riscv_f32Rsqrte7 : (bits_rm, bits_S) -> (bits_fflags, bits_S) function riscv_f32Rsqrte7 (rm, v) = { match fp_class(v)[15 .. 0] { - 0x0001 => (nvFlag(), 0x7fc00000), - 0x0002 => (nvFlag(), 0x7fc00000), - 0x0004 => (nvFlag(), 0x7fc00000), - 0x0100 => (nvFlag(), 0x7fc00000), + 0x0001 => (nvFlag, 0x7fc00000), + 0x0002 => (nvFlag, 0x7fc00000), + 0x0004 => (nvFlag, 0x7fc00000), + 0x0100 => (nvFlag, 0x7fc00000), 0x0200 => (zeros(5), 0x7fc00000), - 0x0008 => (dzFlag(), 0xff800000), - 0x0010 => (dzFlag(), 0x7f800000), + 0x0008 => (dzFlag, 0xff800000), + 0x0010 => (dzFlag, 0x7f800000), 0x0080 => (zeros(5), 0x00000000), 0x0020 => (zeros(5), rsqrt7(v, true)[31 .. 0]), _ => (zeros(5), rsqrt7(v, false)[31 .. 0]) @@ -858,13 +858,13 @@ function riscv_f32Rsqrte7 (rm, v) = { val riscv_f64Rsqrte7 : (bits_rm, bits_D) -> (bits_fflags, bits_D) function riscv_f64Rsqrte7 (rm, v) = { match fp_class(v)[15 .. 0] { - 0x0001 => (nvFlag(), 0x7ff8000000000000), - 0x0002 => (nvFlag(), 0x7ff8000000000000), - 0x0004 => (nvFlag(), 0x7ff8000000000000), - 0x0100 => (nvFlag(), 0x7ff8000000000000), + 0x0001 => (nvFlag, 0x7ff8000000000000), + 0x0002 => (nvFlag, 0x7ff8000000000000), + 0x0004 => (nvFlag, 0x7ff8000000000000), + 0x0100 => (nvFlag, 0x7ff8000000000000), 0x0200 => (zeros(5), 0x7ff8000000000000), - 0x0008 => (dzFlag(), 0xfff0000000000000), - 0x0010 => (dzFlag(), 0x7ff0000000000000), + 0x0008 => (dzFlag, 0xfff0000000000000), + 0x0010 => (dzFlag, 0x7ff0000000000000), 0x0080 => (zeros(5), zeros(64)), 0x0020 => (zeros(5), rsqrt7(v, true)[63 .. 0]), _ => (zeros(5), rsqrt7(v, false)[63 .. 0]) @@ -937,13 +937,13 @@ function riscv_f16Recip7 (rm, v) = { match fp_class(v) { 0x0001 => (zeros(5), 0x8000), 0x0080 => (zeros(5), 0x0000), - 0x0008 => (dzFlag(), 0xfc00), - 0x0010 => (dzFlag(), 0x7c00), - 0x0100 => (nvFlag(), 0x7e00), + 0x0008 => (dzFlag, 0xfc00), + 0x0010 => (dzFlag, 0x7c00), + 0x0100 => (nvFlag, 0x7e00), 0x0200 => (zeros(5), 0x7e00), - 0x0004 => if round_abnormal_true then (nxFlag() | ofFlag(), res_true[15 .. 0]) else (zeros(5), res_true[15 .. 0]), - 0x0020 => if round_abnormal_true then (nxFlag() | ofFlag(), res_true[15 .. 0]) else (zeros(5), res_true[15 .. 0]), - _ => if round_abnormal_false then (nxFlag() | ofFlag(), res_false[15 .. 0]) else (zeros(5), res_false[15 .. 0]) + 0x0004 => if round_abnormal_true then (nxFlag | ofFlag, res_true[15 .. 0]) else (zeros(5), res_true[15 .. 0]), + 0x0020 => if round_abnormal_true then (nxFlag | ofFlag, res_true[15 .. 0]) else (zeros(5), res_true[15 .. 0]), + _ => if round_abnormal_false then (nxFlag | ofFlag, res_false[15 .. 0]) else (zeros(5), res_false[15 .. 0]) } } @@ -954,13 +954,13 @@ function riscv_f32Recip7 (rm, v) = { match fp_class(v)[15 .. 0] { 0x0001 => (zeros(5), 0x80000000), 0x0080 => (zeros(5), 0x00000000), - 0x0008 => (dzFlag(), 0xff800000), - 0x0010 => (dzFlag(), 0x7f800000), - 0x0100 => (nvFlag(), 0x7fc00000), + 0x0008 => (dzFlag, 0xff800000), + 0x0010 => (dzFlag, 0x7f800000), + 0x0100 => (nvFlag, 0x7fc00000), 0x0200 => (zeros(5), 0x7fc00000), - 0x0004 => if round_abnormal_true then (nxFlag() | ofFlag(), res_true[31 .. 0]) else (zeros(5), res_true[31 .. 0]), - 0x0020 => if round_abnormal_true then (nxFlag() | ofFlag(), res_true[31 .. 0]) else (zeros(5), res_true[31 .. 0]), - _ => if round_abnormal_false then (nxFlag() | ofFlag(), res_false[31 .. 0]) else (zeros(5), res_false[31 .. 0]) + 0x0004 => if round_abnormal_true then (nxFlag | ofFlag, res_true[31 .. 0]) else (zeros(5), res_true[31 .. 0]), + 0x0020 => if round_abnormal_true then (nxFlag | ofFlag, res_true[31 .. 0]) else (zeros(5), res_true[31 .. 0]), + _ => if round_abnormal_false then (nxFlag | ofFlag, res_false[31 .. 0]) else (zeros(5), res_false[31 .. 0]) } } @@ -971,12 +971,12 @@ function riscv_f64Recip7 (rm, v) = { match fp_class(v)[15 .. 0] { 0x0001 => (zeros(5), 0x8000000000000000), 0x0080 => (zeros(5), 0x0000000000000000), - 0x0008 => (dzFlag(), 0xfff0000000000000), - 0x0010 => (dzFlag(), 0x7ff0000000000000), - 0x0100 => (nvFlag(), 0x7ff8000000000000), + 0x0008 => (dzFlag, 0xfff0000000000000), + 0x0010 => (dzFlag, 0x7ff0000000000000), + 0x0100 => (nvFlag, 0x7ff8000000000000), 0x0200 => (zeros(5), 0x7ff8000000000000), - 0x0004 => if round_abnormal_true then (nxFlag() | ofFlag(), res_true[63 .. 0]) else (zeros(5), res_true[63 .. 0]), - 0x0020 => if round_abnormal_true then (nxFlag() | ofFlag(), res_true[63 .. 0]) else (zeros(5), res_true[63 .. 0]), - _ => if round_abnormal_false then (nxFlag() | ofFlag(), res_false[63 .. 0]) else (zeros(5), res_false[63 .. 0]) + 0x0004 => if round_abnormal_true then (nxFlag | ofFlag, res_true[63 .. 0]) else (zeros(5), res_true[63 .. 0]), + 0x0020 => if round_abnormal_true then (nxFlag | ofFlag, res_true[63 .. 0]) else (zeros(5), res_true[63 .. 0]), + _ => if round_abnormal_false then (nxFlag | ofFlag, res_false[63 .. 0]) else (zeros(5), res_false[63 .. 0]) } } diff --git a/model/riscv_insts_zfa.sail b/model/riscv_insts_zfa.sail index 0b6e3b89e..29a988535 100644 --- a/model/riscv_insts_zfa.sail +++ b/model/riscv_insts_zfa.sail @@ -170,7 +170,7 @@ function clause execute (RISCV_FMINM_H(rs2, rs1, rd)) = { let rs2_val_H = F_box(16, rs2); let is_quiet = true; - let (rs1_lt_rs2, fflags) = fle_H (rs1_val_H, rs2_val_H, is_quiet); + let (rs1_lt_rs2, fflags) = fle(rs1_val_H, rs2_val_H, is_quiet); let rd_val_H = if (f_is_NaN(rs1_val_H) | f_is_NaN(rs2_val_H)) then canonical_NaN(16) else if (f_is_neg_zero(rs1_val_H) & f_is_pos_zero(rs2_val_H)) then rs1_val_H @@ -200,7 +200,7 @@ function clause execute (RISCV_FMAXM_H(rs2, rs1, rd)) = { let rs2_val_H = F_box(16, rs2); let is_quiet = true; - let (rs2_lt_rs1, fflags) = fle_H (rs2_val_H, rs1_val_H, is_quiet); + let (rs2_lt_rs1, fflags) = fle(rs2_val_H, rs1_val_H, is_quiet); let rd_val_H = if (f_is_NaN(rs1_val_H) | f_is_NaN(rs2_val_H)) then canonical_NaN(16) else if (f_is_neg_zero(rs1_val_H) & f_is_pos_zero(rs2_val_H)) then rs2_val_H @@ -230,7 +230,7 @@ function clause execute (RISCV_FMINM_S(rs2, rs1, rd)) = { let rs2_val_S = F_box(32, rs2); let is_quiet = true; - let (rs1_lt_rs2, fflags) = fle_S (rs1_val_S, rs2_val_S, is_quiet); + let (rs1_lt_rs2, fflags) = fle(rs1_val_S, rs2_val_S, is_quiet); let rd_val_S = if (f_is_NaN(rs1_val_S) | f_is_NaN(rs2_val_S)) then canonical_NaN(32) else if (f_is_neg_zero(rs1_val_S) & f_is_pos_zero(rs2_val_S)) then rs1_val_S @@ -260,7 +260,7 @@ function clause execute (RISCV_FMAXM_S(rs2, rs1, rd)) = { let rs2_val_S = F_box(32, rs2); let is_quiet = true; - let (rs2_lt_rs1, fflags) = fle_S (rs2_val_S, rs1_val_S, is_quiet); + let (rs2_lt_rs1, fflags) = fle(rs2_val_S, rs1_val_S, is_quiet); let rd_val_S = if (f_is_NaN(rs1_val_S) | f_is_NaN(rs2_val_S)) then canonical_NaN(32) else if (f_is_neg_zero(rs1_val_S) & f_is_pos_zero(rs2_val_S)) then rs2_val_S @@ -290,7 +290,7 @@ function clause execute (RISCV_FMINM_D(rs2, rs1, rd)) = { let rs2_val_D = F_box(64, rs2); let is_quiet = true; - let (rs1_lt_rs2, fflags) = fle_D (rs1_val_D, rs2_val_D, is_quiet); + let (rs1_lt_rs2, fflags) = fle(rs1_val_D, rs2_val_D, is_quiet); let rd_val_D = if (f_is_NaN(rs1_val_D) | f_is_NaN(rs2_val_D)) then canonical_NaN(64) else if (f_is_neg_zero(rs1_val_D) & f_is_pos_zero(rs2_val_D)) then rs1_val_D @@ -320,7 +320,7 @@ function clause execute (RISCV_FMAXM_D(rs2, rs1, rd)) = { let rs2_val_D = F_box(64, rs2); let is_quiet = true; - let (rs2_lt_rs1, fflags) = fle_D (rs2_val_D, rs1_val_D, is_quiet); + let (rs2_lt_rs1, fflags) = fle(rs2_val_D, rs1_val_D, is_quiet); let rd_val_D = if (f_is_NaN(rs1_val_D) | f_is_NaN(rs2_val_D)) then canonical_NaN(64) else if (f_is_neg_zero(rs1_val_D) & f_is_pos_zero(rs2_val_D)) then rs2_val_D @@ -721,11 +721,11 @@ function fcvtmod_helper(x64) = { let is_too_large = true_exp >= 84; /* bits will be 'multiplied' out */ let is_too_small = true_exp < 0; /* bits will be 'divided' out */ - if is_zero then (zeros(), zeros()) - else if is_subnorm then (nxFlag(), zeros()) - else if is_nan_or_inf then (nvFlag(), zeros()) - else if is_too_large then (nvFlag(), zeros()) - else if is_too_small then (nxFlag(), zeros()) + if is_zero then (zeros(), zeros()) + else if is_subnorm then (nxFlag, zeros()) + else if is_nan_or_inf then (nvFlag, zeros()) + else if is_too_large then (nvFlag, zeros()) + else if is_too_small then (nxFlag, zeros()) else { /* * Calculate the low 32 bits of the integer value from the @@ -745,8 +745,8 @@ function fcvtmod_helper(x64) = { else integer; /* Raise FP exception flags, honoring the precedence of nV > nX */ - let flags : bits(5) = if (true_exp > 31) then nvFlag() - else if (fractional != zeros()) then nxFlag() + let flags : bits(5) = if (true_exp > 31) then nvFlag + else if (fractional != zeros()) then nxFlag else zeros(); (flags, result) diff --git a/model/riscv_insts_zfh.sail b/model/riscv_insts_zfh.sail index 029e1e13c..8b0301ace 100644 --- a/model/riscv_insts_zfh.sail +++ b/model/riscv_insts_zfh.sail @@ -23,42 +23,6 @@ /* this correspondence as the files are maintained for bug-fixes, */ /* improvements, and version updates. */ -/* **************************************************************** */ - -val fle_H : (bits(16), bits (16), bool) -> (bool, bits(5)) -function fle_H (v1, v2, is_quiet) = { - let (s1, e1, m1) = fsplit (v1); - let (s2, e2, m2) = fsplit (v2); - - let v1Is0 = f_is_neg_zero(v1) | f_is_pos_zero(v1); - let v2Is0 = f_is_neg_zero(v2) | f_is_pos_zero(v2); - - let result : bool = - if (s1 == 0b0) & (s2 == 0b0) then - if (e1 == e2) - then unsigned (m1) <= unsigned (m2) - else unsigned (e1) < unsigned (e2) - else if (s1 == 0b0) & (s2 == 0b1) - then (v1Is0 & v2Is0) /* Equal in this case (+0=-0) */ - else if (s1 == 0b1) & (s2 == 0b0) - then true - else - if (e1 == e2) - then unsigned (m1) >= unsigned (m2) - else unsigned (e1) > unsigned (e2); - - let fflags = if is_quiet then - if (f_is_SNaN(v1) | f_is_SNaN(v2)) - then nvFlag() - else zeros() - else - if (f_is_NaN(v1) | f_is_NaN(v2)) - then nvFlag() - else zeros(); - - (result, fflags) -} - /* **************************************************************** */ /* Helper functions for 'encdec()' */ @@ -273,7 +237,7 @@ function clause execute (F_BIN_TYPE_H(rs2, rs1, rd, FMIN_H)) = { let rs2_val_H = F_or_X_H(rs2); let is_quiet = true; - let (rs1_lt_rs2, fflags) = fle_H (rs1_val_H, rs2_val_H, is_quiet); + let (rs1_lt_rs2, fflags) = fle(rs1_val_H, rs2_val_H, is_quiet); let rd_val_H = if (f_is_NaN(rs1_val_H) & f_is_NaN(rs2_val_H)) then canonical_NaN(16) else if f_is_NaN(rs1_val_H) then rs2_val_H @@ -293,7 +257,7 @@ function clause execute (F_BIN_TYPE_H(rs2, rs1, rd, FMAX_H)) = { let rs2_val_H = F_or_X_H(rs2); let is_quiet = true; - let (rs2_lt_rs1, fflags) = fle_H (rs2_val_H, rs1_val_H, is_quiet); + let (rs2_lt_rs1, fflags) = fle(rs2_val_H, rs1_val_H, is_quiet); let rd_val_H = if (f_is_NaN(rs1_val_H) & f_is_NaN(rs2_val_H)) then canonical_NaN(16) else if f_is_NaN(rs1_val_H) then rs2_val_H