From 38fc8ac5cf1a41d1f58e76c1528504606c9ff4be Mon Sep 17 00:00:00 2001 From: Tim Hutt Date: Thu, 4 Apr 2024 21:45:56 +0100 Subject: [PATCH] Use generic versions of some float utility functions Make `fsplit`/`fmake`, `f_is_...` and `f_negate` generic over the float size. The vector code actually already used functions like this. This reduces a lot of copy/pasted code and will allow even more of the code to be deduplicated later. --- Makefile | 2 +- model/riscv_float.sail | 111 ++++++++++++++++ model/riscv_insts_dext.sail | 207 ++++++++--------------------- model/riscv_insts_fext.sail | 208 ++++++++---------------------- model/riscv_insts_vext_utils.sail | 118 +---------------- model/riscv_insts_zfa.sail | 62 ++++----- model/riscv_insts_zfh.sail | 184 ++++++-------------------- sail-riscv.install | 2 +- 8 files changed, 292 insertions(+), 602 deletions(-) create mode 100644 model/riscv_float.sail diff --git a/Makefile b/Makefile index deaad558f..c71278189 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_softfloat_interface.sail riscv_fdext_regs.sail riscv_fdext_control.sail +SAIL_SYS_SRCS += riscv_float.sail riscv_softfloat_interface.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 new file mode 100644 index 000000000..4f0468369 --- /dev/null +++ b/model/riscv_float.sail @@ -0,0 +1,111 @@ +// --------------------------------------------------------------------------- + +// Split a floating point bitvec up into its sign, exponent, mantissa parts. +val fsplit : forall 'n, 'n in {16, 32, 64}. + bits('n) -> ( + bits(1), + bits(if 'n == 16 then 5 else (if 'n == 32 then 8 else 11)), + bits(if 'n == 16 then 10 else (if 'n == 32 then 23 else 52)), + ) +function fsplit(x) = { + if 'n == 16 then (x[15..15], x[14..10], x[9..0]) + else if 'n == 32 then (x[31..31], x[30..23], x[22..0]) + else (x[63..63], x[62..52], x[51..0]) +} + +// Join sign, exponent, mantissa parts back into a single bit vector. +val fmake : forall 'e, 'e in {5, 8, 11}. + ( + bits(1), + bits('e), + bits(if 'e == 5 then 10 else (if 'e == 8 then 23 else 52)), + ) -> bits(if 'e == 5 then 16 else (if 'e == 8 then 32 else 64)) +function fmake(sign, exp, mant) = sign @ exp @ mant + +// --------------------------------------------------------------------------- +// Floating point property functions. + +// Bit vector type for floating points - restricted to f16, f32, f64. +type fbits = { 'n, 'n in {16, 32, 64}. bits('n) } + +function f_is_neg_inf(x : fbits) -> bool = { + let (sign, exp, mant) = fsplit(x); + ( (sign == 0b1) + & (exp == ones()) + & (mant == zeros())) +} + +function f_is_neg_norm(x : fbits) -> bool = { + let (sign, exp, mant) = fsplit(x); + ( (sign == 0b1) + & (exp != zeros()) + & (exp != ones())) +} + +function f_is_neg_subnorm(x : fbits) -> bool = { + let (sign, exp, mant) = fsplit(x); + ( (sign == 0b1) + & (exp == zeros()) + & (mant != zeros())) +} + +function f_is_neg_zero(x : fbits) -> bool = { + let (sign, exp, mant) = fsplit(x); + ( (sign == ones()) + & (exp == zeros()) + & (mant == zeros())) +} + +function f_is_pos_zero(x : fbits) -> bool = { + let (sign, exp, mant) = fsplit(x); + ( (sign == zeros()) + & (exp == zeros()) + & (mant == zeros())) +} + +function f_is_pos_subnorm(x : fbits) -> bool = { + let (sign, exp, mant) = fsplit(x); + ( (sign == zeros()) + & (exp == zeros()) + & (mant != zeros())) +} + +function f_is_pos_norm(x : fbits) -> bool = { + let (sign, exp, mant) = fsplit(x); + ( (sign == zeros()) + & (exp != zeros()) + & (exp != ones())) +} + +function f_is_pos_inf(x : fbits) -> bool = { + let (sign, exp, mant) = fsplit(x); + ( (sign == zeros()) + & (exp == ones()) + & (mant == zeros())) +} + +function f_is_SNaN(x : fbits) -> bool = { + let (sign, exp, 'mant) = fsplit(x); + ( (exp == ones()) + & (mant['mant - 1] == bitzero) + & (mant != zeros())) +} + +function f_is_QNaN(x : fbits) -> bool = { + let (sign, exp, 'mant) = fsplit(x); + ( (exp == ones()) + & (mant['mant - 1] == bitone)) +} + +// Either QNaN or SNan +function f_is_NaN(x : fbits) -> bool = { + let (sign, exp, mant) = fsplit(x); + ( (exp == ones()) + & (mant != zeros())) +} + +// --------------------------------------------------------------------------- + +// 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] diff --git a/model/riscv_insts_dext.sail b/model/riscv_insts_dext.sail index e568b1df2..81e29e7aa 100644 --- a/model/riscv_insts_dext.sail +++ b/model/riscv_insts_dext.sail @@ -29,127 +29,22 @@ /* In RISC-V, the D extension requires the F extension, so that */ /* should have been processed before this one. */ -/* **************************************************************** */ -/* 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 - -/* ---- 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); - ( (sign == 0b1) - & (exp == ones()) - & (mant == zeros())) -} - -val f_is_neg_norm_D : bits(64) -> bool -function f_is_neg_norm_D x64 = { - let (sign, exp, mant) = fsplit_D (x64); - ( (sign == 0b1) - & (exp != zeros()) - & (exp != ones())) -} - -val f_is_neg_subnorm_D : bits(64) -> bool -function f_is_neg_subnorm_D x64 = { - let (sign, exp, mant) = fsplit_D (x64); - ( (sign == 0b1) - & (exp == zeros()) - & (mant != zeros())) -} - -val f_is_neg_zero_D : bits(64) -> bool -function f_is_neg_zero_D x64 = { - let (sign, exp, mant) = fsplit_D (x64); - ( (sign == ones()) - & (exp == zeros()) - & (mant == zeros())) -} - -val f_is_pos_zero_D : bits(64) -> bool -function f_is_pos_zero_D x64 = { - let (sign, exp, mant) = fsplit_D (x64); - ( (sign == zeros()) - & (exp == zeros()) - & (mant == zeros())) -} - -val f_is_pos_subnorm_D : bits(64) -> bool -function f_is_pos_subnorm_D x64 = { - let (sign, exp, mant) = fsplit_D (x64); - ( (sign == zeros()) - & (exp == zeros()) - & (mant != zeros())) -} - -val f_is_pos_norm_D : bits(64) -> bool -function f_is_pos_norm_D x64 = { - let (sign, exp, mant) = fsplit_D (x64); - ( (sign == zeros()) - & (exp != zeros()) - & (exp != ones())) -} - -val f_is_pos_inf_D : bits(64) -> bool -function f_is_pos_inf_D x64 = { - let (sign, exp, mant) = fsplit_D (x64); - ( (sign == zeros()) - & (exp == ones()) - & (mant == zeros())) -} - -val f_is_SNaN_D : bits(64) -> bool -function f_is_SNaN_D x64 = { - let (sign, exp, mant) = fsplit_D (x64); - ( (exp == ones()) - & (mant [51] == bitzero) - & (mant != zeros())) -} - -val f_is_QNaN_D : bits(64) -> bool -function f_is_QNaN_D x64 = { - let (sign, exp, mant) = fsplit_D (x64); - ( (exp == ones()) - & (mant [51] == bitone)) -} - -/* 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); - ( (exp == ones()) - & (mant != zeros())) -} /* **************************************************************** */ /* Help functions used in the semantic functions */ -val negate_D : bits(64) -> bits(64) -function negate_D (x64) = { - let (sign, exp, mant) = fsplit_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) = fsplit (v1); + let (s2, e2, m2) = fsplit (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); + 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_D(v1) | f_is_SNaN_D(v2)) + let fflags = if (f_is_SNaN(v1) | f_is_SNaN(v2)) then nvFlag() else zeros(); @@ -158,8 +53,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) = fsplit (v1); + let (s2, e2, m2) = fsplit (v2); let result : bool = if (s1 == 0b0) & (s2 == 0b0) then @@ -176,11 +71,11 @@ function flt_D (v1, v2, is_quiet) = { else unsigned (e1) > unsigned (e2); let fflags = if is_quiet then - if (f_is_SNaN_D(v1) | f_is_SNaN_D(v2)) + if (f_is_SNaN(v1) | f_is_SNaN(v2)) then nvFlag() else zeros() else - if (f_is_NaN_D(v1) | f_is_NaN_D(v2)) + if (f_is_NaN(v1) | f_is_NaN(v2)) then nvFlag() else zeros(); @@ -189,11 +84,11 @@ 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) = fsplit (v1); + let (s2, e2, m2) = fsplit (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); + 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 @@ -210,11 +105,11 @@ function fle_D (v1, v2, is_quiet) = { else unsigned (e1) > unsigned (e2); let fflags = if is_quiet then - if (f_is_SNaN_D(v1) | f_is_SNaN_D(v2)) + if (f_is_SNaN(v1) | f_is_SNaN(v2)) then nvFlag() else zeros() else - if (f_is_NaN_D(v1) | f_is_NaN_D(v2)) + if (f_is_NaN(v1) | f_is_NaN(v2)) then nvFlag() else zeros(); @@ -283,9 +178,9 @@ function clause execute (F_MADD_TYPE_D(rs3, rs2, rs1, rm, rd, op)) = { let (fflags, rd_val_64b) : (bits(5), bits(64)) = match op { FMADD_D => riscv_f64MulAdd (rm_3b, rs1_val_64b, rs2_val_64b, rs3_val_64b), - FMSUB_D => riscv_f64MulAdd (rm_3b, rs1_val_64b, rs2_val_64b, negate_D (rs3_val_64b)), - FNMSUB_D => riscv_f64MulAdd (rm_3b, negate_D (rs1_val_64b), rs2_val_64b, rs3_val_64b), - FNMADD_D => riscv_f64MulAdd (rm_3b, negate_D (rs1_val_64b), rs2_val_64b, negate_D (rs3_val_64b)) + FMSUB_D => riscv_f64MulAdd (rm_3b, rs1_val_64b, rs2_val_64b, f_negate (rs3_val_64b)), + FNMSUB_D => riscv_f64MulAdd (rm_3b, f_negate (rs1_val_64b), rs2_val_64b, rs3_val_64b), + FNMADD_D => riscv_f64MulAdd (rm_3b, f_negate (rs1_val_64b), rs2_val_64b, f_negate (rs3_val_64b)) }; accrue_fflags(fflags); F_or_X_D(rd) = rd_val_64b; @@ -723,9 +618,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) = fsplit (rs1_val_D); + let (s2, e2, m2) = fsplit (rs2_val_D); + let rd_val_D = fmake (s2, e1, m1); F_or_X_D(rd) = rd_val_D; RETIRE_SUCCESS @@ -734,9 +629,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) = fsplit (rs1_val_D); + let (s2, e2, m2) = fsplit (rs2_val_D); + let rd_val_D = fmake (0b1 ^ s2, e1, m1); F_or_X_D(rd) = rd_val_D; RETIRE_SUCCESS @@ -745,9 +640,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) = fsplit (rs1_val_D); + let (s2, e2, m2) = fsplit (rs2_val_D); + let rd_val_D = fmake (s1 ^ s2, e1, m1); F_or_X_D(rd) = rd_val_D; RETIRE_SUCCESS @@ -760,13 +655,13 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FMIN_D)) = { let is_quiet = true; let (rs1_lt_rs2, fflags) = fle_D (rs1_val_D, rs2_val_D, is_quiet); - let rd_val_D = if (f_is_NaN_D(rs1_val_D) & f_is_NaN_D(rs2_val_D)) then canonical_NaN(64) - else if f_is_NaN_D(rs1_val_D) then rs2_val_D - else if f_is_NaN_D(rs2_val_D) then rs1_val_D - else if (f_is_neg_zero_D(rs1_val_D) & f_is_pos_zero_D(rs2_val_D)) then rs1_val_D - else if (f_is_neg_zero_D(rs2_val_D) & f_is_pos_zero_D(rs1_val_D)) then rs2_val_D - else if rs1_lt_rs2 then rs1_val_D - else /* (not rs1_lt_rs2) */ rs2_val_D; + 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 + else if f_is_NaN(rs2_val_D) then rs1_val_D + else if (f_is_neg_zero(rs1_val_D) & f_is_pos_zero(rs2_val_D)) then rs1_val_D + else if (f_is_neg_zero(rs2_val_D) & f_is_pos_zero(rs1_val_D)) then rs2_val_D + else if rs1_lt_rs2 then rs1_val_D + else /* (not rs1_lt_rs2) */ rs2_val_D; accrue_fflags(fflags); F_or_X_D(rd) = rd_val_D; @@ -780,13 +675,13 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FMAX_D)) = { let is_quiet = true; let (rs2_lt_rs1, fflags) = fle_D (rs2_val_D, rs1_val_D, is_quiet); - let rd_val_D = if (f_is_NaN_D(rs1_val_D) & f_is_NaN_D(rs2_val_D)) then canonical_NaN(64) - else if f_is_NaN_D(rs1_val_D) then rs2_val_D - else if f_is_NaN_D(rs2_val_D) then rs1_val_D - else if (f_is_neg_zero_D(rs1_val_D) & f_is_pos_zero_D(rs2_val_D)) then rs2_val_D - else if (f_is_neg_zero_D(rs2_val_D) & f_is_pos_zero_D(rs1_val_D)) then rs1_val_D - else if rs2_lt_rs1 then rs1_val_D - else /* (not rs2_lt_rs1) */ rs2_val_D; + 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 + else if f_is_NaN(rs2_val_D) then rs1_val_D + else if (f_is_neg_zero(rs1_val_D) & f_is_pos_zero(rs2_val_D)) then rs2_val_D + else if (f_is_neg_zero(rs2_val_D) & f_is_pos_zero(rs1_val_D)) then rs1_val_D + else if rs2_lt_rs1 then rs1_val_D + else /* (not rs2_lt_rs1) */ rs2_val_D; accrue_fflags(fflags); F_or_X_D(rd) = rd_val_D; @@ -914,16 +809,16 @@ function clause execute (F_UN_TYPE_D(rs1, rd, FCLASS_D)) = { let rs1_val_D = F_or_X_D(rs1); let rd_val_10b : bits (10) = - if f_is_neg_inf_D (rs1_val_D) then 0b_00_0000_0001 - else if f_is_neg_norm_D (rs1_val_D) then 0b_00_0000_0010 - else if f_is_neg_subnorm_D (rs1_val_D) then 0b_00_0000_0100 - else if f_is_neg_zero_D (rs1_val_D) then 0b_00_0000_1000 - else if f_is_pos_zero_D (rs1_val_D) then 0b_00_0001_0000 - else if f_is_pos_subnorm_D (rs1_val_D) then 0b_00_0010_0000 - else if f_is_pos_norm_D (rs1_val_D) then 0b_00_0100_0000 - else if f_is_pos_inf_D (rs1_val_D) then 0b_00_1000_0000 - else if f_is_SNaN_D (rs1_val_D) then 0b_01_0000_0000 - else if f_is_QNaN_D (rs1_val_D) then 0b_10_0000_0000 + if f_is_neg_inf (rs1_val_D) then 0b_00_0000_0001 + else if f_is_neg_norm (rs1_val_D) then 0b_00_0000_0010 + else if f_is_neg_subnorm (rs1_val_D) then 0b_00_0000_0100 + else if f_is_neg_zero (rs1_val_D) then 0b_00_0000_1000 + else if f_is_pos_zero (rs1_val_D) then 0b_00_0001_0000 + else if f_is_pos_subnorm (rs1_val_D) then 0b_00_0010_0000 + else if f_is_pos_norm (rs1_val_D) then 0b_00_0100_0000 + else if f_is_pos_inf (rs1_val_D) then 0b_00_1000_0000 + else if f_is_SNaN (rs1_val_D) then 0b_01_0000_0000 + else if f_is_QNaN (rs1_val_D) then 0b_10_0000_0000 else zeros(); X(rd) = zero_extend (rd_val_10b); diff --git a/model/riscv_insts_fext.sail b/model/riscv_insts_fext.sail index b23e2edf7..2e15fa033 100644 --- a/model/riscv_insts_fext.sail +++ b/model/riscv_insts_fext.sail @@ -65,126 +65,20 @@ function ofFlag() -> bits(5) = 0b_00100 function dzFlag() -> bits(5) = 0b_01000 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 - -/* ---- 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); - ( (sign == 0b1) - & (exp == ones()) - & (mant == zeros())) -} - -val f_is_neg_norm_S : bits(32) -> bool -function f_is_neg_norm_S x32 = { - let (sign, exp, mant) = fsplit_S (x32); - ( (sign == 0b1) - & (exp != zeros()) - & (exp != ones())) -} - -val f_is_neg_subnorm_S : bits(32) -> bool -function f_is_neg_subnorm_S x32 = { - let (sign, exp, mant) = fsplit_S (x32); - ( (sign == 0b1) - & (exp == zeros()) - & (mant != zeros())) -} - -val f_is_neg_zero_S : bits(32) -> bool -function f_is_neg_zero_S x32 = { - let (sign, exp, mant) = fsplit_S (x32); - ( (sign == ones()) - & (exp == zeros()) - & (mant == zeros())) -} - -val f_is_pos_zero_S : bits(32) -> bool -function f_is_pos_zero_S x32 = { - let (sign, exp, mant) = fsplit_S (x32); - ( (sign == zeros()) - & (exp == zeros()) - & (mant == zeros())) -} - -val f_is_pos_subnorm_S : bits(32) -> bool -function f_is_pos_subnorm_S x32 = { - let (sign, exp, mant) = fsplit_S (x32); - ( (sign == zeros()) - & (exp == zeros()) - & (mant != zeros())) -} - -val f_is_pos_norm_S : bits(32) -> bool -function f_is_pos_norm_S x32 = { - let (sign, exp, mant) = fsplit_S (x32); - ( (sign == zeros()) - & (exp != zeros()) - & (exp != ones())) -} - -val f_is_pos_inf_S : bits(32) -> bool -function f_is_pos_inf_S x32 = { - let (sign, exp, mant) = fsplit_S (x32); - ( (sign == zeros()) - & (exp == ones()) - & (mant == zeros())) -} - -val f_is_SNaN_S : bits(32) -> bool -function f_is_SNaN_S x32 = { - let (sign, exp, mant) = fsplit_S (x32); - ( (exp == ones()) - & (mant [22] == bitzero) - & (mant != zeros())) -} - -val f_is_QNaN_S : bits(32) -> bool -function f_is_QNaN_S x32 = { - let (sign, exp, mant) = fsplit_S (x32); - ( (exp == ones()) - & (mant [22] == bitone)) -} - -/* 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); - ( (exp == ones()) - & (mant != zeros())) -} - /* **************************************************************** */ /* Help functions used in the semantic functions */ -val negate_S : bits(32) -> bits(32) -function negate_S (x32) = { - let (sign, exp, mant) = fsplit_S (x32); - let new_sign = if (sign == 0b0) then 0b1 else 0b0; - fmake_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) = fsplit (v1); + let (s2, e2, m2) = fsplit (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); + 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_S(v1) | f_is_SNaN_S(v2)) + let fflags = if (f_is_SNaN(v1) | f_is_SNaN(v2)) then nvFlag() else zeros(); @@ -193,8 +87,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) = fsplit (v1); + let (s2, e2, m2) = fsplit (v2); let result : bool = if (s1 == 0b0) & (s2 == 0b0) then @@ -211,11 +105,11 @@ function flt_S (v1, v2, is_quiet) = { else unsigned (e1) > unsigned (e2); let fflags = if is_quiet then - if (f_is_SNaN_S(v1) | f_is_SNaN_S(v2)) + if (f_is_SNaN(v1) | f_is_SNaN(v2)) then nvFlag() else zeros() else - if (f_is_NaN_S(v1) | f_is_NaN_S(v2)) + if (f_is_NaN(v1) | f_is_NaN(v2)) then nvFlag() else zeros(); @@ -224,11 +118,11 @@ 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) = fsplit (v1); + let (s2, e2, m2) = fsplit (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); + 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 @@ -245,11 +139,11 @@ function fle_S (v1, v2, is_quiet) = { else unsigned (e1) > unsigned (e2); let fflags = if is_quiet then - if (f_is_SNaN_S(v1) | f_is_SNaN_S(v2)) + if (f_is_SNaN(v1) | f_is_SNaN(v2)) then nvFlag() else zeros() else - if (f_is_NaN_S(v1) | f_is_NaN_S(v2)) + if (f_is_NaN(v1) | f_is_NaN(v2)) then nvFlag() else zeros(); @@ -460,9 +354,9 @@ function clause execute (F_MADD_TYPE_S(rs3, rs2, rs1, rm, rd, op)) = { let (fflags, rd_val_32b) : (bits(5), bits(32)) = match op { FMADD_S => riscv_f32MulAdd (rm_3b, rs1_val_32b, rs2_val_32b, rs3_val_32b), - FMSUB_S => riscv_f32MulAdd (rm_3b, rs1_val_32b, rs2_val_32b, negate_S (rs3_val_32b)), - FNMSUB_S => riscv_f32MulAdd (rm_3b, negate_S (rs1_val_32b), rs2_val_32b, rs3_val_32b), - FNMADD_S => riscv_f32MulAdd (rm_3b, negate_S (rs1_val_32b), rs2_val_32b, negate_S (rs3_val_32b)) + FMSUB_S => riscv_f32MulAdd (rm_3b, rs1_val_32b, rs2_val_32b, f_negate (rs3_val_32b)), + FNMSUB_S => riscv_f32MulAdd (rm_3b, f_negate (rs1_val_32b), rs2_val_32b, rs3_val_32b), + FNMADD_S => riscv_f32MulAdd (rm_3b, f_negate (rs1_val_32b), rs2_val_32b, f_negate (rs3_val_32b)) }; accrue_fflags(fflags); F_or_X_S(rd) = rd_val_32b; @@ -847,9 +741,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) = fsplit (rs1_val_S); + let (s2, e2, m2) = fsplit (rs2_val_S); + let rd_val_S = fmake (s2, e1, m1); F_or_X_S(rd) = rd_val_S; RETIRE_SUCCESS @@ -858,9 +752,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) = fsplit (rs1_val_S); + let (s2, e2, m2) = fsplit (rs2_val_S); + let rd_val_S = fmake (0b1 ^ s2, e1, m1); F_or_X_S(rd) = rd_val_S; RETIRE_SUCCESS @@ -869,9 +763,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) = fsplit (rs1_val_S); + let (s2, e2, m2) = fsplit (rs2_val_S); + let rd_val_S = fmake (s1 ^ s2, e1, m1); F_or_X_S(rd) = rd_val_S; RETIRE_SUCCESS @@ -884,13 +778,13 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FMIN_S)) = { let is_quiet = true; let (rs1_lt_rs2, fflags) = fle_S (rs1_val_S, rs2_val_S, is_quiet); - let rd_val_S = if (f_is_NaN_S(rs1_val_S) & f_is_NaN_S(rs2_val_S)) then canonical_NaN(32) - else if f_is_NaN_S(rs1_val_S) then rs2_val_S - else if f_is_NaN_S(rs2_val_S) then rs1_val_S - else if (f_is_neg_zero_S(rs1_val_S) & f_is_pos_zero_S(rs2_val_S)) then rs1_val_S - else if (f_is_neg_zero_S(rs2_val_S) & f_is_pos_zero_S(rs1_val_S)) then rs2_val_S - else if rs1_lt_rs2 then rs1_val_S - else /* (not rs1_lt_rs2) */ rs2_val_S; + 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 + else if f_is_NaN(rs2_val_S) then rs1_val_S + else if (f_is_neg_zero(rs1_val_S) & f_is_pos_zero(rs2_val_S)) then rs1_val_S + else if (f_is_neg_zero(rs2_val_S) & f_is_pos_zero(rs1_val_S)) then rs2_val_S + else if rs1_lt_rs2 then rs1_val_S + else /* (not rs1_lt_rs2) */ rs2_val_S; accrue_fflags(fflags); F_or_X_S(rd) = rd_val_S; @@ -904,13 +798,13 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FMAX_S)) = { let is_quiet = true; let (rs2_lt_rs1, fflags) = fle_S (rs2_val_S, rs1_val_S, is_quiet); - let rd_val_S = if (f_is_NaN_S(rs1_val_S) & f_is_NaN_S(rs2_val_S)) then canonical_NaN(32) - else if f_is_NaN_S(rs1_val_S) then rs2_val_S - else if f_is_NaN_S(rs2_val_S) then rs1_val_S - else if (f_is_neg_zero_S(rs1_val_S) & f_is_pos_zero_S(rs2_val_S)) then rs2_val_S - else if (f_is_neg_zero_S(rs2_val_S) & f_is_pos_zero_S(rs1_val_S)) then rs1_val_S - else if rs2_lt_rs1 then rs1_val_S - else /* (not rs2_lt_rs1) */ rs2_val_S; + 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 + else if f_is_NaN(rs2_val_S) then rs1_val_S + else if (f_is_neg_zero(rs1_val_S) & f_is_pos_zero(rs2_val_S)) then rs2_val_S + else if (f_is_neg_zero(rs2_val_S) & f_is_pos_zero(rs1_val_S)) then rs1_val_S + else if rs2_lt_rs1 then rs1_val_S + else /* (not rs2_lt_rs1) */ rs2_val_S; accrue_fflags(fflags); F_or_X_S(rd) = rd_val_S; @@ -1036,16 +930,16 @@ function clause execute (F_UN_TYPE_S(rs1, rd, FCLASS_S)) = { let rs1_val_S = F_or_X_S(rs1); let rd_val_10b : bits (10) = - if f_is_neg_inf_S (rs1_val_S) then 0b_00_0000_0001 - else if f_is_neg_norm_S (rs1_val_S) then 0b_00_0000_0010 - else if f_is_neg_subnorm_S (rs1_val_S) then 0b_00_0000_0100 - else if f_is_neg_zero_S (rs1_val_S) then 0b_00_0000_1000 - else if f_is_pos_zero_S (rs1_val_S) then 0b_00_0001_0000 - else if f_is_pos_subnorm_S (rs1_val_S) then 0b_00_0010_0000 - else if f_is_pos_norm_S (rs1_val_S) then 0b_00_0100_0000 - else if f_is_pos_inf_S (rs1_val_S) then 0b_00_1000_0000 - else if f_is_SNaN_S (rs1_val_S) then 0b_01_0000_0000 - else if f_is_QNaN_S (rs1_val_S) then 0b_10_0000_0000 + if f_is_neg_inf (rs1_val_S) then 0b_00_0000_0001 + else if f_is_neg_norm (rs1_val_S) then 0b_00_0000_0010 + else if f_is_neg_subnorm (rs1_val_S) then 0b_00_0000_0100 + else if f_is_neg_zero (rs1_val_S) then 0b_00_0000_1000 + else if f_is_pos_zero (rs1_val_S) then 0b_00_0001_0000 + else if f_is_pos_subnorm (rs1_val_S) then 0b_00_0010_0000 + else if f_is_pos_norm (rs1_val_S) then 0b_00_0100_0000 + else if f_is_pos_inf (rs1_val_S) then 0b_00_1000_0000 + else if f_is_SNaN (rs1_val_S) then 0b_01_0000_0000 + else if f_is_QNaN (rs1_val_S) then 0b_10_0000_0000 else zeros(); X(rd) = zero_extend (rd_val_10b); diff --git a/model/riscv_insts_vext_utils.sail b/model/riscv_insts_vext_utils.sail index 4c7032b9f..12e29aa38 100755 --- a/model/riscv_insts_vext_utils.sail +++ b/model/riscv_insts_vext_utils.sail @@ -437,106 +437,6 @@ function read_vreg_seg(num_elem, SEW, LMUL_pow, nf, vrid) = { result } -/* Floating point classification functions */ -val f_is_neg_inf : forall 'm, 'm in {16, 32, 64}. bits('m) -> bool -function f_is_neg_inf(xf) = { - match 'm { - 16 => f_is_neg_inf_H(xf), - 32 => f_is_neg_inf_S(xf), - 64 => f_is_neg_inf_D(xf) - } -} - -val f_is_neg_norm : forall 'm, 'm in {16, 32, 64}. bits('m) -> bool -function f_is_neg_norm(xf) = { - match 'm { - 16 => f_is_neg_norm_H(xf), - 32 => f_is_neg_norm_S(xf), - 64 => f_is_neg_norm_D(xf) - } -} - -val f_is_neg_subnorm : forall 'm, 'm in {16, 32, 64}. bits('m) -> bool -function f_is_neg_subnorm(xf) = { - match 'm { - 16 => f_is_neg_subnorm_H(xf), - 32 => f_is_neg_subnorm_S(xf), - 64 => f_is_neg_subnorm_D(xf) - } -} - -val f_is_neg_zero : forall 'm, 'm in {16, 32, 64}. bits('m) -> bool -function f_is_neg_zero(xf) = { - match 'm { - 16 => f_is_neg_zero_H(xf), - 32 => f_is_neg_zero_S(xf), - 64 => f_is_neg_zero_D(xf) - } -} - -val f_is_pos_zero : forall 'm, 'm in {16, 32, 64}. bits('m) -> bool -function f_is_pos_zero(xf) = { - match 'm { - 16 => f_is_pos_zero_H(xf), - 32 => f_is_pos_zero_S(xf), - 64 => f_is_pos_zero_D(xf) - } -} - -val f_is_pos_subnorm : forall 'm, 'm in {16, 32, 64}. bits('m) -> bool -function f_is_pos_subnorm(xf) = { - match 'm { - 16 => f_is_pos_subnorm_H(xf), - 32 => f_is_pos_subnorm_S(xf), - 64 => f_is_pos_subnorm_D(xf) - } -} - -val f_is_pos_norm : forall 'm, 'm in {16, 32, 64}. bits('m) -> bool -function f_is_pos_norm(xf) = { - match 'm { - 16 => f_is_pos_norm_H(xf), - 32 => f_is_pos_norm_S(xf), - 64 => f_is_pos_norm_D(xf) - } -} - -val f_is_pos_inf : forall 'm, 'm in {16, 32, 64}. bits('m) -> bool -function f_is_pos_inf(xf) = { - match 'm { - 16 => f_is_pos_inf_H(xf), - 32 => f_is_pos_inf_S(xf), - 64 => f_is_pos_inf_D(xf) - } -} - -val f_is_SNaN : forall 'm, 'm in {16, 32, 64}. bits('m) -> bool -function f_is_SNaN(xf) = { - match 'm { - 16 => f_is_SNaN_H(xf), - 32 => f_is_SNaN_S(xf), - 64 => f_is_SNaN_D(xf) - } -} - -val f_is_QNaN : forall 'm, 'm in {16, 32, 64}. bits('m) -> bool -function f_is_QNaN(xf) = { - match 'm { - 16 => f_is_QNaN_H(xf), - 32 => f_is_QNaN_S(xf), - 64 => f_is_QNaN_D(xf) - } -} - -val f_is_NaN : forall 'm, 'm in {16, 32, 64}. bits('m) -> bool -function f_is_NaN(xf) = { - match 'm { - 16 => f_is_NaN_H(xf), - 32 => f_is_NaN_S(xf), - 64 => f_is_NaN_D(xf) - } -} - /* Scalar register shaping for floating point operations */ val get_scalar_fp : forall 'n, 'n in {16, 32, 64}. (regidx, int('n)) -> bits('n) function get_scalar_fp(rs1, SEW) = { @@ -604,16 +504,6 @@ function signed_saturation(len, elem) = { val get_fp_rounding_mode : unit -> rounding_mode function get_fp_rounding_mode() = encdec_rounding_mode(fcsr[FRM]) -/* Negate a floating point number */ -val negate_fp : forall 'm, 'm in {16, 32, 64}. bits('m) -> bits('m) -function negate_fp(xf) = { - match 'm { - 16 => negate_H(xf), - 32 => negate_S(xf), - 64 => negate_D(xf) - } -} - /* Floating point functions using softfloat interface */ val fp_add: forall 'm, 'm in {16, 32, 64}. (bits(3), bits('m), bits('m)) -> bits('m) function fp_add(rm_3b, op1, op2) = { @@ -767,7 +657,7 @@ function fp_muladd(rm_3b, op1, op2, opadd) = { val fp_nmuladd : forall 'm, 'm in {16, 32, 64}. (bits(3), bits('m), bits('m), bits('m)) -> bits('m) function fp_nmuladd(rm_3b, op1, op2, opadd) = { - let op1 = negate_fp(op1); + let op1 = f_negate(op1); let (fflags, result_val) : (bits_fflags, bits('m)) = match 'm { 16 => riscv_f16MulAdd(rm_3b, op1, op2, opadd), 32 => riscv_f32MulAdd(rm_3b, op1, op2, opadd), @@ -779,7 +669,7 @@ function fp_nmuladd(rm_3b, op1, op2, opadd) = { val fp_mulsub : forall 'm, 'm in {16, 32, 64}. (bits(3), bits('m), bits('m), bits('m)) -> bits('m) function fp_mulsub(rm_3b, op1, op2, opsub) = { - let opsub = negate_fp(opsub); + let opsub = f_negate(opsub); let (fflags, result_val) : (bits_fflags, bits('m)) = match 'm { 16 => riscv_f16MulAdd(rm_3b, op1, op2, opsub), 32 => riscv_f32MulAdd(rm_3b, op1, op2, opsub), @@ -791,8 +681,8 @@ function fp_mulsub(rm_3b, op1, op2, opsub) = { val fp_nmulsub : forall 'm, 'm in {16, 32, 64}. (bits(3), bits('m), bits('m), bits('m)) -> bits('m) function fp_nmulsub(rm_3b, op1, op2, opsub) = { - let opsub = negate_fp(opsub); - let op1 = negate_fp(op1); + let opsub = f_negate(opsub); + let op1 = f_negate(op1); let (fflags, result_val) : (bits_fflags, bits('m)) = match 'm { 16 => riscv_f16MulAdd(rm_3b, op1, op2, opsub), 32 => riscv_f32MulAdd(rm_3b, op1, op2, opsub), diff --git a/model/riscv_insts_zfa.sail b/model/riscv_insts_zfa.sail index 68b396cc4..0b6e3b89e 100644 --- a/model/riscv_insts_zfa.sail +++ b/model/riscv_insts_zfa.sail @@ -172,11 +172,11 @@ function clause execute (RISCV_FMINM_H(rs2, rs1, rd)) = { let is_quiet = true; let (rs1_lt_rs2, fflags) = fle_H (rs1_val_H, rs2_val_H, is_quiet); - let rd_val_H = if (f_is_NaN_H(rs1_val_H) | f_is_NaN_H(rs2_val_H)) then canonical_NaN(16) - else if (f_is_neg_zero_H(rs1_val_H) & f_is_pos_zero_H(rs2_val_H)) then rs1_val_H - else if (f_is_neg_zero_H(rs2_val_H) & f_is_pos_zero_H(rs1_val_H)) then rs2_val_H - else if rs1_lt_rs2 then rs1_val_H - else /* (not rs1_lt_rs2) */ rs2_val_H; + 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 + else if (f_is_neg_zero(rs2_val_H) & f_is_pos_zero(rs1_val_H)) then rs2_val_H + else if rs1_lt_rs2 then rs1_val_H + else /* (not rs1_lt_rs2) */ rs2_val_H; accrue_fflags(fflags); F_box(rd) = rd_val_H; @@ -202,11 +202,11 @@ function clause execute (RISCV_FMAXM_H(rs2, rs1, rd)) = { let is_quiet = true; let (rs2_lt_rs1, fflags) = fle_H (rs2_val_H, rs1_val_H, is_quiet); - let rd_val_H = if (f_is_NaN_H(rs1_val_H) | f_is_NaN_H(rs2_val_H)) then canonical_NaN(16) - else if (f_is_neg_zero_H(rs1_val_H) & f_is_pos_zero_H(rs2_val_H)) then rs2_val_H - else if (f_is_neg_zero_H(rs2_val_H) & f_is_pos_zero_H(rs1_val_H)) then rs1_val_H - else if rs2_lt_rs1 then rs1_val_H - else /* (not rs2_lt_rs1) */ rs2_val_H; + 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 + else if (f_is_neg_zero(rs2_val_H) & f_is_pos_zero(rs1_val_H)) then rs1_val_H + else if rs2_lt_rs1 then rs1_val_H + else /* (not rs2_lt_rs1) */ rs2_val_H; accrue_fflags(fflags); F_box(rd) = rd_val_H; @@ -232,11 +232,11 @@ function clause execute (RISCV_FMINM_S(rs2, rs1, rd)) = { let is_quiet = true; let (rs1_lt_rs2, fflags) = fle_S (rs1_val_S, rs2_val_S, is_quiet); - let rd_val_S = if (f_is_NaN_S(rs1_val_S) | f_is_NaN_S(rs2_val_S)) then canonical_NaN(32) - else if (f_is_neg_zero_S(rs1_val_S) & f_is_pos_zero_S(rs2_val_S)) then rs1_val_S - else if (f_is_neg_zero_S(rs2_val_S) & f_is_pos_zero_S(rs1_val_S)) then rs2_val_S - else if rs1_lt_rs2 then rs1_val_S - else /* (not rs1_lt_rs2) */ rs2_val_S; + 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 + else if (f_is_neg_zero(rs2_val_S) & f_is_pos_zero(rs1_val_S)) then rs2_val_S + else if rs1_lt_rs2 then rs1_val_S + else /* (not rs1_lt_rs2) */ rs2_val_S; accrue_fflags(fflags); F_box(rd) = rd_val_S; @@ -262,11 +262,11 @@ function clause execute (RISCV_FMAXM_S(rs2, rs1, rd)) = { let is_quiet = true; let (rs2_lt_rs1, fflags) = fle_S (rs2_val_S, rs1_val_S, is_quiet); - let rd_val_S = if (f_is_NaN_S(rs1_val_S) | f_is_NaN_S(rs2_val_S)) then canonical_NaN(32) - else if (f_is_neg_zero_S(rs1_val_S) & f_is_pos_zero_S(rs2_val_S)) then rs2_val_S - else if (f_is_neg_zero_S(rs2_val_S) & f_is_pos_zero_S(rs1_val_S)) then rs1_val_S - else if rs2_lt_rs1 then rs1_val_S - else /* (not rs2_lt_rs1) */ rs2_val_S; + 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 + else if (f_is_neg_zero(rs2_val_S) & f_is_pos_zero(rs1_val_S)) then rs1_val_S + else if rs2_lt_rs1 then rs1_val_S + else /* (not rs2_lt_rs1) */ rs2_val_S; accrue_fflags(fflags); F_box(rd) = rd_val_S; @@ -292,11 +292,11 @@ function clause execute (RISCV_FMINM_D(rs2, rs1, rd)) = { let is_quiet = true; let (rs1_lt_rs2, fflags) = fle_D (rs1_val_D, rs2_val_D, is_quiet); - let rd_val_D = if (f_is_NaN_D(rs1_val_D) | f_is_NaN_D(rs2_val_D)) then canonical_NaN(64) - else if (f_is_neg_zero_D(rs1_val_D) & f_is_pos_zero_D(rs2_val_D)) then rs1_val_D - else if (f_is_neg_zero_D(rs2_val_D) & f_is_pos_zero_D(rs1_val_D)) then rs2_val_D - else if rs1_lt_rs2 then rs1_val_D - else rs2_val_D; + 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 + else if (f_is_neg_zero(rs2_val_D) & f_is_pos_zero(rs1_val_D)) then rs2_val_D + else if rs1_lt_rs2 then rs1_val_D + else rs2_val_D; accrue_fflags(fflags); F_box(rd) = rd_val_D; @@ -322,11 +322,11 @@ function clause execute (RISCV_FMAXM_D(rs2, rs1, rd)) = { let is_quiet = true; let (rs2_lt_rs1, fflags) = fle_D (rs2_val_D, rs1_val_D, is_quiet); - let rd_val_D = if (f_is_NaN_D(rs1_val_D) | f_is_NaN_D(rs2_val_D)) then canonical_NaN(64) - else if (f_is_neg_zero_D(rs1_val_D) & f_is_pos_zero_D(rs2_val_D)) then rs2_val_D - else if (f_is_neg_zero_D(rs2_val_D) & f_is_pos_zero_D(rs1_val_D)) then rs1_val_D - else if rs2_lt_rs1 then rs1_val_D - else rs2_val_D; + 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 + else if (f_is_neg_zero(rs2_val_D) & f_is_pos_zero(rs1_val_D)) then rs1_val_D + else if rs2_lt_rs1 then rs1_val_D + else rs2_val_D; accrue_fflags(fflags); F_box(rd) = rd_val_D; @@ -699,7 +699,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) = fsplit(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 12f9e4fa7..029e1e13c 100644 --- a/model/riscv_insts_zfh.sail +++ b/model/riscv_insts_zfh.sail @@ -25,113 +25,13 @@ /* **************************************************************** */ -val fsplit_H : bits(16) -> (bits(1), bits(5), bits(10)) -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 negate_H : bits(16) -> bits(16) -function negate_H (xf16) = { - let (sign, exp, mant) = fsplit_H (xf16); - let new_sign = if (sign == 0b0) then 0b1 else 0b0; - fmake_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); - ( (sign == 0b1) - & (exp == ones()) - & (mant == zeros())) -} - -val f_is_neg_norm_H : bits(16) -> bool -function f_is_neg_norm_H xf16 = { - let (sign, exp, mant) = fsplit_H (xf16); - ( (sign == 0b1) - & (exp != zeros()) - & (exp != ones())) -} - -val f_is_neg_subnorm_H : bits(16) -> bool -function f_is_neg_subnorm_H xf16 = { - let (sign, exp, mant) = fsplit_H (xf16); - ( (sign == 0b1) - & (exp == zeros()) - & (mant != zeros())) -} - -val f_is_pos_subnorm_H : bits(16) -> bool -function f_is_pos_subnorm_H xf16 = { - let (sign, exp, mant) = fsplit_H (xf16); - ( (sign == zeros()) - & (exp == zeros()) - & (mant != zeros())) -} - -val f_is_pos_norm_H : bits(16) -> bool -function f_is_pos_norm_H xf16 = { - let (sign, exp, mant) = fsplit_H (xf16); - ( (sign == zeros()) - & (exp != zeros()) - & (exp != ones())) -} - -val f_is_pos_inf_H : bits(16) -> bool -function f_is_pos_inf_H xf16 = { - let (sign, exp, mant) = fsplit_H (xf16); - ( (sign == zeros()) - & (exp == ones()) - & (mant == zeros())) -} - -val f_is_neg_zero_H : bits(16) -> bool -function f_is_neg_zero_H xf16 = { - let (sign, exp, mant) = fsplit_H (xf16); - ( (sign == ones()) - & (exp == zeros()) - & (mant == zeros())) -} - -val f_is_pos_zero_H : bits(16) -> bool -function f_is_pos_zero_H xf16 = { - let (sign, exp, mant) = fsplit_H (xf16); - ( (sign == zeros()) - & (exp == zeros()) - & (mant == zeros())) -} - -val f_is_SNaN_H : bits(16) -> bool -function f_is_SNaN_H xf16 = { - let (sign, exp, mant) = fsplit_H (xf16); - ( (exp == ones()) - & (mant [9] == bitzero) - & (mant != zeros())) -} - -val f_is_QNaN_H : bits(16) -> bool -function f_is_QNaN_H xf16 = { - let (sign, exp, mant) = fsplit_H (xf16); - ( (exp == ones()) - & (mant [9] == bitone)) -} - -/* 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); - ( (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) = fsplit (v1); + let (s2, e2, m2) = fsplit (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); + 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 @@ -148,11 +48,11 @@ function fle_H (v1, v2, is_quiet) = { else unsigned (e1) > unsigned (e2); let fflags = if is_quiet then - if (f_is_SNaN_H(v1) | f_is_SNaN_H(v2)) + if (f_is_SNaN(v1) | f_is_SNaN(v2)) then nvFlag() else zeros() else - if (f_is_NaN_H(v1) | f_is_NaN_H(v2)) + if (f_is_NaN(v1) | f_is_NaN(v2)) then nvFlag() else zeros(); @@ -272,9 +172,9 @@ function clause execute (F_MADD_TYPE_H(rs3, rs2, rs1, rm, rd, op)) = { let (fflags, rd_val_16b) : (bits(5), bits(16)) = match op { FMADD_H => riscv_f16MulAdd (rm_3b, rs1_val_16b, rs2_val_16b, rs3_val_16b), - FMSUB_H => riscv_f16MulAdd (rm_3b, rs1_val_16b, rs2_val_16b, negate_H (rs3_val_16b)), - FNMSUB_H => riscv_f16MulAdd (rm_3b, negate_H (rs1_val_16b), rs2_val_16b, rs3_val_16b), - FNMADD_H => riscv_f16MulAdd (rm_3b, negate_H (rs1_val_16b), rs2_val_16b, negate_H (rs3_val_16b)) + FMSUB_H => riscv_f16MulAdd (rm_3b, rs1_val_16b, rs2_val_16b, f_negate (rs3_val_16b)), + FNMSUB_H => riscv_f16MulAdd (rm_3b, f_negate (rs1_val_16b), rs2_val_16b, rs3_val_16b), + FNMADD_H => riscv_f16MulAdd (rm_3b, f_negate (rs1_val_16b), rs2_val_16b, f_negate (rs3_val_16b)) }; accrue_fflags(fflags); F_or_X_H(rd) = rd_val_16b; @@ -338,9 +238,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) = fsplit (rs1_val_H); + let (s2, e2, m2) = fsplit (rs2_val_H); + let rd_val_H = fmake (s2, e1, m1); F_or_X_H(rd) = rd_val_H; RETIRE_SUCCESS @@ -349,9 +249,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) = fsplit (rs1_val_H); + let (s2, e2, m2) = fsplit (rs2_val_H); + let rd_val_H = fmake (0b1 ^ s2, e1, m1); F_or_X_H(rd) = rd_val_H; RETIRE_SUCCESS @@ -360,9 +260,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) = fsplit (rs1_val_H); + let (s2, e2, m2) = fsplit (rs2_val_H); + let rd_val_H = fmake (s1 ^ s2, e1, m1); F_or_X_H(rd) = rd_val_H; RETIRE_SUCCESS @@ -375,13 +275,13 @@ function clause execute (F_BIN_TYPE_H(rs2, rs1, rd, FMIN_H)) = { let is_quiet = true; let (rs1_lt_rs2, fflags) = fle_H (rs1_val_H, rs2_val_H, is_quiet); - let rd_val_H = if (f_is_NaN_H(rs1_val_H) & f_is_NaN_H(rs2_val_H)) then canonical_NaN(16) - else if f_is_NaN_H(rs1_val_H) then rs2_val_H - else if f_is_NaN_H(rs2_val_H) then rs1_val_H - else if (f_is_neg_zero_H(rs1_val_H) & f_is_pos_zero_H(rs2_val_H)) then rs1_val_H - else if (f_is_neg_zero_H(rs2_val_H) & f_is_pos_zero_H(rs1_val_H)) then rs2_val_H - else if rs1_lt_rs2 then rs1_val_H - else /* (not rs1_lt_rs2) */ rs2_val_H; + 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 + else if f_is_NaN(rs2_val_H) then rs1_val_H + else if (f_is_neg_zero(rs1_val_H) & f_is_pos_zero(rs2_val_H)) then rs1_val_H + else if (f_is_neg_zero(rs2_val_H) & f_is_pos_zero(rs1_val_H)) then rs2_val_H + else if rs1_lt_rs2 then rs1_val_H + else /* (not rs1_lt_rs2) */ rs2_val_H; accrue_fflags(fflags); F_or_X_H(rd) = rd_val_H; @@ -395,13 +295,13 @@ function clause execute (F_BIN_TYPE_H(rs2, rs1, rd, FMAX_H)) = { let is_quiet = true; let (rs2_lt_rs1, fflags) = fle_H (rs2_val_H, rs1_val_H, is_quiet); - let rd_val_H = if (f_is_NaN_H(rs1_val_H) & f_is_NaN_H(rs2_val_H)) then canonical_NaN(16) - else if f_is_NaN_H(rs1_val_H) then rs2_val_H - else if f_is_NaN_H(rs2_val_H) then rs1_val_H - else if (f_is_neg_zero_H(rs1_val_H) & f_is_pos_zero_H(rs2_val_H)) then rs2_val_H - else if (f_is_neg_zero_H(rs2_val_H) & f_is_pos_zero_H(rs1_val_H)) then rs1_val_H - else if rs2_lt_rs1 then rs1_val_H - else /* (not rs2_lt_rs1) */ rs2_val_H; + 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 + else if f_is_NaN(rs2_val_H) then rs1_val_H + else if (f_is_neg_zero(rs1_val_H) & f_is_pos_zero(rs2_val_H)) then rs2_val_H + else if (f_is_neg_zero(rs2_val_H) & f_is_pos_zero(rs1_val_H)) then rs1_val_H + else if rs2_lt_rs1 then rs1_val_H + else /* (not rs2_lt_rs1) */ rs2_val_H; accrue_fflags(fflags); F_or_X_H(rd) = rd_val_H; @@ -893,16 +793,16 @@ function clause execute (F_UN_TYPE_H(rs1, rd, FCLASS_H)) = { let rs1_val_H = F_or_X_H(rs1); let rd_val_10b : bits (10) = - if f_is_neg_inf_H (rs1_val_H) then 0b_00_0000_0001 - else if f_is_neg_norm_H (rs1_val_H) then 0b_00_0000_0010 - else if f_is_neg_subnorm_H (rs1_val_H) then 0b_00_0000_0100 - else if f_is_neg_zero_H (rs1_val_H) then 0b_00_0000_1000 - else if f_is_pos_zero_H (rs1_val_H) then 0b_00_0001_0000 - else if f_is_pos_subnorm_H (rs1_val_H) then 0b_00_0010_0000 - else if f_is_pos_norm_H (rs1_val_H) then 0b_00_0100_0000 - else if f_is_pos_inf_H (rs1_val_H) then 0b_00_1000_0000 - else if f_is_SNaN_H (rs1_val_H) then 0b_01_0000_0000 - else if f_is_QNaN_H (rs1_val_H) then 0b_10_0000_0000 + if f_is_neg_inf (rs1_val_H) then 0b_00_0000_0001 + else if f_is_neg_norm (rs1_val_H) then 0b_00_0000_0010 + else if f_is_neg_subnorm (rs1_val_H) then 0b_00_0000_0100 + else if f_is_neg_zero (rs1_val_H) then 0b_00_0000_1000 + else if f_is_pos_zero (rs1_val_H) then 0b_00_0001_0000 + else if f_is_pos_subnorm (rs1_val_H) then 0b_00_0010_0000 + else if f_is_pos_norm (rs1_val_H) then 0b_00_0100_0000 + else if f_is_pos_inf (rs1_val_H) then 0b_00_1000_0000 + else if f_is_SNaN (rs1_val_H) then 0b_01_0000_0000 + else if f_is_QNaN (rs1_val_H) then 0b_10_0000_0000 else zeros(); X(rd) = zero_extend (rd_val_10b); diff --git a/sail-riscv.install b/sail-riscv.install index 7a539dfb5..af7d71318 100644 --- a/sail-riscv.install +++ b/sail-riscv.install @@ -1,2 +1,2 @@ bin: ["c_emulator/riscv_sim_RV64" "c_emulator/riscv_sim_RV32"] -share: [ "model/main.sail" {"model/main.sail"} "model/prelude.sail" {"model/prelude.sail"} "model/prelude_mem.sail" {"model/prelude_mem.sail"} "model/prelude_mem_metadata.sail" {"model/prelude_mem_metadata.sail"} "model/riscv_addr_checks.sail" {"model/riscv_addr_checks.sail"} "model/riscv_addr_checks_common.sail" {"model/riscv_addr_checks_common.sail"} "model/riscv_analysis.sail" {"model/riscv_analysis.sail"} "model/riscv_csr_ext.sail" {"model/riscv_csr_ext.sail"} "model/riscv_csr_map.sail" {"model/riscv_csr_map.sail"} "model/riscv_decode_ext.sail" {"model/riscv_decode_ext.sail"} "model/riscv_ext_regs.sail" {"model/riscv_ext_regs.sail"} "model/riscv_fdext_control.sail" {"model/riscv_fdext_control.sail"} "model/riscv_fdext_regs.sail" {"model/riscv_fdext_regs.sail"} "model/riscv_fetch.sail" {"model/riscv_fetch.sail"} "model/riscv_fetch_rvfi.sail" {"model/riscv_fetch_rvfi.sail"} "model/riscv_flen_D.sail" {"model/riscv_flen_D.sail"} "model/riscv_flen_F.sail" {"model/riscv_flen_F.sail"} "model/riscv_freg_type.sail" {"model/riscv_freg_type.sail"} "model/riscv_insts_aext.sail" {"model/riscv_insts_aext.sail"} "model/riscv_insts_base.sail" {"model/riscv_insts_base.sail"} "model/riscv_insts_begin.sail" {"model/riscv_insts_begin.sail"} "model/riscv_insts_cdext.sail" {"model/riscv_insts_cdext.sail"} "model/riscv_insts_cext.sail" {"model/riscv_insts_cext.sail"} "model/riscv_insts_cfext.sail" {"model/riscv_insts_cfext.sail"} "model/riscv_insts_dext.sail" {"model/riscv_insts_dext.sail"} "model/riscv_insts_end.sail" {"model/riscv_insts_end.sail"} "model/riscv_insts_fext.sail" {"model/riscv_insts_fext.sail"} "model/riscv_insts_hints.sail" {"model/riscv_insts_hints.sail"} "model/riscv_insts_mext.sail" {"model/riscv_insts_mext.sail"} "model/riscv_insts_next.sail" {"model/riscv_insts_next.sail"} "model/riscv_insts_rmem.sail" {"model/riscv_insts_rmem.sail"} "model/riscv_insts_zba.sail" {"model/riscv_insts_zba.sail"} "model/riscv_insts_zbb.sail" {"model/riscv_insts_zbb.sail"} "model/riscv_insts_zbc.sail" {"model/riscv_insts_zbc.sail"} "model/riscv_insts_zbkb.sail" {"model/riscv_insts_zbkb.sail"} "model/riscv_insts_zbkx.sail" {"model/riscv_insts_zbkx.sail"} "model/riscv_insts_zbs.sail" {"model/riscv_insts_zbs.sail"} "model/riscv_insts_zfh.sail" {"model/riscv_insts_zfh.sail"} "model/riscv_insts_zicsr.sail" {"model/riscv_insts_zicsr.sail"} "model/riscv_insts_zkn.sail" {"model/riscv_insts_zkn.sail"} "model/riscv_insts_zks.sail" {"model/riscv_insts_zks.sail"} "model/riscv_jalr_rmem.sail" {"model/riscv_jalr_rmem.sail"} "model/riscv_jalr_seq.sail" {"model/riscv_jalr_seq.sail"} "model/riscv_mem.sail" {"model/riscv_mem.sail"} "model/riscv_misa_ext.sail" {"model/riscv_misa_ext.sail"} "model/riscv_next_control.sail" {"model/riscv_next_control.sail"} "model/riscv_next_regs.sail" {"model/riscv_next_regs.sail"} "model/riscv_pc_access.sail" {"model/riscv_pc_access.sail"} "model/riscv_platform.sail" {"model/riscv_platform.sail"} "model/riscv_pmp_control.sail" {"model/riscv_pmp_control.sail"} "model/riscv_pmp_regs.sail" {"model/riscv_pmp_regs.sail"} "model/riscv_pte.sail" {"model/riscv_pte.sail"} "model/riscv_ptw.sail" {"model/riscv_ptw.sail"} "model/riscv_reg_type.sail" {"model/riscv_reg_type.sail"} "model/riscv_regs.sail" {"model/riscv_regs.sail"} "model/riscv_softfloat_interface.sail" {"model/riscv_softfloat_interface.sail"} "model/riscv_step.sail" {"model/riscv_step.sail"} "model/riscv_step_common.sail" {"model/riscv_step_common.sail"} "model/riscv_step_ext.sail" {"model/riscv_step_ext.sail"} "model/riscv_step_rvfi.sail" {"model/riscv_step_rvfi.sail"} "model/riscv_sync_exception.sail" {"model/riscv_sync_exception.sail"} "model/riscv_sys_control.sail" {"model/riscv_sys_control.sail"} "model/riscv_sys_exceptions.sail" {"model/riscv_sys_exceptions.sail"} "model/riscv_sys_regs.sail" {"model/riscv_sys_regs.sail"} "model/riscv_termination_common.sail" {"model/riscv_termination_common.sail"} "model/riscv_termination_rv32.sail" {"model/riscv_termination_rv32.sail"} "model/riscv_termination_rv64.sail" {"model/riscv_termination_rv64.sail"} "model/riscv_types.sail" {"model/riscv_types.sail"} "model/riscv_types_common.sail" {"model/riscv_types_common.sail"} "model/riscv_types_ext.sail" {"model/riscv_types_ext.sail"} "model/riscv_types_kext.sail" {"model/riscv_types_kext.sail"} "model/riscv_vmem_common.sail" {"model/riscv_vmem_common.sail"} "model/riscv_vmem_rv32.sail" {"model/riscv_vmem_rv32.sail"} "model/riscv_vmem_rv64.sail" {"model/riscv_vmem_rv64.sail"} "model/riscv_vmem_sv32.sail" {"model/riscv_vmem_sv32.sail"} "model/riscv_vmem_sv39.sail" {"model/riscv_vmem_sv39.sail"} "model/riscv_vmem_sv48.sail" {"model/riscv_vmem_sv48.sail"} "model/riscv_vmem_tlb.sail" {"model/riscv_vmem_tlb.sail"} "model/riscv_vmem_types.sail" {"model/riscv_vmem_types.sail"} "model/riscv_xlen32.sail" {"model/riscv_xlen32.sail"} "model/riscv_xlen64.sail" {"model/riscv_xlen64.sail"} "model/rvfi_dii.sail" {"model/rvfi_dii.sail"} "c_emulator/riscv_platform.c" {"c_emulator/riscv_platform.c"} "c_emulator/riscv_platform_impl.c" {"c_emulator/riscv_platform_impl.c"} "c_emulator/riscv_prelude.c" {"c_emulator/riscv_prelude.c"} "c_emulator/riscv_sim.c" {"c_emulator/riscv_sim.c"} "c_emulator/riscv_softfloat.c" {"c_emulator/riscv_softfloat.c"} "c_emulator/riscv_config.h" {"c_emulator/riscv_config.h"} "c_emulator/riscv_platform.h" {"c_emulator/riscv_platform.h"} "c_emulator/riscv_platform_impl.h" {"c_emulator/riscv_platform_impl.h"} "c_emulator/riscv_prelude.h" {"c_emulator/riscv_prelude.h"} "c_emulator/riscv_sail.h" {"c_emulator/riscv_sail.h"} "c_emulator/riscv_softfloat.h" {"c_emulator/riscv_softfloat.h"} "handwritten_support/mem_metadata.lem" {"handwritten_support/mem_metadata.lem"} "handwritten_support/riscv_extras.lem" {"handwritten_support/riscv_extras.lem"} "handwritten_support/riscv_extras_fdext.lem" {"handwritten_support/riscv_extras_fdext.lem"} "handwritten_support/riscv_extras_sequential.lem" {"handwritten_support/riscv_extras_sequential.lem"} "handwritten_support/hgen/ast.hgen" {"handwritten_support/hgen/ast.hgen"} "handwritten_support/hgen/fold.hgen" {"handwritten_support/hgen/fold.hgen"} "handwritten_support/hgen/herdtools_ast_to_shallow_ast.hgen" {"handwritten_support/hgen/herdtools_ast_to_shallow_ast.hgen"} "handwritten_support/hgen/herdtools_types_to_shallow_types.hgen" {"handwritten_support/hgen/herdtools_types_to_shallow_types.hgen"} "handwritten_support/hgen/lexer.hgen" {"handwritten_support/hgen/lexer.hgen"} "handwritten_support/hgen/lexer_regexps.hgen" {"handwritten_support/hgen/lexer_regexps.hgen"} "handwritten_support/hgen/map.hgen" {"handwritten_support/hgen/map.hgen"} "handwritten_support/hgen/parser.hgen" {"handwritten_support/hgen/parser.hgen"} "handwritten_support/hgen/pretty.hgen" {"handwritten_support/hgen/pretty.hgen"} "handwritten_support/hgen/pretty_xml.hgen" {"handwritten_support/hgen/pretty_xml.hgen"} "handwritten_support/hgen/sail_trans_out.hgen" {"handwritten_support/hgen/sail_trans_out.hgen"} "handwritten_support/hgen/shallow_ast_to_herdtools_ast.hgen" {"handwritten_support/hgen/shallow_ast_to_herdtools_ast.hgen"} "handwritten_support/hgen/shallow_types_to_herdtools_types.hgen" {"handwritten_support/hgen/shallow_types_to_herdtools_types.hgen"} "handwritten_support/hgen/token_types.hgen" {"handwritten_support/hgen/token_types.hgen"} "handwritten_support/hgen/tokens.hgen" {"handwritten_support/hgen/tokens.hgen"} "handwritten_support/hgen/trans_sail.hgen" {"handwritten_support/hgen/trans_sail.hgen"} "handwritten_support/hgen/types.hgen" {"handwritten_support/hgen/types.hgen"} "handwritten_support/hgen/types_sail_trans_out.hgen" {"handwritten_support/hgen/types_sail_trans_out.hgen"} "handwritten_support/hgen/types_trans_sail.hgen" {"handwritten_support/hgen/types_trans_sail.hgen"} "handwritten_support/0.11/mem_metadata.lem" {"handwritten_support/0.11/mem_metadata.lem"} "handwritten_support/0.11/riscv_extras.lem" {"handwritten_support/0.11/riscv_extras.lem"} "handwritten_support/0.11/riscv_extras_fdext.lem" {"handwritten_support/0.11/riscv_extras_fdext.lem"} "handwritten_support/0.11/riscv_extras_sequential.lem" {"handwritten_support/0.11/riscv_extras_sequential.lem"} "generated_definitions/for-rmem/riscv.lem" {"generated_definitions/for-rmem/riscv.lem"} "generated_definitions/for-rmem/riscv_types.lem" {"generated_definitions/for-rmem/riscv_types.lem"} "generated_definitions/for-rmem/riscv_toFromInterp2.ml" {"generated_definitions/for-rmem/riscv_toFromInterp2.ml"} "generated_definitions/for-rmem/riscv.defs" {"generated_definitions/for-rmem/riscv.defs"} ] +share: [ "model/main.sail" {"model/main.sail"} "model/prelude.sail" {"model/prelude.sail"} "model/prelude_mem.sail" {"model/prelude_mem.sail"} "model/prelude_mem_metadata.sail" {"model/prelude_mem_metadata.sail"} "model/riscv_addr_checks.sail" {"model/riscv_addr_checks.sail"} "model/riscv_addr_checks_common.sail" {"model/riscv_addr_checks_common.sail"} "model/riscv_analysis.sail" {"model/riscv_analysis.sail"} "model/riscv_csr_ext.sail" {"model/riscv_csr_ext.sail"} "model/riscv_csr_map.sail" {"model/riscv_csr_map.sail"} "model/riscv_decode_ext.sail" {"model/riscv_decode_ext.sail"} "model/riscv_ext_regs.sail" {"model/riscv_ext_regs.sail"} "model/riscv_fdext_control.sail" {"model/riscv_fdext_control.sail"} "model/riscv_fdext_regs.sail" {"model/riscv_fdext_regs.sail"} "model/riscv_fetch.sail" {"model/riscv_fetch.sail"} "model/riscv_fetch_rvfi.sail" {"model/riscv_fetch_rvfi.sail"} "model/riscv_flen_D.sail" {"model/riscv_flen_D.sail"} "model/riscv_flen_F.sail" {"model/riscv_flen_F.sail"} "model/riscv_freg_type.sail" {"model/riscv_freg_type.sail"} "model/riscv_insts_aext.sail" {"model/riscv_insts_aext.sail"} "model/riscv_insts_base.sail" {"model/riscv_insts_base.sail"} "model/riscv_insts_begin.sail" {"model/riscv_insts_begin.sail"} "model/riscv_insts_cdext.sail" {"model/riscv_insts_cdext.sail"} "model/riscv_insts_cext.sail" {"model/riscv_insts_cext.sail"} "model/riscv_insts_cfext.sail" {"model/riscv_insts_cfext.sail"} "model/riscv_insts_dext.sail" {"model/riscv_insts_dext.sail"} "model/riscv_insts_end.sail" {"model/riscv_insts_end.sail"} "model/riscv_insts_fext.sail" {"model/riscv_insts_fext.sail"} "model/riscv_insts_hints.sail" {"model/riscv_insts_hints.sail"} "model/riscv_insts_mext.sail" {"model/riscv_insts_mext.sail"} "model/riscv_insts_next.sail" {"model/riscv_insts_next.sail"} "model/riscv_insts_rmem.sail" {"model/riscv_insts_rmem.sail"} "model/riscv_insts_zba.sail" {"model/riscv_insts_zba.sail"} "model/riscv_insts_zbb.sail" {"model/riscv_insts_zbb.sail"} "model/riscv_insts_zbc.sail" {"model/riscv_insts_zbc.sail"} "model/riscv_insts_zbkb.sail" {"model/riscv_insts_zbkb.sail"} "model/riscv_insts_zbkx.sail" {"model/riscv_insts_zbkx.sail"} "model/riscv_insts_zbs.sail" {"model/riscv_insts_zbs.sail"} "model/riscv_insts_zfh.sail" {"model/riscv_insts_zfh.sail"} "model/riscv_insts_zicsr.sail" {"model/riscv_insts_zicsr.sail"} "model/riscv_insts_zkn.sail" {"model/riscv_insts_zkn.sail"} "model/riscv_insts_zks.sail" {"model/riscv_insts_zks.sail"} "model/riscv_jalr_rmem.sail" {"model/riscv_jalr_rmem.sail"} "model/riscv_jalr_seq.sail" {"model/riscv_jalr_seq.sail"} "model/riscv_mem.sail" {"model/riscv_mem.sail"} "model/riscv_misa_ext.sail" {"model/riscv_misa_ext.sail"} "model/riscv_next_control.sail" {"model/riscv_next_control.sail"} "model/riscv_next_regs.sail" {"model/riscv_next_regs.sail"} "model/riscv_pc_access.sail" {"model/riscv_pc_access.sail"} "model/riscv_platform.sail" {"model/riscv_platform.sail"} "model/riscv_pmp_control.sail" {"model/riscv_pmp_control.sail"} "model/riscv_pmp_regs.sail" {"model/riscv_pmp_regs.sail"} "model/riscv_pte.sail" {"model/riscv_pte.sail"} "model/riscv_ptw.sail" {"model/riscv_ptw.sail"} "model/riscv_reg_type.sail" {"model/riscv_reg_type.sail"} "model/riscv_regs.sail" {"model/riscv_regs.sail"} "model/riscv_float.sail" {"model/riscv_float.sail"} "model/riscv_softfloat_interface.sail" {"model/riscv_softfloat_interface.sail"} "model/riscv_step.sail" {"model/riscv_step.sail"} "model/riscv_step_common.sail" {"model/riscv_step_common.sail"} "model/riscv_step_ext.sail" {"model/riscv_step_ext.sail"} "model/riscv_step_rvfi.sail" {"model/riscv_step_rvfi.sail"} "model/riscv_sync_exception.sail" {"model/riscv_sync_exception.sail"} "model/riscv_sys_control.sail" {"model/riscv_sys_control.sail"} "model/riscv_sys_exceptions.sail" {"model/riscv_sys_exceptions.sail"} "model/riscv_sys_regs.sail" {"model/riscv_sys_regs.sail"} "model/riscv_termination_common.sail" {"model/riscv_termination_common.sail"} "model/riscv_termination_rv32.sail" {"model/riscv_termination_rv32.sail"} "model/riscv_termination_rv64.sail" {"model/riscv_termination_rv64.sail"} "model/riscv_types.sail" {"model/riscv_types.sail"} "model/riscv_types_common.sail" {"model/riscv_types_common.sail"} "model/riscv_types_ext.sail" {"model/riscv_types_ext.sail"} "model/riscv_types_kext.sail" {"model/riscv_types_kext.sail"} "model/riscv_vmem_common.sail" {"model/riscv_vmem_common.sail"} "model/riscv_vmem_rv32.sail" {"model/riscv_vmem_rv32.sail"} "model/riscv_vmem_rv64.sail" {"model/riscv_vmem_rv64.sail"} "model/riscv_vmem_sv32.sail" {"model/riscv_vmem_sv32.sail"} "model/riscv_vmem_sv39.sail" {"model/riscv_vmem_sv39.sail"} "model/riscv_vmem_sv48.sail" {"model/riscv_vmem_sv48.sail"} "model/riscv_vmem_tlb.sail" {"model/riscv_vmem_tlb.sail"} "model/riscv_vmem_types.sail" {"model/riscv_vmem_types.sail"} "model/riscv_xlen32.sail" {"model/riscv_xlen32.sail"} "model/riscv_xlen64.sail" {"model/riscv_xlen64.sail"} "model/rvfi_dii.sail" {"model/rvfi_dii.sail"} "c_emulator/riscv_platform.c" {"c_emulator/riscv_platform.c"} "c_emulator/riscv_platform_impl.c" {"c_emulator/riscv_platform_impl.c"} "c_emulator/riscv_prelude.c" {"c_emulator/riscv_prelude.c"} "c_emulator/riscv_sim.c" {"c_emulator/riscv_sim.c"} "c_emulator/riscv_softfloat.c" {"c_emulator/riscv_softfloat.c"} "c_emulator/riscv_config.h" {"c_emulator/riscv_config.h"} "c_emulator/riscv_platform.h" {"c_emulator/riscv_platform.h"} "c_emulator/riscv_platform_impl.h" {"c_emulator/riscv_platform_impl.h"} "c_emulator/riscv_prelude.h" {"c_emulator/riscv_prelude.h"} "c_emulator/riscv_sail.h" {"c_emulator/riscv_sail.h"} "c_emulator/riscv_softfloat.h" {"c_emulator/riscv_softfloat.h"} "handwritten_support/mem_metadata.lem" {"handwritten_support/mem_metadata.lem"} "handwritten_support/riscv_extras.lem" {"handwritten_support/riscv_extras.lem"} "handwritten_support/riscv_extras_fdext.lem" {"handwritten_support/riscv_extras_fdext.lem"} "handwritten_support/riscv_extras_sequential.lem" {"handwritten_support/riscv_extras_sequential.lem"} "handwritten_support/hgen/ast.hgen" {"handwritten_support/hgen/ast.hgen"} "handwritten_support/hgen/fold.hgen" {"handwritten_support/hgen/fold.hgen"} "handwritten_support/hgen/herdtools_ast_to_shallow_ast.hgen" {"handwritten_support/hgen/herdtools_ast_to_shallow_ast.hgen"} "handwritten_support/hgen/herdtools_types_to_shallow_types.hgen" {"handwritten_support/hgen/herdtools_types_to_shallow_types.hgen"} "handwritten_support/hgen/lexer.hgen" {"handwritten_support/hgen/lexer.hgen"} "handwritten_support/hgen/lexer_regexps.hgen" {"handwritten_support/hgen/lexer_regexps.hgen"} "handwritten_support/hgen/map.hgen" {"handwritten_support/hgen/map.hgen"} "handwritten_support/hgen/parser.hgen" {"handwritten_support/hgen/parser.hgen"} "handwritten_support/hgen/pretty.hgen" {"handwritten_support/hgen/pretty.hgen"} "handwritten_support/hgen/pretty_xml.hgen" {"handwritten_support/hgen/pretty_xml.hgen"} "handwritten_support/hgen/sail_trans_out.hgen" {"handwritten_support/hgen/sail_trans_out.hgen"} "handwritten_support/hgen/shallow_ast_to_herdtools_ast.hgen" {"handwritten_support/hgen/shallow_ast_to_herdtools_ast.hgen"} "handwritten_support/hgen/shallow_types_to_herdtools_types.hgen" {"handwritten_support/hgen/shallow_types_to_herdtools_types.hgen"} "handwritten_support/hgen/token_types.hgen" {"handwritten_support/hgen/token_types.hgen"} "handwritten_support/hgen/tokens.hgen" {"handwritten_support/hgen/tokens.hgen"} "handwritten_support/hgen/trans_sail.hgen" {"handwritten_support/hgen/trans_sail.hgen"} "handwritten_support/hgen/types.hgen" {"handwritten_support/hgen/types.hgen"} "handwritten_support/hgen/types_sail_trans_out.hgen" {"handwritten_support/hgen/types_sail_trans_out.hgen"} "handwritten_support/hgen/types_trans_sail.hgen" {"handwritten_support/hgen/types_trans_sail.hgen"} "handwritten_support/0.11/mem_metadata.lem" {"handwritten_support/0.11/mem_metadata.lem"} "handwritten_support/0.11/riscv_extras.lem" {"handwritten_support/0.11/riscv_extras.lem"} "handwritten_support/0.11/riscv_extras_fdext.lem" {"handwritten_support/0.11/riscv_extras_fdext.lem"} "handwritten_support/0.11/riscv_extras_sequential.lem" {"handwritten_support/0.11/riscv_extras_sequential.lem"} "generated_definitions/for-rmem/riscv.lem" {"generated_definitions/for-rmem/riscv.lem"} "generated_definitions/for-rmem/riscv_types.lem" {"generated_definitions/for-rmem/riscv_types.lem"} "generated_definitions/for-rmem/riscv_toFromInterp2.ml" {"generated_definitions/for-rmem/riscv_toFromInterp2.ml"} "generated_definitions/for-rmem/riscv.defs" {"generated_definitions/for-rmem/riscv.defs"} ]