Skip to content

Commit

Permalink
Simplify float by making le/lt/eq functions generic
Browse files Browse the repository at this point in the history 
I'm not sure of the exact history here but only the le function is actually used. I left the other two in for reference.

I also changed the flags from functions to global constants, since that's what they are.
  • Loading branch information
@Timmmm
Timmmm committed Apr 4, 2024
1 parent 38fc8ac commit eb681d3
Show file tree
Hide file tree
Showing 7 changed files with 159 additions and 282 deletions.
2 changes: 1 addition & 1 deletion Makefile
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
94 changes: 94 additions & 0 deletions model/riscv_float.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
}
91 changes: 2 additions & 89 deletions model/riscv_insts_dext.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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()' */

Expand Down Expand Up @@ -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
Expand All @@ -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
Expand Down
98 changes: 2 additions & 96 deletions model/riscv_insts_fext.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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()' */

Expand Down Expand Up @@ -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
Expand All @@ -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
Expand Down
Loading

0 comments on commit eb681d3

Please sign in to comment.