diff --git a/config.svh b/config.svh index f30a234..d52206f 100644 --- a/config.svh +++ b/config.svh @@ -1,28 +1,28 @@ // define macros for which models to check coverage for // e.g. `define COVER_B1 for model B1 -`define COVER_B1 -`define COVER_B2 -`define COVER_B3 -`define COVER_B4 -`define COVER_B5 +//`define COVER_B1 +//`define COVER_B2 +//`define COVER_B3 +//`define COVER_B4 +//`define COVER_B5 // `define COVER_B6 // `define COVER_B7 // `define COVER_B8 -`define COVER_B9 -`define COVER_B10 +//`define COVER_B9 +//`define COVER_B10 // `define COVER_B11 -`define COVER_B12 +//`define COVER_B12 // `define COVER_B13 -`define COVER_B14 +//`define COVER_B14 // `define COVER_B15 -`define COVER_B16 +// `define COVER_B16 // `define COVER_B17 // `define COVER_B18 `define COVER_B19 // `define COVER_B20 -`define COVER_B21 -`define COVER_B22 +//`define COVER_B21 +// `define COVER_B22 // `define COVER_B23 // `define COVER_B24 // `define COVER_B25 diff --git a/coverage/covergroups/B19-2.svh b/coverage/covergroups/B19-2.svh new file mode 100644 index 0000000..d3e7f46 --- /dev/null +++ b/coverage/covergroups/B19-2.svh @@ -0,0 +1,780 @@ +covergroup B19_cg (virtual coverfloat_interface CFI); + + option.per_instance = 0; + + FP_compare_ops: coverpoint CFI.op { + type_option.weight = 0; + + bins min = {OP_MIN}; + bins max = {OP_MAX}; + bins feq = {OP_FEQ}; + bins flt = {OP_FLT}; + bins fle = {OP_FLE}; + } + + + F16_result_fmt: coverpoint CFI.resultFmt == FMT_HALF { + type_option.weight = 0; + // half precision format for result + bins f16 = {1}; + } + + F16_operand_a_sign: coverpoint CFI.a[F16_SIGN_BIT] { + type_option.weight = 0; + + bins pos = {0}; + bins neg = {1}; + } + + F16_operand_b_sign: coverpoint CFI.b[F16_SIGN_BIT] { + type_option.weight = 0; + + bins pos = {0}; + bins neg = {1}; + } + + F16_a_norm: coverpoint (CFI.a[F16_E_UPPER : F16_E_LOWER] != 0 && CFI.a[F16_E_UPPER : F16_E_LOWER] != '1) { + type_option.weight = 0; + + bins normal = {1}; + } + + F16_b_norm: coverpoint (CFI.b[F16_E_UPPER : F16_E_LOWER] != 0 && CFI.b[F16_E_UPPER : F16_E_LOWER] != '1) { + type_option.weight = 0; + + bins normal = {1}; + } + + F16_a_subnorm: coverpoint (CFI.a[F16_E_UPPER : F16_E_LOWER] == 0 && CFI.a[F16_M_BITS-1 : 0] != 0) { + type_option.weight = 0; + + bins subnormal = {1}; + } + + F16_b_subnorm: coverpoint (CFI.b[F16_E_UPPER : F16_E_LOWER] == 0 && CFI.b[F16_M_BITS-1 : 0] != 0) { + type_option.weight = 0; + + bins subnormal = {1}; + } + + F16_a_zero: coverpoint (CFI.a[F16_E_UPPER : 0] == 0) { + type_option.weight = 0; + + bins zero = {1}; + } + + F16_b_zero: coverpoint (CFI.b[F16_E_UPPER : 0] == 0) { + type_option.weight = 0; + + bins zero = {1}; + } + + F16_exp_compare: coverpoint $signed( + (effective_exponent(CFI.a, FMT_HALF) + - effective_exponent(CFI.b, FMT_HALF))) { + type_option.weight = 0; + + bins lt = {[$ : -1]}; + bins eq = {0}; + bins gt = {[1 : $]}; + + } + + F16_frac_compare: coverpoint $signed( + (effective_fraction(CFI.a, FMT_HALF) + - effective_fraction(CFI.b, FMT_HALF))) { + type_option.weight = 0; + + bins lt = {[$ : -1]}; + bins eq = {0}; + bins gt = {[1 : $]}; + + } + + F16_frac_LTE: coverpoint $signed( + (effective_fraction(CFI.a, FMT_HALF) + - effective_fraction(CFI.b, FMT_HALF))) { + type_option.weight = 0; + + bins lt = {[$ : -1]}; + bins eq = {0}; + // bins gt = {[1 : $]}; + + } + + F16_frac_GTE: coverpoint $signed( + (effective_fraction(CFI.a, FMT_HALF) + - effective_fraction(CFI.b, FMT_HALF))) { + type_option.weight = 0; + + // bins lt = {[$ : -1]}; + bins eq = {0}; + bins gt = {[1 : $]}; + + } + + F16_frac_LT: coverpoint $signed( + (effective_fraction(CFI.a, FMT_HALF) + - effective_fraction(CFI.b, FMT_HALF))) { + type_option.weight = 0; + + bins lt = {[$ : -1]}; + // bins eq = {0}; + // bins gt = {[1 : $]}; + + } + + F16_frac_GT: coverpoint $signed( + (effective_fraction(CFI.a, FMT_HALF) + - effective_fraction(CFI.b, FMT_HALF))) { + type_option.weight = 0; + + // bins lt = {[$ : -1]}; + // bins eq = {0}; + bins gt = {[1 : $]}; + + } + + + BF16_result_fmt: coverpoint CFI.resultFmt == FMT_BF16 { + type_option.weight = 0; + // BF16 precision format for result + bins bf16 = {1}; + } + + BF16_operand_a_sign: coverpoint CFI.a[BF16_SIGN_BIT] { + type_option.weight = 0; + + bins pos = {0}; + bins neg = {1}; + } + + BF16_operand_b_sign: coverpoint CFI.b[BF16_SIGN_BIT] { + type_option.weight = 0; + + bins pos = {0}; + bins neg = {1}; + } + + BF16_a_norm: coverpoint (CFI.a[BF16_E_UPPER : BF16_E_LOWER] != 0 && CFI.a[BF16_E_UPPER : BF16_E_LOWER] != '1) { + type_option.weight = 0; + + bins normal = {1}; + } + + BF16_b_norm: coverpoint (CFI.b[BF16_E_UPPER : BF16_E_LOWER] != 0 && CFI.b[BF16_E_UPPER : BF16_E_LOWER] != '1) { + type_option.weight = 0; + + bins normal = {1}; + } + + BF16_a_subnorm: coverpoint (CFI.a[BF16_E_UPPER : BF16_E_LOWER] == 0 && CFI.a[BF16_M_BITS-1 : 0] != 0) { + type_option.weight = 0; + + bins subnormal = {1}; + } + + BF16_b_subnorm: coverpoint (CFI.b[BF16_E_UPPER : BF16_E_LOWER] == 0 && CFI.b[BF16_M_BITS-1 : 0] != 0) { + type_option.weight = 0; + + bins subnormal = {1}; + } + + BF16_a_zero: coverpoint (CFI.a[BF16_E_UPPER : 0] == 0) { + type_option.weight = 0; + + bins zero = {1}; + } + + BF16_b_zero: coverpoint (CFI.b[BF16_E_UPPER : 0] == 0) { + type_option.weight = 0; + + bins zero = {1}; + } + + BF16_exp_compare: coverpoint $signed( + (effective_exponent(CFI.a, FMT_BF16) + - effective_exponent(CFI.b, FMT_BF16))) { + type_option.weight = 0; + + bins lt = {[$ : -1]}; + bins eq = {0}; + bins gt = {[1 : $]}; + + } + + BF16_frac_compare: coverpoint $signed( + (effective_fraction(CFI.a, FMT_BF16) + - effective_fraction(CFI.b, FMT_BF16))) { + type_option.weight = 0; + + bins lt = {[$ : -1]}; + bins eq = {0}; + bins gt = {[1 : $]}; + + } + + BF16_frac_LTE: coverpoint $signed( + (effective_fraction(CFI.a, FMT_BF16) + - effective_fraction(CFI.b, FMT_BF16))) { + type_option.weight = 0; + + bins lt = {[$ : -1]}; + bins eq = {0}; + // bins gt = {[1 : $]}; + + } + + BF16_frac_GTE: coverpoint $signed( + (effective_fraction(CFI.a, FMT_BF16) + - effective_fraction(CFI.b, FMT_BF16))) { + type_option.weight = 0; + + // bins lt = {[$ : -1]}; + bins eq = {0}; + bins gt = {[1 : $]}; + + } + + BF16_frac_LT: coverpoint $signed( + (effective_fraction(CFI.a, FMT_BF16) + - effective_fraction(CFI.b, FMT_BF16))) { + type_option.weight = 0; + + bins lt = {[$ : -1]}; + // bins eq = {0}; + // bins gt = {[1 : $]}; + + } + + BF16_frac_GT: coverpoint $signed( + (effective_fraction(CFI.a, FMT_BF16) + - effective_fraction(CFI.b, FMT_BF16))) { + type_option.weight = 0; + + // bins lt = {[$ : -1]}; + // bins eq = {0}; + bins gt = {[1 : $]}; + + } + + F32_result_fmt: coverpoint CFI.resultFmt == FMT_SINGLE { + type_option.weight = 0; + // single precision format for result + bins f32 = {1}; + } + + F32_operand_a_sign: coverpoint CFI.a[F32_SIGN_BIT] { + type_option.weight = 0; + + bins pos = {0}; + bins neg = {1}; + } + + F32_operand_b_sign: coverpoint CFI.b[F32_SIGN_BIT] { + type_option.weight = 0; + + bins pos = {0}; + bins neg = {1}; + } + + F32_a_norm: coverpoint (CFI.a[F32_E_UPPER : F32_E_LOWER] != 0 && CFI.a[F32_E_UPPER : F32_E_LOWER] != '1) { + type_option.weight = 0; + + bins normal = {1}; + } + + F32_b_norm: coverpoint (CFI.b[F32_E_UPPER : F32_E_LOWER] != 0 && CFI.b[F32_E_UPPER : F32_E_LOWER] != '1) { + type_option.weight = 0; + + bins normal = {1}; + } + + F32_a_subnorm: coverpoint (CFI.a[F32_E_UPPER : F32_E_LOWER] == 0 && CFI.a[F32_M_BITS-1 : 0] != 0) { + type_option.weight = 0; + + bins subnormal = {1}; + } + + F32_b_subnorm: coverpoint (CFI.b[F32_E_UPPER : F32_E_LOWER] == 0 && CFI.b[F32_M_BITS-1 : 0] != 0) { + type_option.weight = 0; + + bins subnormal = {1}; + } + + F32_a_zero: coverpoint (CFI.a[F32_E_UPPER : 0] == 0) { + type_option.weight = 0; + + bins zero = {1}; + } + + F32_b_zero: coverpoint (CFI.b[F32_E_UPPER : 0] == 0) { + type_option.weight = 0; + + bins zero = {1}; + } + + F32_exp_compare: coverpoint $signed( + (effective_exponent(CFI.a, FMT_SINGLE) + - effective_exponent(CFI.b, FMT_SINGLE))) { + type_option.weight = 0; + + bins lt = {[$ : -1]}; + bins eq = {0}; + bins gt = {[1 : $]}; + + } + + F32_frac_compare: coverpoint $signed( + (effective_fraction(CFI.a, FMT_SINGLE) + - effective_fraction(CFI.b, FMT_SINGLE))) { + type_option.weight = 0; + + bins lt = {[$ : -1]}; + bins eq = {0}; + bins gt = {[1 : $]}; + + } + + F32_frac_LTE: coverpoint $signed( + (effective_fraction(CFI.a, FMT_SINGLE) + - effective_fraction(CFI.b, FMT_SINGLE))) { + type_option.weight = 0; + + bins lt = {[$ : -1]}; + bins eq = {0}; + // bins gt = {[1 : $]}; + + } + + F32_frac_GTE: coverpoint $signed( + (effective_fraction(CFI.a, FMT_SINGLE) + - effective_fraction(CFI.b, FMT_SINGLE))) { + type_option.weight = 0; + + // bins lt = {[$ : -1]}; + bins eq = {0}; + bins gt = {[1 : $]}; + + } + + F32_frac_LT: coverpoint $signed( + (effective_fraction(CFI.a, FMT_SINGLE) + - effective_fraction(CFI.b, FMT_SINGLE))) { + type_option.weight = 0; + + bins lt = {[$ : -1]}; + // bins eq = {0}; + // bins gt = {[1 : $]}; + + } + + F32_frac_GT: coverpoint $signed( + (effective_fraction(CFI.a, FMT_SINGLE) + - effective_fraction(CFI.b, FMT_SINGLE))) { + type_option.weight = 0; + + // bins lt = {[$ : -1]}; + // bins eq = {0}; + bins gt = {[1 : $]}; + + } + + + F64_result_fmt: coverpoint CFI.resultFmt == FMT_DOUBLE { + type_option.weight = 0; + // double precision format for result + bins F64 = {1}; + } + + F64_operand_a_sign: coverpoint CFI.a[F64_SIGN_BIT] { + type_option.weight = 0; + + bins pos = {0}; + bins neg = {1}; + } + + F64_operand_b_sign: coverpoint CFI.b[F64_SIGN_BIT] { + type_option.weight = 0; + + bins pos = {0}; + bins neg = {1}; + } + + F64_a_norm: coverpoint (CFI.a[F64_E_UPPER : F64_E_LOWER] != 0 && CFI.a[F64_E_UPPER : F64_E_LOWER] != '1) { + type_option.weight = 0; + + bins normal = {1}; + } + + F64_b_norm: coverpoint (CFI.b[F64_E_UPPER : F64_E_LOWER] != 0 && CFI.b[F64_E_UPPER : F64_E_LOWER] != '1) { + type_option.weight = 0; + + bins normal = {1}; + } + + F64_a_subnorm: coverpoint (CFI.a[F64_E_UPPER : F64_E_LOWER] == 0 && CFI.a[F64_M_BITS-1 : 0] != 0) { + type_option.weight = 0; + + bins subnormal = {1}; + } + + F64_b_subnorm: coverpoint (CFI.b[F64_E_UPPER : F64_E_LOWER] == 0 && CFI.b[F64_M_BITS-1 : 0] != 0) { + type_option.weight = 0; + + bins subnormal = {1}; + } + + F64_a_zero: coverpoint (CFI.a[F64_E_UPPER : 0] == 0) { + type_option.weight = 0; + + bins zero = {1}; + } + + F64_b_zero: coverpoint (CFI.b[F64_E_UPPER : 0] == 0) { + type_option.weight = 0; + + bins zero = {1}; + } + + F64_exp_compare: coverpoint $signed( + (effective_exponent(CFI.a, FMT_DOUBLE) + - effective_exponent(CFI.b, FMT_DOUBLE))) { + type_option.weight = 0; + + bins lt = {[$ : -1]}; + bins eq = {0}; + bins gt = {[1 : $]}; + + } + + F64_frac_compare: coverpoint $signed( + (effective_fraction(CFI.a, FMT_DOUBLE) + - effective_fraction(CFI.b, FMT_DOUBLE))) { + type_option.weight = 0; + + bins lt = {[$ : -1]}; + bins eq = {0}; + bins gt = {[1 : $]}; + + } + + F64_frac_LTE: coverpoint $signed( + (effective_fraction(CFI.a, FMT_DOUBLE) + - effective_fraction(CFI.b, FMT_DOUBLE))) { + type_option.weight = 0; + + bins lt = {[$ : -1]}; + bins eq = {0}; + // bins gt = {[1 : $]}; + + } + + F64_frac_GTE: coverpoint $signed( + (effective_fraction(CFI.a, FMT_DOUBLE) + - effective_fraction(CFI.b, FMT_DOUBLE))) { + type_option.weight = 0; + + // bins lt = {[$ : -1]}; + bins eq = {0}; + bins gt = {[1 : $]}; + + } + + F64_frac_LT: coverpoint $signed( + (effective_fraction(CFI.a, FMT_DOUBLE) + - effective_fraction(CFI.b, FMT_DOUBLE))) { + type_option.weight = 0; + + bins lt = {[$ : -1]}; + // bins eq = {0}; + // bins gt = {[1 : $]}; + + } + + F64_frac_GT: coverpoint $signed( + (effective_fraction(CFI.a, FMT_DOUBLE) + - effective_fraction(CFI.b, FMT_DOUBLE))) { + type_option.weight = 0; + + // bins lt = {[$ : -1]}; + // bins eq = {0}; + bins gt = {[1 : $]}; + + } + + + F128_result_fmt: coverpoint CFI.resultFmt == FMT_QUAD { + type_option.weight = 0; + // quad precision format for result + bins F128 = {1}; + } + + F128_operand_a_sign: coverpoint CFI.a[F128_SIGN_BIT] { + type_option.weight = 0; + + bins pos = {0}; + bins neg = {1}; + } + + F128_operand_b_sign: coverpoint CFI.b[F128_SIGN_BIT] { + type_option.weight = 0; + + bins pos = {0}; + bins neg = {1}; + } + + F128_a_norm: coverpoint (CFI.a[F128_E_UPPER : F128_E_LOWER] != 0 && CFI.a[F128_E_UPPER : F128_E_LOWER] != '1) { + type_option.weight = 0; + + bins normal = {1}; + } + + F128_b_norm: coverpoint (CFI.b[F128_E_UPPER : F128_E_LOWER] != 0 && CFI.b[F128_E_UPPER : F128_E_LOWER] != '1) { + type_option.weight = 0; + + bins normal = {1}; + } + + F128_a_subnorm: coverpoint (CFI.a[F128_E_UPPER : F128_E_LOWER] == 0 && CFI.a[F128_M_BITS-1 : 0] != 0) { + type_option.weight = 0; + + bins subnormal = {1}; + } + + F128_b_subnorm: coverpoint (CFI.b[F128_E_UPPER : F128_E_LOWER] == 0 && CFI.b[F128_M_BITS-1 : 0] != 0) { + type_option.weight = 0; + + bins subnormal = {1}; + } + + F128_a_zero: coverpoint (CFI.a[F128_E_UPPER : 0] == 0) { + type_option.weight = 0; + + bins zero = {1}; + } + + F128_b_zero: coverpoint (CFI.b[F128_E_UPPER : 0] == 0) { + type_option.weight = 0; + + bins zero = {1}; + } + + F128_exp_compare: coverpoint $signed( + (effective_exponent(CFI.a, FMT_QUAD) + - effective_exponent(CFI.b, FMT_QUAD))) { + type_option.weight = 0; + + bins lt = {[$ : -1]}; + bins eq = {0}; + bins gt = {[1 : $]}; + + } + + F128_frac_compare: coverpoint $signed( + (effective_fraction(CFI.a, FMT_QUAD) + - effective_fraction(CFI.b, FMT_QUAD))) { + type_option.weight = 0; + + bins lt = {[$ : -1]}; + bins eq = {0}; + bins gt = {[1 : $]}; + + } + + F128_frac_LTE: coverpoint $signed( + (effective_fraction(CFI.a, FMT_QUAD) + - effective_fraction(CFI.b, FMT_QUAD))) { + type_option.weight = 0; + + bins lt = {[$ : -1]}; + bins eq = {0}; + // bins gt = {[1 : $]}; + + } + + F128_frac_GTE: coverpoint $signed( + (effective_fraction(CFI.a, FMT_QUAD) + - effective_fraction(CFI.b, FMT_QUAD))) { + type_option.weight = 0; + + // bins lt = {[$ : -1]}; + bins eq = {0}; + bins gt = {[1 : $]}; + + } + + F128_frac_LT: coverpoint $signed( + (effective_fraction(CFI.a, FMT_QUAD) + - effective_fraction(CFI.b, FMT_QUAD))) { + type_option.weight = 0; + + bins lt = {[$ : -1]}; + // bins eq = {0}; + // bins gt = {[1 : $]}; + + } + + F128_frac_GT: coverpoint $signed( + (effective_fraction(CFI.a, FMT_QUAD) + - effective_fraction(CFI.b, FMT_QUAD))) { + type_option.weight = 0; + + // bins lt = {[$ : -1]}; + // bins eq = {0}; + bins gt = {[1 : $]}; + + } + + + `ifdef COVER_F16 + B19_F16__norm_x_norm: cross FP_compare_ops, F16_operand_a_sign, F16_operand_b_sign, F16_a_norm, F16_b_norm, + F16_exp_compare, F16_frac_compare, F16_result_fmt; + + B19_F16__norm_x_subnorm: cross FP_compare_ops, F16_operand_a_sign, F16_operand_b_sign, F16_a_norm, F16_b_subnorm, + /* a.EXP > b.EXP*/ F16_frac_compare, F16_result_fmt; + + B19_F16__subnorm_x_norm: cross FP_compare_ops, F16_operand_a_sign, F16_operand_b_sign, F16_a_norm, F16_b_subnorm, + /* a.EXP < b.EXP*/ F16_frac_compare, F16_result_fmt; + + B19_F16__subnorm_x_subnorm: cross FP_compare_ops, F16_operand_a_sign, F16_operand_b_sign, F16_a_norm, F16_b_subnorm, + F16_exp_compare, F16_frac_compare, F16_result_fmt; + + B19_F16__zero_x_norm: cross FP_compare_ops, F16_operand_a_sign, F16_operand_b_sign, F16_a_zero, F16_b_norm, + /* a.EXP < b.EXP*/ F16_frac_LTE, F16_result_fmt; + + B19_F16__norm_x_zero: cross FP_compare_ops, F16_operand_a_sign, F16_operand_b_sign, F16_a_norm, F16_b_zero, + /* a.EXP > b.EXP*/ F16_frac_GTE, F16_result_fmt; + + B19_F16__subnorm_x_zero: cross FP_compare_ops, F16_operand_a_sign, F16_operand_b_sign, F16_a_subnorm, F16_b_zero, + /* a.EXP < b.EXP*/ F16_frac_LT, F16_result_fmt; + + B19_F16__zero_x_subnorm: cross FP_compare_ops, F16_operand_a_sign, F16_operand_b_sign, F16_a_zero, F16_b_subnorm, + /* a.EXP > b.EXP*/ F16_frac_GT, F16_result_fmt; + + B19_F16__zero_x_zero: cross FP_compare_ops, F16_operand_a_sign, F16_operand_b_sign, F16_a_zero, F16_b_zero, + /* a.EXP = b.EXP*/ /* a.FRAC = b.FRAC*/ F16_result_fmt; + `endif // COVER_F16 + + + `ifdef COVER_BF16 + B19_BF16__norm_x_norm: cross FP_compare_ops, BF16_operand_a_sign, BF16_operand_b_sign, BF16_a_norm, BF16_b_norm, + BF16_exp_compare, BF16_frac_compare, BF16_result_fmt; + + B19_BF16__norm_x_subnorm: cross FP_compare_ops, BF16_operand_a_sign, BF16_operand_b_sign, BF16_a_norm, BF16_b_subnorm, + /* a.EXP > b.EXP*/ BF16_frac_compare, BF16_result_fmt; + + B19_BF16__subnorm_x_norm: cross FP_compare_ops, BF16_operand_a_sign, BF16_operand_b_sign, BF16_a_norm, BF16_b_subnorm, + /* a.EXP < b.EXP*/ BF16_frac_compare, BF16_result_fmt; + + B19_BF16__subnorm_x_subnorm: cross FP_compare_ops, BF16_operand_a_sign, BF16_operand_b_sign, BF16_a_norm, BF16_b_subnorm, + BF16_exp_compare, BF16_frac_compare, BF16_result_fmt; + + B19_BF16__zero_x_norm: cross FP_compare_ops, BF16_operand_a_sign, BF16_operand_b_sign, BF16_a_zero, BF16_b_norm, + /* a.EXP < b.EXP*/ BF16_frac_LTE, BF16_result_fmt; + + B19_BF16__norm_x_zero: cross FP_compare_ops, BF16_operand_a_sign, BF16_operand_b_sign, BF16_a_norm, BF16_b_zero, + /* a.EXP > b.EXP*/ BF16_frac_GTE, BF16_result_fmt; + + B19_BF16__subnorm_x_zero: cross FP_compare_ops, BF16_operand_a_sign, BF16_operand_b_sign, BF16_a_subnorm, BF16_b_zero, + /* a.EXP < b.EXP*/ BF16_frac_LT, BF16_result_fmt; + + B19_BF16__zero_x_subnorm: cross FP_compare_ops, BF16_operand_a_sign, BF16_operand_b_sign, BF16_a_zero, BF16_b_subnorm, + /* a.EXP > b.EXP*/ BF16_frac_GT, BF16_result_fmt; + + B19_BF16__zero_x_zero: cross FP_compare_ops, BF16_operand_a_sign, BF16_operand_b_sign, BF16_a_zero, BF16_b_zero, + /* a.EXP = b.EXP*/ /* a.FRAC = b.FRAC*/ BF16_result_fmt; + `endif // COVER_BF16 + + + `ifdef COVER_F32 + B19_F32__norm_x_norm: cross FP_compare_ops, F32_operand_a_sign, F32_operand_b_sign, F32_a_norm, F32_b_norm, + F32_exp_compare, F32_frac_compare, F32_result_fmt; + + B19_F32__norm_x_subnorm: cross FP_compare_ops, F32_operand_a_sign, F32_operand_b_sign, F32_a_norm, F32_b_subnorm, + /* a.EXP > b.EXP*/ F32_frac_compare, F32_result_fmt; + + B19_F32__subnorm_x_norm: cross FP_compare_ops, F32_operand_a_sign, F32_operand_b_sign, F32_a_norm, F32_b_subnorm, + /* a.EXP < b.EXP*/ F32_frac_compare, F32_result_fmt; + + B19_F32__subnorm_x_subnorm: cross FP_compare_ops, F32_operand_a_sign, F32_operand_b_sign, F32_a_norm, F32_b_subnorm, + F32_exp_compare, F32_frac_compare, F32_result_fmt; + + B19_F32__zero_x_norm: cross FP_compare_ops, F32_operand_a_sign, F32_operand_b_sign, F32_a_zero, F32_b_norm, + /* a.EXP < b.EXP*/ F32_frac_LTE, F32_result_fmt; + + B19_F32__norm_x_zero: cross FP_compare_ops, F32_operand_a_sign, F32_operand_b_sign, F32_a_norm, F32_b_zero, + /* a.EXP > b.EXP*/ F32_frac_GTE, F32_result_fmt; + + B19_F32__subnorm_x_zero: cross FP_compare_ops, F32_operand_a_sign, F32_operand_b_sign, F32_a_subnorm, F32_b_zero, + /* a.EXP < b.EXP*/ F32_frac_LT, F32_result_fmt; + + B19_F32__zero_x_subnorm: cross FP_compare_ops, F32_operand_a_sign, F32_operand_b_sign, F32_a_zero, F32_b_subnorm, + /* a.EXP > b.EXP*/ F32_frac_GT, F32_result_fmt; + + B19_F32__zero_x_zero: cross FP_compare_ops, F32_operand_a_sign, F32_operand_b_sign, F32_a_zero, F32_b_zero, + /* a.EXP = b.EXP*/ /* a.FRAC = b.FRAC*/ F32_result_fmt; + `endif // COVER_F32 + + + `ifdef COVER_F64 + B19_F64__norm_x_norm: cross FP_compare_ops, F64_operand_a_sign, F64_operand_b_sign, F64_a_norm, F64_b_norm, + F64_exp_compare, F64_frac_compare, F64_result_fmt; + + B19_F64__norm_x_subnorm: cross FP_compare_ops, F64_operand_a_sign, F64_operand_b_sign, F64_a_norm, F64_b_subnorm, + /* a.EXP > b.EXP*/ F64_frac_compare, F64_result_fmt; + + B19_F64__subnorm_x_norm: cross FP_compare_ops, F64_operand_a_sign, F64_operand_b_sign, F64_a_norm, F64_b_subnorm, + /* a.EXP < b.EXP*/ F64_frac_compare, F64_result_fmt; + + B19_F64__subnorm_x_subnorm: cross FP_compare_ops, F64_operand_a_sign, F64_operand_b_sign, F64_a_norm, F64_b_subnorm, + F64_exp_compare, F64_frac_compare, F64_result_fmt; + + B19_F64__zero_x_norm: cross FP_compare_ops, F64_operand_a_sign, F64_operand_b_sign, F64_a_zero, F64_b_norm, + /* a.EXP < b.EXP*/ F64_frac_LTE, F64_result_fmt; + + B19_F64__norm_x_zero: cross FP_compare_ops, F64_operand_a_sign, F64_operand_b_sign, F64_a_norm, F64_b_zero, + /* a.EXP > b.EXP*/ F64_frac_GTE, F64_result_fmt; + + B19_F64__subnorm_x_zero: cross FP_compare_ops, F64_operand_a_sign, F64_operand_b_sign, F64_a_subnorm, F64_b_zero, + /* a.EXP < b.EXP*/ F64_frac_LT, F64_result_fmt; + + B19_F64__zero_x_subnorm: cross FP_compare_ops, F64_operand_a_sign, F64_operand_b_sign, F64_a_zero, F64_b_subnorm, + /* a.EXP > b.EXP*/ F64_frac_GT, F64_result_fmt; + + B19_F64__zero_x_zero: cross FP_compare_ops, F64_operand_a_sign, F64_operand_b_sign, F64_a_zero, F64_b_zero, + /* a.EXP = b.EXP*/ /* a.FRAC = b.FRAC*/ F64_result_fmt; + `endif // COVER_F64 + + + `ifdef COVER_F128 + B19_F128__norm_x_norm: cross FP_compare_ops, F128_operand_a_sign, F128_operand_b_sign, F128_a_norm, F128_b_norm, + F128_exp_compare, F128_frac_compare, F128_result_fmt; + + B19_F128__norm_x_subnorm: cross FP_compare_ops, F128_operand_a_sign, F128_operand_b_sign, F128_a_norm, F128_b_subnorm, + /* a.EXP > b.EXP*/ F128_frac_compare, F128_result_fmt; + + B19_F128__subnorm_x_norm: cross FP_compare_ops, F128_operand_a_sign, F128_operand_b_sign, F128_a_norm, F128_b_subnorm, + /* a.EXP < b.EXP*/ F128_frac_compare, F128_result_fmt; + + B19_F128__subnorm_x_subnorm: cross FP_compare_ops, F128_operand_a_sign, F128_operand_b_sign, F128_a_norm, F128_b_subnorm, + F128_exp_compare, F128_frac_compare, F128_result_fmt; + + B19_F128__zero_x_norm: cross FP_compare_ops, F128_operand_a_sign, F128_operand_b_sign, F128_a_zero, F128_b_norm, + /* a.EXP < b.EXP*/ F128_frac_LTE, F128_result_fmt; + + B19_F128__norm_x_zero: cross FP_compare_ops, F128_operand_a_sign, F128_operand_b_sign, F128_a_norm, F128_b_zero, + /* a.EXP > b.EXP*/ F128_frac_GTE, F128_result_fmt; + + B19_F128__subnorm_x_zero: cross FP_compare_ops, F128_operand_a_sign, F128_operand_b_sign, F128_a_subnorm, F128_b_zero, + /* a.EXP < b.EXP*/ F128_frac_LT, F128_result_fmt; + + B19_F128__zero_x_subnorm: cross FP_compare_ops, F128_operand_a_sign, F128_operand_b_sign, F128_a_zero, F128_b_subnorm, + /* a.EXP > b.EXP*/ F128_frac_GT, F128_result_fmt; + + B19_F128__zero_x_zero: cross FP_compare_ops, F128_operand_a_sign, F128_operand_b_sign, F128_a_zero, F128_b_zero, + /* a.EXP = b.EXP*/ /* a.FRAC = b.FRAC*/ F128_result_fmt; + `endif // COVER_F128 + + +endgroup diff --git a/coverage/covergroups/B19.svh b/coverage/covergroups/B19.svh index d3e7f46..60b7384 100644 --- a/coverage/covergroups/B19.svh +++ b/coverage/covergroups/B19.svh @@ -634,10 +634,10 @@ covergroup B19_cg (virtual coverfloat_interface CFI); B19_F16__norm_x_subnorm: cross FP_compare_ops, F16_operand_a_sign, F16_operand_b_sign, F16_a_norm, F16_b_subnorm, /* a.EXP > b.EXP*/ F16_frac_compare, F16_result_fmt; - B19_F16__subnorm_x_norm: cross FP_compare_ops, F16_operand_a_sign, F16_operand_b_sign, F16_a_norm, F16_b_subnorm, + B19_F16__subnorm_x_norm: cross FP_compare_ops, F16_operand_a_sign, F16_operand_b_sign, F16_a_subnorm, F16_b_norm, /* a.EXP < b.EXP*/ F16_frac_compare, F16_result_fmt; - B19_F16__subnorm_x_subnorm: cross FP_compare_ops, F16_operand_a_sign, F16_operand_b_sign, F16_a_norm, F16_b_subnorm, + B19_F16__subnorm_x_subnorm: cross FP_compare_ops, F16_operand_a_sign, F16_operand_b_sign, F16_a_subnorm, F16_b_subnorm, F16_exp_compare, F16_frac_compare, F16_result_fmt; B19_F16__zero_x_norm: cross FP_compare_ops, F16_operand_a_sign, F16_operand_b_sign, F16_a_zero, F16_b_norm, @@ -647,10 +647,10 @@ covergroup B19_cg (virtual coverfloat_interface CFI); /* a.EXP > b.EXP*/ F16_frac_GTE, F16_result_fmt; B19_F16__subnorm_x_zero: cross FP_compare_ops, F16_operand_a_sign, F16_operand_b_sign, F16_a_subnorm, F16_b_zero, - /* a.EXP < b.EXP*/ F16_frac_LT, F16_result_fmt; + /* a.EXP < b.EXP*/ F16_frac_GTE, F16_result_fmt; B19_F16__zero_x_subnorm: cross FP_compare_ops, F16_operand_a_sign, F16_operand_b_sign, F16_a_zero, F16_b_subnorm, - /* a.EXP > b.EXP*/ F16_frac_GT, F16_result_fmt; + /* a.EXP > b.EXP*/ F16_frac_LTE, F16_result_fmt; B19_F16__zero_x_zero: cross FP_compare_ops, F16_operand_a_sign, F16_operand_b_sign, F16_a_zero, F16_b_zero, /* a.EXP = b.EXP*/ /* a.FRAC = b.FRAC*/ F16_result_fmt; @@ -664,10 +664,10 @@ covergroup B19_cg (virtual coverfloat_interface CFI); B19_BF16__norm_x_subnorm: cross FP_compare_ops, BF16_operand_a_sign, BF16_operand_b_sign, BF16_a_norm, BF16_b_subnorm, /* a.EXP > b.EXP*/ BF16_frac_compare, BF16_result_fmt; - B19_BF16__subnorm_x_norm: cross FP_compare_ops, BF16_operand_a_sign, BF16_operand_b_sign, BF16_a_norm, BF16_b_subnorm, + B19_BF16__subnorm_x_norm: cross FP_compare_ops, BF16_operand_a_sign, BF16_operand_b_sign, BF16_a_subnorm, BF16_b_norm, /* a.EXP < b.EXP*/ BF16_frac_compare, BF16_result_fmt; - B19_BF16__subnorm_x_subnorm: cross FP_compare_ops, BF16_operand_a_sign, BF16_operand_b_sign, BF16_a_norm, BF16_b_subnorm, + B19_BF16__subnorm_x_subnorm: cross FP_compare_ops, BF16_operand_a_sign, BF16_operand_b_sign, BF16_a_subnorm, BF16_b_subnorm, BF16_exp_compare, BF16_frac_compare, BF16_result_fmt; B19_BF16__zero_x_norm: cross FP_compare_ops, BF16_operand_a_sign, BF16_operand_b_sign, BF16_a_zero, BF16_b_norm, @@ -677,10 +677,10 @@ covergroup B19_cg (virtual coverfloat_interface CFI); /* a.EXP > b.EXP*/ BF16_frac_GTE, BF16_result_fmt; B19_BF16__subnorm_x_zero: cross FP_compare_ops, BF16_operand_a_sign, BF16_operand_b_sign, BF16_a_subnorm, BF16_b_zero, - /* a.EXP < b.EXP*/ BF16_frac_LT, BF16_result_fmt; + /* a.EXP < b.EXP*/ BF16_frac_GTE, BF16_result_fmt; B19_BF16__zero_x_subnorm: cross FP_compare_ops, BF16_operand_a_sign, BF16_operand_b_sign, BF16_a_zero, BF16_b_subnorm, - /* a.EXP > b.EXP*/ BF16_frac_GT, BF16_result_fmt; + /* a.EXP > b.EXP*/ BF16_frac_LTE, BF16_result_fmt; B19_BF16__zero_x_zero: cross FP_compare_ops, BF16_operand_a_sign, BF16_operand_b_sign, BF16_a_zero, BF16_b_zero, /* a.EXP = b.EXP*/ /* a.FRAC = b.FRAC*/ BF16_result_fmt; @@ -694,10 +694,10 @@ covergroup B19_cg (virtual coverfloat_interface CFI); B19_F32__norm_x_subnorm: cross FP_compare_ops, F32_operand_a_sign, F32_operand_b_sign, F32_a_norm, F32_b_subnorm, /* a.EXP > b.EXP*/ F32_frac_compare, F32_result_fmt; - B19_F32__subnorm_x_norm: cross FP_compare_ops, F32_operand_a_sign, F32_operand_b_sign, F32_a_norm, F32_b_subnorm, + B19_F32__subnorm_x_norm: cross FP_compare_ops, F32_operand_a_sign, F32_operand_b_sign, F32_a_subnorm, F32_b_norm, /* a.EXP < b.EXP*/ F32_frac_compare, F32_result_fmt; - B19_F32__subnorm_x_subnorm: cross FP_compare_ops, F32_operand_a_sign, F32_operand_b_sign, F32_a_norm, F32_b_subnorm, + B19_F32__subnorm_x_subnorm: cross FP_compare_ops, F32_operand_a_sign, F32_operand_b_sign, F32_a_subnorm, F32_b_subnorm, F32_exp_compare, F32_frac_compare, F32_result_fmt; B19_F32__zero_x_norm: cross FP_compare_ops, F32_operand_a_sign, F32_operand_b_sign, F32_a_zero, F32_b_norm, @@ -707,10 +707,10 @@ covergroup B19_cg (virtual coverfloat_interface CFI); /* a.EXP > b.EXP*/ F32_frac_GTE, F32_result_fmt; B19_F32__subnorm_x_zero: cross FP_compare_ops, F32_operand_a_sign, F32_operand_b_sign, F32_a_subnorm, F32_b_zero, - /* a.EXP < b.EXP*/ F32_frac_LT, F32_result_fmt; + /* a.EXP < b.EXP*/ F32_frac_GTE, F32_result_fmt; B19_F32__zero_x_subnorm: cross FP_compare_ops, F32_operand_a_sign, F32_operand_b_sign, F32_a_zero, F32_b_subnorm, - /* a.EXP > b.EXP*/ F32_frac_GT, F32_result_fmt; + /* a.EXP > b.EXP*/ F32_frac_LTE, F32_result_fmt; B19_F32__zero_x_zero: cross FP_compare_ops, F32_operand_a_sign, F32_operand_b_sign, F32_a_zero, F32_b_zero, /* a.EXP = b.EXP*/ /* a.FRAC = b.FRAC*/ F32_result_fmt; @@ -724,10 +724,10 @@ covergroup B19_cg (virtual coverfloat_interface CFI); B19_F64__norm_x_subnorm: cross FP_compare_ops, F64_operand_a_sign, F64_operand_b_sign, F64_a_norm, F64_b_subnorm, /* a.EXP > b.EXP*/ F64_frac_compare, F64_result_fmt; - B19_F64__subnorm_x_norm: cross FP_compare_ops, F64_operand_a_sign, F64_operand_b_sign, F64_a_norm, F64_b_subnorm, + B19_F64__subnorm_x_norm: cross FP_compare_ops, F64_operand_a_sign, F64_operand_b_sign, F64_a_subnorm, F64_b_norm, /* a.EXP < b.EXP*/ F64_frac_compare, F64_result_fmt; - B19_F64__subnorm_x_subnorm: cross FP_compare_ops, F64_operand_a_sign, F64_operand_b_sign, F64_a_norm, F64_b_subnorm, + B19_F64__subnorm_x_subnorm: cross FP_compare_ops, F64_operand_a_sign, F64_operand_b_sign, F64_a_subnorm, F64_b_subnorm, F64_exp_compare, F64_frac_compare, F64_result_fmt; B19_F64__zero_x_norm: cross FP_compare_ops, F64_operand_a_sign, F64_operand_b_sign, F64_a_zero, F64_b_norm, @@ -737,10 +737,10 @@ covergroup B19_cg (virtual coverfloat_interface CFI); /* a.EXP > b.EXP*/ F64_frac_GTE, F64_result_fmt; B19_F64__subnorm_x_zero: cross FP_compare_ops, F64_operand_a_sign, F64_operand_b_sign, F64_a_subnorm, F64_b_zero, - /* a.EXP < b.EXP*/ F64_frac_LT, F64_result_fmt; + /* a.EXP < b.EXP*/ F64_frac_GTE, F64_result_fmt; B19_F64__zero_x_subnorm: cross FP_compare_ops, F64_operand_a_sign, F64_operand_b_sign, F64_a_zero, F64_b_subnorm, - /* a.EXP > b.EXP*/ F64_frac_GT, F64_result_fmt; + /* a.EXP > b.EXP*/ F64_frac_LTE, F64_result_fmt; B19_F64__zero_x_zero: cross FP_compare_ops, F64_operand_a_sign, F64_operand_b_sign, F64_a_zero, F64_b_zero, /* a.EXP = b.EXP*/ /* a.FRAC = b.FRAC*/ F64_result_fmt; @@ -754,10 +754,10 @@ covergroup B19_cg (virtual coverfloat_interface CFI); B19_F128__norm_x_subnorm: cross FP_compare_ops, F128_operand_a_sign, F128_operand_b_sign, F128_a_norm, F128_b_subnorm, /* a.EXP > b.EXP*/ F128_frac_compare, F128_result_fmt; - B19_F128__subnorm_x_norm: cross FP_compare_ops, F128_operand_a_sign, F128_operand_b_sign, F128_a_norm, F128_b_subnorm, + B19_F128__subnorm_x_norm: cross FP_compare_ops, F128_operand_a_sign, F128_operand_b_sign, F128_a_subnorm, F128_b_norm, /* a.EXP < b.EXP*/ F128_frac_compare, F128_result_fmt; - B19_F128__subnorm_x_subnorm: cross FP_compare_ops, F128_operand_a_sign, F128_operand_b_sign, F128_a_norm, F128_b_subnorm, + B19_F128__subnorm_x_subnorm: cross FP_compare_ops, F128_operand_a_sign, F128_operand_b_sign, F128_a_subnorm, F128_b_subnorm, F128_exp_compare, F128_frac_compare, F128_result_fmt; B19_F128__zero_x_norm: cross FP_compare_ops, F128_operand_a_sign, F128_operand_b_sign, F128_a_zero, F128_b_norm, @@ -767,10 +767,10 @@ covergroup B19_cg (virtual coverfloat_interface CFI); /* a.EXP > b.EXP*/ F128_frac_GTE, F128_result_fmt; B19_F128__subnorm_x_zero: cross FP_compare_ops, F128_operand_a_sign, F128_operand_b_sign, F128_a_subnorm, F128_b_zero, - /* a.EXP < b.EXP*/ F128_frac_LT, F128_result_fmt; + /* a.EXP < b.EXP*/ F128_frac_GTE, F128_result_fmt; B19_F128__zero_x_subnorm: cross FP_compare_ops, F128_operand_a_sign, F128_operand_b_sign, F128_a_zero, F128_b_subnorm, - /* a.EXP > b.EXP*/ F128_frac_GT, F128_result_fmt; + /* a.EXP > b.EXP*/ F128_frac_LTE, F128_result_fmt; B19_F128__zero_x_zero: cross FP_compare_ops, F128_operand_a_sign, F128_operand_b_sign, F128_a_zero, F128_b_zero, /* a.EXP = b.EXP*/ /* a.FRAC = b.FRAC*/ F128_result_fmt; diff --git a/docs/B19.adoc b/docs/B19.adoc new file mode 100644 index 0000000..d90b22a --- /dev/null +++ b/docs/B19.adoc @@ -0,0 +1,907 @@ += B19 Compare: Different Input Fields Relations +:toc: +:toclevels: 3 +:sectnums: +:stem: latexmath + +== Overview + +*Aharoni et al.* + +This model checks various possible differences between two inputs. A test-case will be created for each combination of the following table: + +[cols="1,1,1,1",options="header"] +|=== +| First Input | Second Input | Difference between exponents | Difference between significands + +| +Normal +| +Normal +| > 0 +| > 0 + +| -Normal +| -Normal +| = 0 +| = 0 + +| +SubNormal +| +SubNormal +| < 0 +| < 0 + +| -SubNormal +| -SubNormal +| +| + +| 0 +| 0 +| +| +|=== + +*Number of tests:* ~9 E 2 + +*Precisions supported:* BF_16, FP_16, FP_32, FP_64, FP_128 + +*Operations supported:* OP_FEQ, OP_FLT, OP_FLE, OP_MIN, OP_MAX + + +== Implementation + +=== Definitions + +[source] +---- +bias = (2 ^ (exp_bits - 1)) - 1 +max_bexp = (2 ^ exp_bits) - 1 (all-ones; encodes NaN/Inf are not a valid normal) +min_norm_bexp = 1 (smallest valid normal biased exponent) +max_norm_bexp = max_bexp - 1 (largest valid normal biased exponent) +frac_bits = sig_bits - 1 (stored mantissa width, excludes implicit leading 1) +frac_max = (2 ^ frac_bits) - 1 + +all zeros = fraction with all zeros (the frac of MinNorm) +all ones = fraction with all ones (the frac of MaxNorm) +00..001 = fraction where the LSB is one = 1 (the frac of MinSubNorm) +10000..000 = fraction with only the MSB set to 1 +any frac = a randomized value in the fraction field, representative mid-range fraction (all zeros < any frac < all ones) +any exp = a randomized exponent value, representative of mid-range exponents (min_norm_bexp < any exp < max_norm_bexp) +significand = mantissa = fraction (interchangable terms) +---- + +==== Exponent interpretation for subnormals + +A subnormal number has a fixed biased exponent field of 0, but its _effective exponent_ — the exponent of its leading significant bit — depends on the position of the leading 1 in the frac field: + +Let stem:[L_z] be the number of leading zeros in the fraction field before the first 1. The effective exponent can be calculated as: + +[source] +---- +eff_exp(frac) = -bias - L +---- +For example, suppose we are given two FP16 subnormal numbers (where stem:[\text{bias} = 15] and stem:[\text{frac_bits} = 10]): + +* `0 00000 0100100000` <- Has 1 leading zero in the fraction (stem:[L_z = 1]). Its effective exponent is stem:[-\text{bias} - 1 = -16]. +* `0 00000 0000010100` <- Has 5 leading zeros in the fraction (stem:[L_z = 5]). Its effective exponent is stem:[-\text{bias} - 5 = -20]. + +This means two subnormals can have exp >, =, or < relationships based on their fraction fields. A subnormal with a higher leading-1 position has both a larger effective exponent AND a larger fraction value, so exp > always implies significands > and exponents < always implies significands <. Only exponents = leaves significands free. + + +=== General Procedure + +For each (format, operation, case), the generator iterates over the achievable (exp_rel, sig_rel) cells. For each cell it enumerates: + +* All 4 sign combinations: (+/+), (+/-), (-/+), (-/-) + +The frac field values are deterministic constants derived from the format (all zeros, all ones, 00..001, 10000..000, any_frac). A seeded random is used only for the bits of 'any frac' and 'any exp' where randomisation is appropriate (see implementation). + + +== Test Case Analysis + +=== Case 1: ±Normal × ±Normal + +[cols="1,1,1,1,1,1",options="header"] +|=== +| Exp | Frac | Exp_input_1 | Exp_input_2 | F_input_1 | F_input_2 + +| > +| > +| max_norm_bexp +| any exp +| any frac +| all zeros + +| > +| < +| max_norm_bexp +| any exp +| all zeros +| any frac + +| > +| = +| max_norm_bexp +| any exp +| all zeros +| all zeros + +| < +| > +| min_norm_bexp +| any exp +| all ones +| any frac + +| < +| < +| min_norm_bexp +| any exp +| any frac +| all ones + +| < +| = +| min_norm_bexp +| any exp +| all ones +| all ones + +| = +| > +| any exp +| any exp (same) +| all ones +| all zeros + +| = +| < +| any exp +| any exp (same) +| all zeros +| all ones + +| = +| = +| any exp +| any exp (same) +| all zeros +| all zeros +|=== + +*Total per precision:* 9 cells × 4 sign combos = **36** + +--- + +=== Case 2: ±Normal × ±SubNormal + +[cols="1,1,1,1,1,1",options="header"] +|=== +| Exp | Frac | Exp_input_1 | Exp_input_2 | F_input_1 | F_input_2 + +| > +| > +| any exp +| 0s +| any frac +| 00..001 + +| > +| < +| any exp +| 0s +| 00..001 +| any frac + +| > +| = +| any exp +| 0s +| all zeros +| 10...000 + +| < +| > +| impossible +| +| +| + +| < +| < +| impossible +| +| +| + +| < +| = +| impossible +| +| +| + +| = +| > +| impossible +| +| +| + +| = +| < +| impossible +| +| +| + +| = +| = +| impossible +| +| +| +|=== + +*Total per precision:* 3 cells × 4 sign combos = **12** + +==== Impossibility reasoning + +A normal number has biased exponent ≥ 1, while a subnormal has biased exponent = 0. Therefore exp < (normal < subnormal) and exp = are structurally impossible — *only exp > is achievable*. + +--- + +=== Case 3: ±SubNormal × ±Normal + +[cols="1,1,1,1,1,1",options="header"] +|=== +| Exp | Frac | Exp_input_1 | Exp_input_2 | F_input_1 | F_input_2 + +| > +| > +| impossible +| +| +| + +| > +| < +| impossible +| +| +| + +| > +| = +| impossible +| +| +| + +| < +| > +| 0s +| any exp +| all ones +| all zeros + +| < +| < +| 0s +| any exp +| any frac +| all ones + +| < +| = +| 0s +| any exp +| 10...000 +| all zeros + +| = +| > +| impossible +| +| +| + +| = +| < +| impossible +| +| +| + +| = +| = +| impossible +| +| +| +|=== + +*Total per precision:* 3 cells × 4 sign combos = **12** + +==== Impossibility reasoning + +Symmetric to Case 2. The subnormal's effective exponent is always strictly less than the normal's, so exp > (subnormal > normal) and exp = are structurally impossible — *only exp < is achievable*. + +--- + +=== Case 4: ±SubNormal × ±SubNormal + +[cols="1,1,1,1,1,1",options="header"] +|=== +| Exp | Frac | Exp_input_1 | Exp_input_2 | F_input_1 | F_input_2 + +| > +| > +| 0s +| 0s +| any frac +| 00..001 + +| > +| < +| impossible +| +| +| + +| > +| = +| impossible +| +| +| + +| < +| > +| impossible +| +| +| + +| < +| < +| 0s +| 0s +| 00..001 +| any frac + +| < +| = +| impossible +| +| +| + +| = +| > +| 0s +| 0s +| all ones +| 10000..000 + +| = +| < +| 0s +| 0s +| 10000..000 +| all ones + +| = +| = +| 0s +| 0s +| any frac +| any frac +|=== + +*Total per precision:* 5 cells × 4 sign combos = **20** (no exp axis — both bexp fields are always 0) + +==== Impossibility reasoning + +Both subnormals have a stored biased exponent field of 0. Their _effective_ exponents are determined by the position of the leading 1 in the frac field. A higher leading-1 position means a larger effective exponent AND a larger frac value simultaneously, because the higher bit dominates all lower bits. This creates a strict coupling: + +* *exp > forces sig >*: if eff_exp1 > eff_exp2, then the leading-1 of frac1 is at a higher bit position than the leading-1 of frac2, which means frac1 > frac2 necessarily. Therefore exp > sig < and exp > sig = are impossible. +* *exp < forces sig <*: symmetric reasoning. exp < sig > and exp < sig = are impossible. +* *exp = leaves sig free*: if both fracs have their leading-1 at the same bit position, eff_exp1 = eff_exp2. The lower bits then determine sig freely: all ones (1111..1) > 10000..000 (1000..0) for sig >, reversed for sig <, and identical fracs for sig =. + +The cells (>, <), (>, =), (<, >), (<, =) are impossible except the five rows shown. + +--- + +=== Case 5: ±Zero × ±Normal + +[cols="1,1,1,1,1,1",options="header"] +|=== +| Exp | Frac | Exp_input_1 | Exp_input_2 | F_input_1 | F_input_2 + +| > +| > +| impossible +| +| +| + +| > +| < +| impossible +| +| +| + +| > +| = +| impossible +| +| +| + +| < +| > +| impossible +| +| +| + +| < +| < +| 0s +| any exp +| all zeros +| any frac + +| < +| = +| 0s +| any exp +| all zeros +| all zeros + +| = +| > +| impossible +| +| +| + +| = +| < +| impossible +| +| +| + +| = +| = +| impossible +| +| +| +|=== + +*Total per precision:* 2 cells × 4 sign combos = **8** + +==== Impossibility reasoning + +* *exp > and exp = impossible:* Zero has biased exponent 0 and frac 0. A normal number has biased exponent ≥ 1. Since zero's exponent field is 0 and any normal's is ≥ 1, the zero is always numerically smaller in exponent. exp > (zero > normal) and exp = are structurally impossible. + +* *exp < sig > impossible:* Zero's frac is fixed at 0. For sig > we would need frac1 (= 0) > frac2. Since frac2 ≥ 0 always, this is impossible — 0 cannot be greater than anything. + +* *exp < sig < and exp < sig = are achievable:* frac2 = any_frac > 0 gives sig <; frac2 = all zeros gives frac1 = frac2 = 0 giving sig =. + +--- + +=== Case 6: ±Normal × ±Zero + +[cols="1,1,1,1,1,1",options="header"] +|=== +| Exp | Frac | Exp_input_1 | Exp_input_2 | F_input_1 | F_input_2 + +| > +| > +| any exp +| 0s +| any frac +| all zeros + +| > +| < +| impossible +| +| +| + +| > +| = +| any exp +| 0s +| all zeros +| all zeros + +| < +| > +| impossible +| +| +| + +| < +| < +| impossible +| +| +| + +| < +| = +| impossible +| +| +| + +| = +| > +| impossible +| +| +| + +| = +| < +| impossible +| +| +| + +| = +| = +| impossible +| +| +| +|=== + +*Total per precision:* 2 cells × 4 sign combos = **8** + +==== Impossibility reasoning + +* *exp < and exp = impossible:* Symmetric to Case 5. A normal always has biased exponent ≥ 1 while zero has biased exponent 0, so exp < (normal < zero) and exp = are structurally impossible. + +* *exp > sig < impossible:* Zero's frac is fixed at 0. For sig < we would need frac1 < frac2 (= 0). Since frac1 ≥ 0 always, frac1 < 0 is impossible. + +* *exp > sig > achievable:* F_input_1 = any_frac > 0 = F_input_2. Correct. + +* *exp > sig = achievable:* Both fracs must be equal. Since frac2 = 0 (zero's frac is fixed), frac1 must also be 0. So F_input_1 = all zeros, not any_frac. Both are 0, giving sig =. + +--- + +=== Case 7: ±Zero × ±Subnormal + +[cols="1,1,1,1,1,1",options="header"] +|=== +| Exp | Frac | Exp_input_1 | Exp_input_2 | F_input_1 | F_input_2 + +| > +| > +| impossible +| +| +| + +| > +| < +| 0s +| 0s +| all zeros +| any frac + +| > +| = +| 0s +| 0s +| all zeros +| 10...000 + +| < +| > +| impossible +| +| +| + +| < +| < +| impossible +| +| +| + +| < +| = +| impossible +| +| +| + +| = +| > +| impossible +| +| +| + +| = +| < +| impossible +| +| +| + +| = +| = +| impossible +| +| +|=== + +*Total per precision:* 2 cells × 4 sign combos = **8** + +==== Impossibility reasoning + +Subnormal numbers have effective exponents that are strictly negative, while zero has a biased exponent of 0. Consequently, exp_zero > exp_subnormal is the only achievable relationship. Given this constraint, the zero's mantissa is fixed at all zeros, which necessitates the subnormal's mantissa to be non-zero for any comparison. Thus, the sole valid scenario is: exp_zero > exp_subnormal with frac_zero < frac_subnormal. + +--- + +=== Case 8: ±Subnormal × ±Zero + +[cols="1,1,1,1,1,1",options="header"] +|=== +| Exp | Frac | Exp_input_1 | Exp_input_2 | F_input_1 | F_input_2 + +| > +| > +| impossible +| +| +| + +| > +| < +| impossible +| +| +| + +| > +| = +| impossible +| +| +| + +| < +| > +| 0s +| 0s +| any frac +| all zeros + +| < +| < +| impossible +| +| +| + +| < +| = +| 0s +| 0s +| 10...000 +| all zeros + +| = +| > +| impossible +| +| +| + +| = +| < +| impossible +| +| +| + +| = +| = +| impossible +| +| +|=== + +*Total per precision:* 2 cell × 4 sign combos = **8** + +==== Impossibility reasoning + +By symmetry with Case 7, with the same constraints on exponents and mantissas, only the achievable cell differs due to the swapped operand positions. + +--- + +=== Case 9: ±Zero × ±Zero + +[cols="1,1,1,1,1,1",options="header"] +|=== +| Exp | Frac | Exp_input_1 | Exp_input_2 | F_input_1 | F_input_2 + +| > +| > +| impossible +| +| +| + +| > +| < +| impossible +| +| +| + +| > +| = +| impossible +| +| +| + +| < +| > +| impossible +| +| +| + +| < +| < +| impossible +| +| +| + +| < +| = +| impossible +| +| +| + +| = +| > +| impossible +| +| +| + +| = +| < +| impossible +| +| +| + +| = +| = +| 0s +| 0s +| all zeros +| all zeros +|=== + +*Total per precision:* 1 cell × 4 sign combos = **4** + +==== Impossibility reasoning + +Both operands are zero: bexp = 0 and frac = 0 are fixed for both. The exp fields are identical (0 = 0), so exp > and exp < are impossible — only exp = is achievable. The frac fields are both fixed at 0, so frac1 = frac2 = 0 always — sig > and sig < are impossible. *Only (exp =, sig =) is achievable.* + +The 4 vectors come from the 4 sign combinations: (+0,+0), (+0,−0), (−0,+0), (−0,−0). + +--- + +== Test Count Breakdown + +[cols="1,2,2,1,1",options="header"] +|=== +| Case | Category pair | Achievable cells | Sign axis | Per (fmt, op) + +| 1 +| Normal × Normal +| 9 +| × 4 +| 36 + +| 2 +| Normal × SubNormal +| 3 +| × 4 +| 12 + +| 3 +| SubNormal × Normal +| 3 +| × 4 +| 12 + +| 4 +| SubNormal × SubNormal +| 5 +| × 4 +| 20 + +| 5 +| Zero × Normal +| 2 +| × 4 +| 8 + +| 6 +| Normal × Zero +| 2 +| × 4 +| 8 + +| 7 +| Zero × Subnormal +| 2 +| × 4 +| 8 + +| 8 +| Subnormal × Zero +| 2 +| × 4 +| 8 + +| 9 +| Zero × Zero +| 1 +| × 4 +| 4 + +| +| +| +| *Total per (fmt, op):* +| *116* +|=== + +=== Grand Total Breakdown + +[cols="2,2",options="header"] +|=== +| Format | Total vectors + +| BF_16 +| 116 per op × 5 ops = 580 + +| FP_16 +| 116 per op × 5 ops = 580 + +| FP_32 +| 116 per op × 5 ops = 580 + +| FP_64 +| 116 per op × 5 ops = 580 + +| FP_128 +| 116 per op × 5 ops = 580 + +| +| *Grand Total: 2900* +|=== + +*Note:* Differs from Aharoni test count. Aharoni reports ~9 E 2 total; our count is higher because we enumerate all 4 sign combinations explicitly and implement 5 operations separately. diff --git a/src/cover_float/cli.py b/src/cover_float/cli.py index e5a842e..a22280d 100644 --- a/src/cover_float/cli.py +++ b/src/cover_float/cli.py @@ -82,6 +82,8 @@ def testgen() -> None: auto_parse("B14", args.output_dir) tg.B15.main() auto_parse("B15", args.output_dir) + tg.B19.main() + auto_parse("B19", args.output_dir) tg.B20.main() auto_parse("B20", args.output_dir) tg.B21.main() @@ -134,6 +136,9 @@ def testgen() -> None: if "B15" in args.models: tg.B15.main() auto_parse("B15", args.output_dir) + if "B19" in args.models: + tg.B19.main() + auto_parse("B19", args.output_dir) if "B20" in args.models: tg.B20.main() auto_parse("B20", args.output_dir) diff --git a/src/cover_float/testgen/B19.py b/src/cover_float/testgen/B19.py new file mode 100644 index 0000000..84711bd --- /dev/null +++ b/src/cover_float/testgen/B19.py @@ -0,0 +1,310 @@ +# B19 - Compare: Different Input Fields Relations +# Aharoni et al. +# +# This model checks various possible differences between two inputs for +# comparison and min/max operations. Test cases are generated for each +# combination of exponent and significand relationship constraints. +# +# Total vectors: 2700 (108 per format x op, across 5 formats and 5 operations) + +import random +from pathlib import Path +from typing import TextIO + +import cover_float.common.constants as const +from cover_float.common.util import reproducible_hash +from cover_float.reference import run_and_store_test_vector + +OPS = [const.OP_FEQ, const.OP_FLT, const.OP_FLE, const.OP_MIN, const.OP_MAX] + +# --------------------------------------------------------------------------- +# Format helpers +# --------------------------------------------------------------------------- + + +def _fmt_params(fmt: str) -> tuple[int, int, int]: + """Return (min_norm_bexp, max_norm_bexp, frac_max) for the format.""" + max_bexp = (1 << const.EXPONENT_BITS[fmt]) - 1 + min_norm_bexp = 1 + max_norm_bexp = max_bexp - 1 + frac_max = (1 << const.MANTISSA_BITS[fmt]) - 1 + return min_norm_bexp, max_norm_bexp, frac_max + + +def _any_frac(fmt: str) -> int: + """Seeded random mid-range fraction: 00..001 < any_frac < all_ones.""" + frac_max = (1 << const.MANTISSA_BITS[fmt]) - 1 + return random.randint(2, frac_max - 1) + + +def _any_exp(fmt: str) -> int: + """Seeded random mid-range exponent: min_norm_bexp < any_exp < max_norm_bexp.""" + max_bexp = (1 << const.EXPONENT_BITS[fmt]) - 1 + max_norm_bexp = max_bexp - 1 + return random.randint(2, max_norm_bexp - 1) + + +def _build(fmt: str, sign: int, bexp: int, frac: int) -> str: + """Pack sign/biased-exp/frac into a 128-bit (32 hex char) string.""" + bits = f"{sign:01b}{bexp:0{const.EXPONENT_BITS[fmt]}b}{frac:0{const.MANTISSA_BITS[fmt]}b}" + return f"{int(bits, 2):032X}" + + +def _emit( + fmt: str, + op: str, + test_f: TextIO, + cover_f: TextIO, + s1: int, + bexp1: int, + frac1: int, + s2: int, + bexp2: int, + frac2: int, +) -> None: + hex1 = _build(fmt, s1, bexp1, frac1) + hex2 = _build(fmt, s2, bexp2, frac2) + run_and_store_test_vector( + f"{op}_{const.ROUND_NEAR_EVEN}_{hex1}_{hex2}_{32 * '0'}_{fmt}_{32 * '0'}_{fmt}_00", + test_f, + cover_f, + ) + + +# --------------------------------------------------------------------------- +# Case functions +# --------------------------------------------------------------------------- + + +def _case_1_normal_x_normal(fmt: str, op: str, test_f: TextIO, cover_f: TextIO) -> int: + """Case 1: +/-Normal x +/-Normal. 9 cells x 4 sign combos = 36.""" + min_nb, max_nb, frac_max = _fmt_params(fmt) + Z = 0 # all zeros + ALL_ONES = frac_max # all ones + count = 0 + + # Exp >: bexp1 = max_norm_bexp, bexp2 = any exp + for frac1, frac2 in [ + (_any_frac(fmt), Z), # sig > + (Z, _any_frac(fmt)), # sig < + (Z, Z), # sig = + ]: + bexp2 = _any_exp(fmt) + for s1 in (0, 1): + for s2 in (0, 1): + _emit(fmt, op, test_f, cover_f, s1, max_nb, frac1, s2, bexp2, frac2) + count += 1 + + # Exp <: bexp1 = min_norm_bexp, bexp2 = any exp + for frac1, frac2 in [ + (ALL_ONES, _any_frac(fmt)), # sig > + (_any_frac(fmt), ALL_ONES), # sig < + (ALL_ONES, ALL_ONES), # sig = + ]: + bexp2 = _any_exp(fmt) + for s1 in (0, 1): + for s2 in (0, 1): + _emit(fmt, op, test_f, cover_f, s1, min_nb, frac1, s2, bexp2, frac2) + count += 1 + + # Exp =: bexp1 = bexp2 = any exp (same value) + for frac1, frac2 in [ + (ALL_ONES, Z), # sig > + (Z, ALL_ONES), # sig < + (Z, Z), # sig = + ]: + bexp = _any_exp(fmt) + for s1 in (0, 1): + for s2 in (0, 1): + _emit(fmt, op, test_f, cover_f, s1, bexp, frac1, s2, bexp, frac2) + count += 1 + + return count + + +def _case_2_normal_x_subnormal(fmt: str, op: str, test_f: TextIO, cover_f: TextIO) -> int: + """Case 2: +/-Normal x +/-SubNormal. 3 cells x 4 sign combos = 12.""" + af = _any_frac(fmt) + bexp1 = _any_exp(fmt) + lsb = 1 # 00..001 + count = 0 + msb = 1 << (const.MANTISSA_BITS[fmt] - 1) # 10000..000 + + for frac1, frac2 in [ + (af, lsb), # sig > + (lsb, af), # sig < (all zeros vs 00..001) + (0, msb), # sig = (same any_frac for both fields) + ]: + for s1 in (0, 1): + for s2 in (0, 1): + _emit(fmt, op, test_f, cover_f, s1, bexp1, frac1, s2, 0, frac2) + count += 1 + + return count + + +def _case_3_subnormal_x_normal(fmt: str, op: str, test_f: TextIO, cover_f: TextIO) -> int: + """Case 3: +/-SubNormal x +/-Normal. 3 cells x 4 sign combos = 12.""" + _, _, frac_max = _fmt_params(fmt) + af = _any_frac(fmt) + bexp2 = _any_exp(fmt) + ALL_ONES = frac_max # all ones + msb = 1 << (const.MANTISSA_BITS[fmt] - 1) # 10000..000 + count = 0 + + for frac1, frac2 in [ + (ALL_ONES, 0), # sig > (all ones vs all zeros) + (af, ALL_ONES), # sig < + (msb, 0), # sig = (same any_frac for both fields) + ]: + for s1 in (0, 1): + for s2 in (0, 1): + _emit(fmt, op, test_f, cover_f, s1, 0, frac1, s2, bexp2, frac2) + count += 1 + + return count + + +def _case_4_subnormal_x_subnormal(fmt: str, op: str, test_f: TextIO, cover_f: TextIO) -> int: + """Case 4: +/-SubNormal x +/-SubNormal. 5 cells x 4 sign combos = 20.""" + _, _, frac_max = _fmt_params(fmt) + af = _any_frac(fmt) + lsb = 1 # 00..001 + msb = 1 << (const.MANTISSA_BITS[fmt] - 1) # 10000..000 + ALL_ONES = frac_max # all ones + count = 0 + + for frac1, frac2 in [ + (af, lsb), # exp >, sig > + (lsb, af), # exp <, sig < + (ALL_ONES, msb), # exp =, sig > + (msb, ALL_ONES), # exp =, sig < + (af, af), # exp =, sig = (same any_frac) + ]: + for s1 in (0, 1): + for s2 in (0, 1): + _emit(fmt, op, test_f, cover_f, s1, 0, frac1, s2, 0, frac2) + count += 1 + + return count + + +def _case_5_zero_x_normal(fmt: str, op: str, test_f: TextIO, cover_f: TextIO) -> int: + """Case 5: +/-Zero x +/-Normal. 2 cells x 4 sign combos = 8.""" + af = _any_frac(fmt) + bexp2 = _any_exp(fmt) + count = 0 + + for frac2 in [ + af, # sig < (zero frac=0 < any_frac) + 0, # sig = (zero frac=0 == all zeros) + ]: + for s1 in (0, 1): + for s2 in (0, 1): + _emit(fmt, op, test_f, cover_f, s1, 0, 0, s2, bexp2, frac2) + count += 1 + + return count + + +def _case_6_normal_x_zero(fmt: str, op: str, test_f: TextIO, cover_f: TextIO) -> int: + """Case 6: +/-Normal x +/-Zero. 2 cells x 4 sign combos = 8.""" + af = _any_frac(fmt) + bexp1 = _any_exp(fmt) + count = 0 + + for frac1 in [ + af, # sig > (any_frac > zero frac=0) + 0, # sig = (all zeros == zero frac=0) + ]: + for s1 in (0, 1): + for s2 in (0, 1): + _emit(fmt, op, test_f, cover_f, s1, bexp1, frac1, s2, 0, 0) + count += 1 + + return count + + +def _case_7_zero_x_subnormal(fmt: str, op: str, test_f: TextIO, cover_f: TextIO) -> int: + """Case 7: +/-Zero x +/-Subnormal. 1 cell x 4 sign combos = 4.""" + af = _any_frac(fmt) + count = 0 + msb = 1 << (const.MANTISSA_BITS[fmt] - 1) # 10000..000 + + for frac2 in [ + af, # sig < (zero frac=0 < any_frac) + msb, + ]: + for s1 in (0, 1): + for s2 in (0, 1): + _emit(fmt, op, test_f, cover_f, s1, 0, 0, s2, 0, frac2) + count += 1 + + return count + + +def _case_8_subnormal_x_zero(fmt: str, op: str, test_f: TextIO, cover_f: TextIO) -> int: + """Case 8: +/-Subnormal x +/-Zero. 1 cell x 4 sign combos = 4.""" + af = _any_frac(fmt) + count = 0 + msb = 1 << (const.MANTISSA_BITS[fmt] - 1) # 10000..000 + + for frac1 in [ + af, # sig > (any_frac > zero frac=0) + msb, + ]: + for s1 in (0, 1): + for s2 in (0, 1): + _emit(fmt, op, test_f, cover_f, s1, 0, frac1, s2, 0, 0) + count += 1 + + return count + + +def _case_9_zero_x_zero(fmt: str, op: str, test_f: TextIO, cover_f: TextIO) -> int: + """Case 9: +/-Zero x +/-Zero. 1 cell x 4 sign combos = 4.""" + count = 0 + for s1 in (0, 1): + for s2 in (0, 1): + _emit(fmt, op, test_f, cover_f, s1, 0, 0, s2, 0, 0) + count += 1 + return count + + +# --------------------------------------------------------------------------- +# Top-level entry points +# --------------------------------------------------------------------------- + + +def generate_b19_tests(test_f: TextIO, cover_f: TextIO, fmt: str) -> None: + """Generate all B19 test vectors for a given format.""" + for op in OPS: + random.seed(reproducible_hash(f"B19 {fmt} {op}")) + c1 = _case_1_normal_x_normal(fmt, op, test_f, cover_f) + c2 = _case_2_normal_x_subnormal(fmt, op, test_f, cover_f) + c3 = _case_3_subnormal_x_normal(fmt, op, test_f, cover_f) + c4 = _case_4_subnormal_x_subnormal(fmt, op, test_f, cover_f) + c5 = _case_5_zero_x_normal(fmt, op, test_f, cover_f) + c6 = _case_6_normal_x_zero(fmt, op, test_f, cover_f) + c7 = _case_7_zero_x_subnormal(fmt, op, test_f, cover_f) + c8 = _case_8_subnormal_x_zero(fmt, op, test_f, cover_f) + c9 = _case_9_zero_x_zero(fmt, op, test_f, cover_f) + total = c1 + c2 + c3 + c4 + c5 + c6 + c7 + c8 + c9 + print(f" {op}: c1={c1} c2={c2} c3={c3} c4={c4} c5={c5} c6={c6} c7={c7} c8={c8} c9={c9} total={total}") + + +def main() -> None: + """Main entry point for B19 test generation.""" + print("Generating B19 test vectors...") + with ( + Path("./tests/testvectors/B19_tv.txt").open("w") as test_f, + Path("./tests/covervectors/B19_cv.txt").open("w") as cover_f, + ): + for fmt in const.FLOAT_FMTS: + print(f"Format: {fmt}") + generate_b19_tests(test_f, cover_f, fmt) + print("Done!") + + +if __name__ == "__main__": + main() diff --git a/src/cover_float/testgen/__init__.py b/src/cover_float/testgen/__init__.py index 05a4a0d..46f9f5b 100644 --- a/src/cover_float/testgen/__init__.py +++ b/src/cover_float/testgen/__init__.py @@ -11,6 +11,7 @@ import cover_float.testgen.B13 as B13 import cover_float.testgen.B14 as B14 import cover_float.testgen.B15 as B15 +import cover_float.testgen.B19 as B19 import cover_float.testgen.B20 as B20 import cover_float.testgen.B21 as B21 import cover_float.testgen.B25 as B25 @@ -32,6 +33,7 @@ "B13", "B14", "B15", + "B19", "B20", "B21", "B25",