From be903ec12c18655b920863238e4b0aa0c49367dd Mon Sep 17 00:00:00 2001 From: KotorinMinami Date: Fri, 27 Sep 2024 10:37:38 +0800 Subject: [PATCH] replace fsplit and fmake with mapping fstruct --- model/riscv_insts_dext.sail | 63 +++++++++++++++++++---------------- model/riscv_insts_fext.sail | 65 ++++++++++++++++++++----------------- model/riscv_insts_zfa.sail | 2 +- model/riscv_insts_zfh.sail | 56 ++++++++++++++++++-------------- 4 files changed, 104 insertions(+), 82 deletions(-) diff --git a/model/riscv_insts_dext.sail b/model/riscv_insts_dext.sail index 22e3d936f..8f86ec124 100644 --- a/model/riscv_insts_dext.sail +++ b/model/riscv_insts_dext.sail @@ -32,18 +32,25 @@ /* **************************************************************** */ /* S and D value structure (sign, exponent, mantissa) */ -/* TODO: this should be a 'mapping' */ val fsplit_D : bits(64) -> (bits(1), bits(11), bits(52)) function fsplit_D x64 = (x64[63..63], x64[62..52], x64[51..0]) val fmake_D : (bits(1), bits(11), bits(52)) -> bits(64) function fmake_D (sign, exp, mant) = sign @ exp @ mant +val fExtractor_D : bits(64) <-> (bits(1), bits(11), bits(52)) +function fExtractor_D_forwards(x64) = fsplit_D(x64) +function fExtractor_D_forwards_matches(x64) = true +function fExtractor_D_backwards(sign, exp, mant) = fmake_D(sign, exp, mant) +function fExtractor_D_backwards_matches(sign, exp, mant) = true + +mapping fstruct_D : bits(64) <-> (bits(1), bits(11), bits(52)) = {fExtractor_D(sign, exp, mant) <-> (sign, exp, mant)} + /* ---- Structure tests */ val f_is_neg_inf_D : bits(64) -> bool function f_is_neg_inf_D x64 = { - let (sign, exp, mant) = fsplit_D (x64); + let (sign, exp, mant) = fstruct_D (x64); ( (sign == 0b1) & (exp == ones()) & (mant == zeros())) @@ -51,7 +58,7 @@ function f_is_neg_inf_D x64 = { val f_is_neg_norm_D : bits(64) -> bool function f_is_neg_norm_D x64 = { - let (sign, exp, mant) = fsplit_D (x64); + let (sign, exp, mant) = fstruct_D (x64); ( (sign == 0b1) & (exp != zeros()) & (exp != ones())) @@ -59,7 +66,7 @@ function f_is_neg_norm_D x64 = { val f_is_neg_subnorm_D : bits(64) -> bool function f_is_neg_subnorm_D x64 = { - let (sign, exp, mant) = fsplit_D (x64); + let (sign, exp, mant) = fstruct_D (x64); ( (sign == 0b1) & (exp == zeros()) & (mant != zeros())) @@ -67,7 +74,7 @@ function f_is_neg_subnorm_D x64 = { val f_is_neg_zero_D : bits(64) -> bool function f_is_neg_zero_D x64 = { - let (sign, exp, mant) = fsplit_D (x64); + let (sign, exp, mant) = fstruct_D (x64); ( (sign == ones()) & (exp == zeros()) & (mant == zeros())) @@ -75,7 +82,7 @@ function f_is_neg_zero_D x64 = { val f_is_pos_zero_D : bits(64) -> bool function f_is_pos_zero_D x64 = { - let (sign, exp, mant) = fsplit_D (x64); + let (sign, exp, mant) = fstruct_D (x64); ( (sign == zeros()) & (exp == zeros()) & (mant == zeros())) @@ -83,7 +90,7 @@ function f_is_pos_zero_D x64 = { val f_is_pos_subnorm_D : bits(64) -> bool function f_is_pos_subnorm_D x64 = { - let (sign, exp, mant) = fsplit_D (x64); + let (sign, exp, mant) = fstruct_D (x64); ( (sign == zeros()) & (exp == zeros()) & (mant != zeros())) @@ -91,7 +98,7 @@ function f_is_pos_subnorm_D x64 = { val f_is_pos_norm_D : bits(64) -> bool function f_is_pos_norm_D x64 = { - let (sign, exp, mant) = fsplit_D (x64); + let (sign, exp, mant) = fstruct_D (x64); ( (sign == zeros()) & (exp != zeros()) & (exp != ones())) @@ -99,7 +106,7 @@ function f_is_pos_norm_D x64 = { val f_is_pos_inf_D : bits(64) -> bool function f_is_pos_inf_D x64 = { - let (sign, exp, mant) = fsplit_D (x64); + let (sign, exp, mant) = fstruct_D (x64); ( (sign == zeros()) & (exp == ones()) & (mant == zeros())) @@ -107,7 +114,7 @@ function f_is_pos_inf_D x64 = { val f_is_SNaN_D : bits(64) -> bool function f_is_SNaN_D x64 = { - let (sign, exp, mant) = fsplit_D (x64); + let (sign, exp, mant) = fstruct_D (x64); ( (exp == ones()) & (mant [51] == bitzero) & (mant != zeros())) @@ -115,7 +122,7 @@ function f_is_SNaN_D x64 = { val f_is_QNaN_D : bits(64) -> bool function f_is_QNaN_D x64 = { - let (sign, exp, mant) = fsplit_D (x64); + let (sign, exp, mant) = fstruct_D (x64); ( (exp == ones()) & (mant [51] == bitone)) } @@ -123,7 +130,7 @@ function f_is_QNaN_D x64 = { /* Either QNaN or SNan */ val f_is_NaN_D : bits(64) -> bool function f_is_NaN_D x64 = { - let (sign, exp, mant) = fsplit_D (x64); + let (sign, exp, mant) = fstruct_D (x64); ( (exp == ones()) & (mant != zeros())) } @@ -134,15 +141,15 @@ function f_is_NaN_D x64 = { val negate_D : bits(64) -> bits(64) function negate_D (x64) = { - let (sign, exp, mant) = fsplit_D (x64); + let (sign, exp, mant) = fstruct_D (x64); let new_sign = if (sign == 0b0) then 0b1 else 0b0; fmake_D (new_sign, exp, mant) } val feq_quiet_D : (bits(64), bits (64)) -> (bool, bits(5)) function feq_quiet_D (v1, v2) = { - let (s1, e1, m1) = fsplit_D (v1); - let (s2, e2, m2) = fsplit_D (v2); + let (s1, e1, m1) = fstruct_D (v1); + let (s2, e2, m2) = fstruct_D (v2); let v1Is0 = f_is_neg_zero_D(v1) | f_is_pos_zero_D(v1); let v2Is0 = f_is_neg_zero_D(v2) | f_is_pos_zero_D(v2); @@ -158,8 +165,8 @@ function feq_quiet_D (v1, v2) = { val flt_D : (bits(64), bits (64), bool) -> (bool, bits(5)) function flt_D (v1, v2, is_quiet) = { - let (s1, e1, m1) = fsplit_D (v1); - let (s2, e2, m2) = fsplit_D (v2); + let (s1, e1, m1) = fstruct_D (v1); + let (s2, e2, m2) = fstruct_D (v2); let result : bool = if (s1 == 0b0) & (s2 == 0b0) then @@ -189,8 +196,8 @@ function flt_D (v1, v2, is_quiet) = { val fle_D : (bits(64), bits (64), bool) -> (bool, bits(5)) function fle_D (v1, v2, is_quiet) = { - let (s1, e1, m1) = fsplit_D (v1); - let (s2, e2, m2) = fsplit_D (v2); + let (s1, e1, m1) = fstruct_D (v1); + let (s2, e2, m2) = fstruct_D (v2); let v1Is0 = f_is_neg_zero_D(v1) | f_is_pos_zero_D(v1); let v2Is0 = f_is_neg_zero_D(v2) | f_is_pos_zero_D(v2); @@ -726,9 +733,9 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FSGNJ_D)) = { let rs1_val_D = F_or_X_D(rs1); let rs2_val_D = F_or_X_D(rs2); - let (s1, e1, m1) = fsplit_D (rs1_val_D); - let (s2, e2, m2) = fsplit_D (rs2_val_D); - let rd_val_D = fmake_D (s2, e1, m1); + let (s1, e1, m1) = fstruct_D (rs1_val_D); + let (s2, e2, m2) = fstruct_D (rs2_val_D); + let rd_val_D = fstruct_D ((s2, e1, m1)); F_or_X_D(rd) = rd_val_D; RETIRE_SUCCESS @@ -737,9 +744,9 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FSGNJ_D)) = { function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FSGNJN_D)) = { let rs1_val_D = F_or_X_D(rs1); let rs2_val_D = F_or_X_D(rs2); - let (s1, e1, m1) = fsplit_D (rs1_val_D); - let (s2, e2, m2) = fsplit_D (rs2_val_D); - let rd_val_D = fmake_D (0b1 ^ s2, e1, m1); + let (s1, e1, m1) = fstruct_D (rs1_val_D); + let (s2, e2, m2) = fstruct_D (rs2_val_D); + let rd_val_D = fstruct_D ((0b1 ^ s2, e1, m1)); F_or_X_D(rd) = rd_val_D; RETIRE_SUCCESS @@ -748,9 +755,9 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FSGNJN_D)) = { function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FSGNJX_D)) = { let rs1_val_D = F_or_X_D(rs1); let rs2_val_D = F_or_X_D(rs2); - let (s1, e1, m1) = fsplit_D (rs1_val_D); - let (s2, e2, m2) = fsplit_D (rs2_val_D); - let rd_val_D = fmake_D (s1 ^ s2, e1, m1); + let (s1, e1, m1) = fstruct_D (rs1_val_D); + let (s2, e2, m2) = fstruct_D (rs2_val_D); + let rd_val_D = fstruct_D ((s1 ^ s2, e1, m1)); F_or_X_D(rd) = rd_val_D; RETIRE_SUCCESS diff --git a/model/riscv_insts_fext.sail b/model/riscv_insts_fext.sail index 3a5509ea4..da4bf6993 100644 --- a/model/riscv_insts_fext.sail +++ b/model/riscv_insts_fext.sail @@ -71,18 +71,25 @@ function nvFlag() -> bits(5) = 0b_10000 /* **************************************************************** */ /* S and D value structure (sign, exponent, mantissa) */ -/* TODO: this should be a 'mapping' */ val fsplit_S : bits(32) -> (bits(1), bits(8), bits(23)) function fsplit_S x32 = (x32[31..31], x32[30..23], x32[22..0]) val fmake_S : (bits(1), bits(8), bits(23)) -> bits(32) function fmake_S (sign, exp, mant) = sign @ exp @ mant +val fExtractor_S : bits(32) <-> (bits(1), bits(8), bits(23)) +function fExtractor_S_forwards(x32) = fsplit_S(x32) +function fExtractor_S_forwards_matches(x32) = true +function fExtractor_S_backwards(sign, exp, mant) = fmake_S(sign, exp, mant) +function fExtractor_S_backwards_matches(sign, exp, mant) = true + +mapping fstruct_S : bits(32) <-> (bits(1), bits(8), bits(23)) = {fExtractor_S(sign, exp, mant) <-> (sign, exp, mant)} + /* ---- Structure tests */ val f_is_neg_inf_S : bits(32) -> bool function f_is_neg_inf_S x32 = { - let (sign, exp, mant) = fsplit_S (x32); + let (sign, exp, mant) = fstruct_S (x32); ( (sign == 0b1) & (exp == ones()) & (mant == zeros())) @@ -90,7 +97,7 @@ function f_is_neg_inf_S x32 = { val f_is_neg_norm_S : bits(32) -> bool function f_is_neg_norm_S x32 = { - let (sign, exp, mant) = fsplit_S (x32); + let (sign, exp, mant) = fstruct_S (x32); ( (sign == 0b1) & (exp != zeros()) & (exp != ones())) @@ -98,7 +105,7 @@ function f_is_neg_norm_S x32 = { val f_is_neg_subnorm_S : bits(32) -> bool function f_is_neg_subnorm_S x32 = { - let (sign, exp, mant) = fsplit_S (x32); + let (sign, exp, mant) = fstruct_S (x32); ( (sign == 0b1) & (exp == zeros()) & (mant != zeros())) @@ -106,7 +113,7 @@ function f_is_neg_subnorm_S x32 = { val f_is_neg_zero_S : bits(32) -> bool function f_is_neg_zero_S x32 = { - let (sign, exp, mant) = fsplit_S (x32); + let (sign, exp, mant) = fstruct_S (x32); ( (sign == ones()) & (exp == zeros()) & (mant == zeros())) @@ -114,7 +121,7 @@ function f_is_neg_zero_S x32 = { val f_is_pos_zero_S : bits(32) -> bool function f_is_pos_zero_S x32 = { - let (sign, exp, mant) = fsplit_S (x32); + let (sign, exp, mant) = fstruct_S (x32); ( (sign == zeros()) & (exp == zeros()) & (mant == zeros())) @@ -122,7 +129,7 @@ function f_is_pos_zero_S x32 = { val f_is_pos_subnorm_S : bits(32) -> bool function f_is_pos_subnorm_S x32 = { - let (sign, exp, mant) = fsplit_S (x32); + let (sign, exp, mant) = fstruct_S (x32); ( (sign == zeros()) & (exp == zeros()) & (mant != zeros())) @@ -130,7 +137,7 @@ function f_is_pos_subnorm_S x32 = { val f_is_pos_norm_S : bits(32) -> bool function f_is_pos_norm_S x32 = { - let (sign, exp, mant) = fsplit_S (x32); + let (sign, exp, mant) = fstruct_S (x32); ( (sign == zeros()) & (exp != zeros()) & (exp != ones())) @@ -138,7 +145,7 @@ function f_is_pos_norm_S x32 = { val f_is_pos_inf_S : bits(32) -> bool function f_is_pos_inf_S x32 = { - let (sign, exp, mant) = fsplit_S (x32); + let (sign, exp, mant) = fstruct_S (x32); ( (sign == zeros()) & (exp == ones()) & (mant == zeros())) @@ -146,7 +153,7 @@ function f_is_pos_inf_S x32 = { val f_is_SNaN_S : bits(32) -> bool function f_is_SNaN_S x32 = { - let (sign, exp, mant) = fsplit_S (x32); + let (sign, exp, mant) = fstruct_S (x32); ( (exp == ones()) & (mant [22] == bitzero) & (mant != zeros())) @@ -154,7 +161,7 @@ function f_is_SNaN_S x32 = { val f_is_QNaN_S : bits(32) -> bool function f_is_QNaN_S x32 = { - let (sign, exp, mant) = fsplit_S (x32); + let (sign, exp, mant) = fstruct_S (x32); ( (exp == ones()) & (mant [22] == bitone)) } @@ -162,7 +169,7 @@ function f_is_QNaN_S x32 = { /* Either QNaN or SNan */ val f_is_NaN_S : bits(32) -> bool function f_is_NaN_S x32 = { - let (sign, exp, mant) = fsplit_S (x32); + let (sign, exp, mant) = fstruct_S (x32); ( (exp == ones()) & (mant != zeros())) } @@ -172,15 +179,15 @@ function f_is_NaN_S x32 = { val negate_S : bits(32) -> bits(32) function negate_S (x32) = { - let (sign, exp, mant) = fsplit_S (x32); + let (sign, exp, mant) = fstruct_S (x32); let new_sign = if (sign == 0b0) then 0b1 else 0b0; - fmake_S (new_sign, exp, mant) + fstruct_S ((new_sign, exp, mant)) } val feq_quiet_S : (bits(32), bits (32)) -> (bool, bits(5)) function feq_quiet_S (v1, v2) = { - let (s1, e1, m1) = fsplit_S (v1); - let (s2, e2, m2) = fsplit_S (v2); + let (s1, e1, m1) = fstruct_S (v1); + let (s2, e2, m2) = fstruct_S (v2); let v1Is0 = f_is_neg_zero_S(v1) | f_is_pos_zero_S(v1); let v2Is0 = f_is_neg_zero_S(v2) | f_is_pos_zero_S(v2); @@ -196,8 +203,8 @@ function feq_quiet_S (v1, v2) = { val flt_S : (bits(32), bits (32), bool) -> (bool, bits(5)) function flt_S (v1, v2, is_quiet) = { - let (s1, e1, m1) = fsplit_S (v1); - let (s2, e2, m2) = fsplit_S (v2); + let (s1, e1, m1) = fstruct_S (v1); + let (s2, e2, m2) = fstruct_S (v2); let result : bool = if (s1 == 0b0) & (s2 == 0b0) then @@ -227,8 +234,8 @@ function flt_S (v1, v2, is_quiet) = { val fle_S : (bits(32), bits (32), bool) -> (bool, bits(5)) function fle_S (v1, v2, is_quiet) = { - let (s1, e1, m1) = fsplit_S (v1); - let (s2, e2, m2) = fsplit_S (v2); + let (s1, e1, m1) = fstruct_S (v1); + let (s2, e2, m2) = fstruct_S (v2); let v1Is0 = f_is_neg_zero_S(v1) | f_is_pos_zero_S(v1); let v2Is0 = f_is_neg_zero_S(v2) | f_is_pos_zero_S(v2); @@ -850,9 +857,9 @@ mapping clause encdec = F_BIN_TYPE_S(rs2, rs1, rd, FLE_S) if hav function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FSGNJ_S)) = { let rs1_val_S = F_or_X_S(rs1); let rs2_val_S = F_or_X_S(rs2); - let (s1, e1, m1) = fsplit_S (rs1_val_S); - let (s2, e2, m2) = fsplit_S (rs2_val_S); - let rd_val_S = fmake_S (s2, e1, m1); + let (s1, e1, m1) = fstruct_S (rs1_val_S); + let (s2, e2, m2) = fstruct_S (rs2_val_S); + let rd_val_S = fstruct_S ((s2, e1, m1)); F_or_X_S(rd) = rd_val_S; RETIRE_SUCCESS @@ -861,9 +868,9 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FSGNJ_S)) = { function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FSGNJN_S)) = { let rs1_val_S = F_or_X_S(rs1); let rs2_val_S = F_or_X_S(rs2); - let (s1, e1, m1) = fsplit_S (rs1_val_S); - let (s2, e2, m2) = fsplit_S (rs2_val_S); - let rd_val_S = fmake_S (0b1 ^ s2, e1, m1); + let (s1, e1, m1) = fstruct_S (rs1_val_S); + let (s2, e2, m2) = fstruct_S (rs2_val_S); + let rd_val_S = fstruct_S ((0b1 ^ s2, e1, m1)); F_or_X_S(rd) = rd_val_S; RETIRE_SUCCESS @@ -872,9 +879,9 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FSGNJN_S)) = { function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FSGNJX_S)) = { let rs1_val_S = F_or_X_S(rs1); let rs2_val_S = F_or_X_S(rs2); - let (s1, e1, m1) = fsplit_S (rs1_val_S); - let (s2, e2, m2) = fsplit_S (rs2_val_S); - let rd_val_S = fmake_S (s1 ^ s2, e1, m1); + let (s1, e1, m1) = fstruct_S (rs1_val_S); + let (s2, e2, m2) = fstruct_S (rs2_val_S); + let rd_val_S = fstruct_S ((s1 ^ s2, e1, m1)); F_or_X_S(rd) = rd_val_S; RETIRE_SUCCESS diff --git a/model/riscv_insts_zfa.sail b/model/riscv_insts_zfa.sail index 2b1f7c50f..751652c40 100644 --- a/model/riscv_insts_zfa.sail +++ b/model/riscv_insts_zfa.sail @@ -702,7 +702,7 @@ function clause execute(RISCV_FLTQ_D(rs2, rs1, rd)) = { */ val fcvtmod_helper : bits(64) -> (bits(5), bits(32)) function fcvtmod_helper(x64) = { - let (sign, exp, mant) = fsplit_D(x64); + let (sign, exp, mant) = fstruct_D(x64); /* Detect the non-normal cases */ let is_subnorm = exp == zeros() & mant != zeros(); diff --git a/model/riscv_insts_zfh.sail b/model/riscv_insts_zfh.sail index 5e55fb8a2..0eb9d0bbb 100644 --- a/model/riscv_insts_zfh.sail +++ b/model/riscv_insts_zfh.sail @@ -34,16 +34,24 @@ function fsplit_H (xf16) = (xf16[15..15], xf16[14..10], xf16[9..0]) val fmake_H : (bits(1), bits(5), bits(10)) -> bits(16) function fmake_H (sign, exp, mant) = sign @ exp @ mant +val fExtractor_H : bits(16) <-> (bits(1), bits(5), bits(10)) +function fExtractor_H_forwards(xf16) = fsplit_H(xf16) +function fExtractor_H_forwards_matches(xf16) = true +function fExtractor_H_backwards(sign, exp, mant) = fmake_H(sign, exp, mant) +function fExtractor_H_backwards_matches(sign, exp, mant) = true + +mapping fstruct_H : bits(16) <-> (bits(1), bits(5), bits(10)) = {fExtractor_H(sign, exp, mant) <-> (sign, exp, mant)} + val negate_H : bits(16) -> bits(16) function negate_H (xf16) = { - let (sign, exp, mant) = fsplit_H (xf16); + let (sign, exp, mant) = fstruct_H (xf16); let new_sign = if (sign == 0b0) then 0b1 else 0b0; - fmake_H (new_sign, exp, mant) + fstruct_H ((new_sign, exp, mant)) } val f_is_neg_inf_H : bits(16) -> bool function f_is_neg_inf_H xf16 = { - let (sign, exp, mant) = fsplit_H (xf16); + let (sign, exp, mant) = fstruct_H (xf16); ( (sign == 0b1) & (exp == ones()) & (mant == zeros())) @@ -51,7 +59,7 @@ function f_is_neg_inf_H xf16 = { val f_is_neg_norm_H : bits(16) -> bool function f_is_neg_norm_H xf16 = { - let (sign, exp, mant) = fsplit_H (xf16); + let (sign, exp, mant) = fstruct_H (xf16); ( (sign == 0b1) & (exp != zeros()) & (exp != ones())) @@ -59,7 +67,7 @@ function f_is_neg_norm_H xf16 = { val f_is_neg_subnorm_H : bits(16) -> bool function f_is_neg_subnorm_H xf16 = { - let (sign, exp, mant) = fsplit_H (xf16); + let (sign, exp, mant) = fstruct_H (xf16); ( (sign == 0b1) & (exp == zeros()) & (mant != zeros())) @@ -67,7 +75,7 @@ function f_is_neg_subnorm_H xf16 = { val f_is_pos_subnorm_H : bits(16) -> bool function f_is_pos_subnorm_H xf16 = { - let (sign, exp, mant) = fsplit_H (xf16); + let (sign, exp, mant) = fstruct_H (xf16); ( (sign == zeros()) & (exp == zeros()) & (mant != zeros())) @@ -75,7 +83,7 @@ function f_is_pos_subnorm_H xf16 = { val f_is_pos_norm_H : bits(16) -> bool function f_is_pos_norm_H xf16 = { - let (sign, exp, mant) = fsplit_H (xf16); + let (sign, exp, mant) = fstruct_H (xf16); ( (sign == zeros()) & (exp != zeros()) & (exp != ones())) @@ -83,7 +91,7 @@ function f_is_pos_norm_H xf16 = { val f_is_pos_inf_H : bits(16) -> bool function f_is_pos_inf_H xf16 = { - let (sign, exp, mant) = fsplit_H (xf16); + let (sign, exp, mant) = fstruct_H (xf16); ( (sign == zeros()) & (exp == ones()) & (mant == zeros())) @@ -91,7 +99,7 @@ function f_is_pos_inf_H xf16 = { val f_is_neg_zero_H : bits(16) -> bool function f_is_neg_zero_H xf16 = { - let (sign, exp, mant) = fsplit_H (xf16); + let (sign, exp, mant) = fstruct_H (xf16); ( (sign == ones()) & (exp == zeros()) & (mant == zeros())) @@ -99,7 +107,7 @@ function f_is_neg_zero_H xf16 = { val f_is_pos_zero_H : bits(16) -> bool function f_is_pos_zero_H xf16 = { - let (sign, exp, mant) = fsplit_H (xf16); + let (sign, exp, mant) = fstruct_H (xf16); ( (sign == zeros()) & (exp == zeros()) & (mant == zeros())) @@ -107,7 +115,7 @@ function f_is_pos_zero_H xf16 = { val f_is_SNaN_H : bits(16) -> bool function f_is_SNaN_H xf16 = { - let (sign, exp, mant) = fsplit_H (xf16); + let (sign, exp, mant) = fstruct_H (xf16); ( (exp == ones()) & (mant [9] == bitzero) & (mant != zeros())) @@ -115,7 +123,7 @@ function f_is_SNaN_H xf16 = { val f_is_QNaN_H : bits(16) -> bool function f_is_QNaN_H xf16 = { - let (sign, exp, mant) = fsplit_H (xf16); + let (sign, exp, mant) = fstruct_H (xf16); ( (exp == ones()) & (mant [9] == bitone)) } @@ -123,15 +131,15 @@ function f_is_QNaN_H xf16 = { /* Either QNaN or SNan */ val f_is_NaN_H : bits(16) -> bool function f_is_NaN_H xf16 = { - let (sign, exp, mant) = fsplit_H (xf16); + let (sign, exp, mant) = fstruct_H (xf16); ( (exp == ones()) & (mant != zeros())) } val fle_H : (bits(16), bits (16), bool) -> (bool, bits(5)) function fle_H (v1, v2, is_quiet) = { - let (s1, e1, m1) = fsplit_H (v1); - let (s2, e2, m2) = fsplit_H (v2); + let (s1, e1, m1) = fstruct_H (v1); + let (s2, e2, m2) = fstruct_H (v2); let v1Is0 = f_is_neg_zero_H(v1) | f_is_pos_zero_H(v1); let v2Is0 = f_is_neg_zero_H(v2) | f_is_pos_zero_H(v2); @@ -341,9 +349,9 @@ mapping clause encdec = F_BIN_TYPE_H(rs2, rs1, rd, FLE_H) if hav function clause execute (F_BIN_TYPE_H(rs2, rs1, rd, FSGNJ_H)) = { let rs1_val_H = F_or_X_H(rs1); let rs2_val_H = F_or_X_H(rs2); - let (s1, e1, m1) = fsplit_H (rs1_val_H); - let (s2, e2, m2) = fsplit_H (rs2_val_H); - let rd_val_H = fmake_H (s2, e1, m1); + let (s1, e1, m1) = fstruct_H (rs1_val_H); + let (s2, e2, m2) = fstruct_H (rs2_val_H); + let rd_val_H = fstruct_H ((s2, e1, m1)); F_or_X_H(rd) = rd_val_H; RETIRE_SUCCESS @@ -352,9 +360,9 @@ function clause execute (F_BIN_TYPE_H(rs2, rs1, rd, FSGNJ_H)) = { function clause execute (F_BIN_TYPE_H(rs2, rs1, rd, FSGNJN_H)) = { let rs1_val_H = F_or_X_H(rs1); let rs2_val_H = F_or_X_H(rs2); - let (s1, e1, m1) = fsplit_H (rs1_val_H); - let (s2, e2, m2) = fsplit_H (rs2_val_H); - let rd_val_H = fmake_H (0b1 ^ s2, e1, m1); + let (s1, e1, m1) = fstruct_H (rs1_val_H); + let (s2, e2, m2) = fstruct_H (rs2_val_H); + let rd_val_H = fstruct_H ((0b1 ^ s2, e1, m1)); F_or_X_H(rd) = rd_val_H; RETIRE_SUCCESS @@ -363,9 +371,9 @@ function clause execute (F_BIN_TYPE_H(rs2, rs1, rd, FSGNJN_H)) = { function clause execute (F_BIN_TYPE_H(rs2, rs1, rd, FSGNJX_H)) = { let rs1_val_H = F_or_X_H(rs1); let rs2_val_H = F_or_X_H(rs2); - let (s1, e1, m1) = fsplit_H (rs1_val_H); - let (s2, e2, m2) = fsplit_H (rs2_val_H); - let rd_val_H = fmake_H (s1 ^ s2, e1, m1); + let (s1, e1, m1) = fstruct_H (rs1_val_H); + let (s2, e2, m2) = fstruct_H (rs2_val_H); + let rd_val_H = fstruct_H ((s1 ^ s2, e1, m1)); F_or_X_H(rd) = rd_val_H; RETIRE_SUCCESS