From 2d60db7c0c9d848be8d11d75399bac43b04abfc5 Mon Sep 17 00:00:00 2001 From: Sisi Wang Date: Wed, 1 Apr 2026 20:32:28 -0700 Subject: [PATCH 1/8] Implement B19 test vector generator according to spec MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Implement B19.py with all 7 test cases (Cases 1-5, 7, 9) - Generate 8200 test vectors per spec (328 per format×op) - Support all 5 comparison/min-max operations - Support all 5 floating-point formats (BF16, FP16, FP32, FP64, FP128) - Add comprehensive B19.adoc documentation with all case tables - Correct for Python 3.9 compatibility (avoid type union syntax) Made-with: Cursor --- Makefile | 5 +- docs/B19.adoc | 793 ++++++++++++++++++++++++++++ src/cover_float/cli.py | 3 + src/cover_float/testgen/B19.py | 309 +++++++++++ src/cover_float/testgen/__init__.py | 3 +- 5 files changed, 1111 insertions(+), 2 deletions(-) create mode 100644 docs/B19.adoc create mode 100644 src/cover_float/testgen/B19.py diff --git a/Makefile b/Makefile index 191dd81..f01bd5e 100644 --- a/Makefile +++ b/Makefile @@ -2,7 +2,7 @@ RM_CMD ?= rm -rf -.PHONY: build clean sim all B1 B10 +.PHONY: build clean sim all B1 B10 B19 # Notice that we pass --managed-python, we do this so that uv (scikit-build-core) # will have a python enviornment with Python.h to build with. @@ -32,6 +32,9 @@ B12: B14: uv run --managed-python cover-float-testgen --model B14 +B19: + uv run --managed-python cover-float-testgen --model B19 + # Clean target to remove build artifacts clean: @echo "Cleaning build directory..." diff --git a/docs/B19.adoc b/docs/B19.adoc new file mode 100644 index 0000000..a8cf87b --- /dev/null +++ b/docs/B19.adoc @@ -0,0 +1,793 @@ += 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 — 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-ones frac = "1s padding") + +0s padding = frac field of all zeros (the frac of MinNorm) +1s padding = frac field of all ones (the frac of MaxNorm) +00..001 = frac = 1 (the frac of MinSubNorm) +10000..000 = frac with only the MSB set +any frac = representative mid-range frac (0x5A tiled pattern, always > 1) +any exp = one of 4 representative normal biased-exponent anchors (see below) +00000 = biased exponent field of 0 (subnormal / zero encoding) +11110 = max_norm_bexp in 5-bit FP16 notation; generalises to max_norm_bexp +00001 = min_norm_bexp = 1 +---- + +==== 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: + +[source] +---- +eff_exp(frac) = bit_position_of_leading_1(frac) + (1 - bias - frac_bits) +---- + +This means two subnormals can have exp >, =, or < relationships based on their frac fields. A subnormal with a higher leading-1 position has both a larger effective exponent AND a larger frac value, so exp > always implies sig > and exp < always implies sig <. Only exp = leaves sig free. + +==== 'any exp' anchor values + +For each format, 4 evenly-spaced representative normal biased-exponent values are used: + +[cols="2,3,3,3",options="header"] +|=== +| Format | Full anchors (any exp) | Anchors < max (exp> rows) | Anchors > min (exp< rows) + +| BF16 +| 1, 85, 169, 254 +| 1, 85, 169, 253 +| 2, 86, 170, 254 + +| FP16 +| 1, 10, 19, 30 +| 1, 10, 19, 29 +| 2, 11, 20, 30 + +| FP32 +| 1, 85, 169, 254 +| 1, 85, 169, 253 +| 2, 86, 170, 254 + +| FP64 +| 1, 682, 1363, 2046 +| 1, 682, 1363, 2045 +| 2, 683, 1364, 2046 + +| FP128 +| 1, 10922, 21843, 32766 +| 1, 10922, 21843, 32765 +| 2, 10923, 21844, 32766 +|=== + +For exp> rows, anchors are restricted to be strictly less than max_norm_bexp so that bexp1 = max_norm_bexp > bexp2 is always satisfied. Similarly for exp< rows, anchors are strictly greater than min_norm_bexp. + +--- + +=== 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: (+/+), (+/−), (−/+), (−/−) +* All 4 'any exp' anchors (where applicable) + +The frac field values are deterministic constants derived from the format (0s, 1s, 00..001, 10000..000, any_frac). The 'any exp' biased-exponent anchors are also deterministic. A seeded random is used only for the bits of 'any frac' 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 (< max) +| any frac +| 0s padding + +| > +| < +| max_norm_bexp +| any exp (< max) +| 0s padding +| any frac + +| > +| = +| max_norm_bexp +| any exp (< max) +| 0s padding +| 0s padding + +| < +| > +| min_norm_bexp +| any exp (> min) +| 1s padding +| any frac + +| < +| < +| min_norm_bexp +| any exp (> min) +| any frac +| 1s padding + +| < +| = +| min_norm_bexp +| any exp (> min) +| 1s padding +| 1s padding + +| = +| > +| any exp +| any exp (same) +| 1s padding +| 0s padding + +| = +| < +| any exp +| any exp (same) +| 0s padding +| 1s padding + +| = +| = +| any exp +| any exp (same) +| 0s padding +| 0s padding +|=== + +*Total per precision:* 9 cells × 4 exp anchors × 4 sign combos = **144** + +==== Impossibility reasoning + +All 9 combinations are achievable. Normal numbers have a freely adjustable biased exponent in [1, max_norm_bexp] and a freely adjustable frac in [0, frac_max], so all three exp relations and all three sig relations can be independently constructed. + +--- + +=== 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 +| 00000 +| any frac +| 00..001 + +| > +| < +| any exp +| 00000 +| 0s padding +| 00..001 + +| > +| = +| any exp +| 00000 +| any frac +| any frac + +| < +| > +| impossible +| +| +| + +| < +| < +| impossible +| +| +| + +| < +| = +| impossible +| +| +| + +| = +| > +| impossible +| +| +| + +| = +| < +| impossible +| +| +| + +| = +| = +| impossible +| +| +| +|=== + +*Total per precision:* 3 cells × 4 exp anchors × 4 sign combos = **48** + +==== Impossibility reasoning + +A normal number has biased exponent ≥ 1, while a subnormal has biased exponent = 0. The normal's effective exponent ranges from (1 − bias) to bias, while the subnormal's effective exponent ranges from (1 − bias − frac_bits) to (−bias). Since (−bias) < (1 − bias), the subnormal's effective exponent is always strictly less than the normal's. Therefore exp < (normal < subnormal) and exp = are structurally impossible — *only exp > is achievable*. + +For the sig relation: F_input_2 is fixed at 00..001 (= 1, the smallest valid subnormal frac). F_input_1 = any_frac > 1 gives sig >. F_input_1 = 0s (= 0) < 1 gives sig <. F_input_1 = any_frac with F_input_2 = any_frac (same value) gives sig =. + +--- + +=== 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 +| +| +| + +| < +| > +| 00000 +| any exp +| 1s padding +| 0s padding + +| < +| < +| 00000 +| any exp +| any frac +| 1s padding + +| < +| = +| 00000 +| any exp +| any frac +| any frac + +| = +| > +| impossible +| +| +| + +| = +| < +| impossible +| +| +| + +| = +| = +| impossible +| +| +| +|=== + +*Total per precision:* 3 cells × 4 exp anchors × 4 sign combos = **48** + +==== 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*. + +For the sig relation: F_input_2 = 0s (= 0) gives frac2 < frac1 = 1s, yielding sig >. F_input_2 = 1s (= frac_max) with F_input_1 = any_frac < frac_max gives sig <. F_input_1 = any_frac = F_input_2 = any_frac gives sig =. + +--- + +=== 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 +| 1s padding +| 10000..000 + +| = +| < +| 0s +| 0s +| 10000..000 +| 1s padding + +| = +| = +| 0s +| 0s +| any frac +| any frac +|=== + +*Total per precision:* 5 cells × 4 sign combos = **20** (no exp anchor 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: 1s padding (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 +| 0s +| any frac + +| < +| = +| 0s +| any exp +| 0s +| 0s + +| = +| > +| impossible +| +| +| + +| = +| < +| impossible +| +| +| + +| = +| = +| impossible +| +| +| +|=== + +*Total per precision:* 2 cells × 4 exp anchors × 4 sign combos = **32** + +==== 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 = 0s gives frac1 = frac2 = 0 giving sig =. + +--- + +=== Case 7: ±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 +| 0s + +| > +| < +| impossible +| +| +| + +| > +| = +| any exp +| 0s +| 0s padding +| 0s + +| < +| > +| impossible +| +| +| + +| < +| < +| impossible +| +| +| + +| < +| = +| impossible +| +| +| + +| = +| > +| impossible +| +| +| + +| = +| < +| impossible +| +| +| + +| = +| = +| impossible +| +| +| +|=== + +*Total per precision:* 2 cells × 4 exp anchors × 4 sign combos = **32** + +==== 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 = 0s padding, not any_frac. Both are 0, giving sig =. + +--- + +=== 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 +| 0s +| 0s +|=== + +*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,1",options="header"] +|=== +| Case | Category pair | Achievable cells | Anchor axis | Sign axis | Per (fmt, op) + +| 1 +| Normal × Normal +| 9 +| × 4 +| × 4 +| 144 + +| 2 +| Normal × SubNormal +| 3 +| × 4 +| × 4 +| 48 + +| 3 +| SubNormal × Normal +| 3 +| × 4 +| × 4 +| 48 + +| 4 +| SubNormal × SubNormal +| 5 +| × 1 +| × 4 +| 20 + +| 5 +| Zero × Normal +| 2 +| × 4 +| × 4 +| 32 + +| 7 +| Normal × Zero +| 2 +| × 4 +| × 4 +| 32 + +| 9 +| Zero × Zero +| 1 +| × 1 +| × 4 +| 4 + +| +| +| +| +| *Total per (fmt, op):* +| *328* +|=== + +=== Grand Total Breakdown + +[cols="2,2",options="header"] +|=== +| Format | Total vectors + +| BF_16 +| 328 per op × 5 ops = 1640 + +| FP_16 +| 328 per op × 5 ops = 1640 + +| FP_32 +| 328 per op × 5 ops = 1640 + +| FP_64 +| 328 per op × 5 ops = 1640 + +| FP_128 +| 328 per op × 5 ops = 1640 + +| +| *Grand Total: 8200* +|=== + +*Note:* Differs from Aharoni test count. Aharoni reports ~9 E 2 total; our count is higher because we enumerate all 4 sign combinations and 4 representative exponent anchors explicitly, and implement 5 operations separately. diff --git a/src/cover_float/cli.py b/src/cover_float/cli.py index c9d5b3b..7efd558 100644 --- a/src/cover_float/cli.py +++ b/src/cover_float/cli.py @@ -43,6 +43,7 @@ def testgen() -> None: tg.B9.main() tg.B10.main() tg.B12.main() + tg.B19.main() else: if "B1" in args.models: tg.B1.main() @@ -52,3 +53,5 @@ def testgen() -> None: tg.B10.main() if "B12" in args.models: tg.B12.main() + if "B19" in args.models: + tg.B19.main() diff --git a/src/cover_float/testgen/B19.py b/src/cover_float/testgen/B19.py new file mode 100644 index 0000000..29219ef --- /dev/null +++ b/src/cover_float/testgen/B19.py @@ -0,0 +1,309 @@ +# 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: 8200 (328 per format×op, across 5 formats and 5 operations) + +from pathlib import Path +from typing import NamedTuple, TextIO + +import cover_float.common.constants as const +from cover_float.reference import run_and_store_test_vector + + +# Operations to test +OPS = [const.OP_FEQ, const.OP_FLT, const.OP_FLE, const.OP_MIN, const.OP_MAX] + +# Exponent anchor values per format (4 evenly-spaced representatives per format) +EXP_ANCHORS = { + const.FMT_BF16: [1, 85, 169, 254], + const.FMT_HALF: [1, 10, 19, 30], + const.FMT_SINGLE: [1, 85, 169, 254], + const.FMT_DOUBLE: [1, 682, 1363, 2046], + const.FMT_QUAD: [1, 10922, 21843, 32766], +} + +# Exponent anchor values for exp> cases (restricted to be < max_norm_bexp) +EXP_ANCHORS_LT_MAX = { + const.FMT_BF16: [1, 85, 169, 253], + const.FMT_HALF: [1, 10, 19, 29], + const.FMT_SINGLE: [1, 85, 169, 253], + const.FMT_DOUBLE: [1, 682, 1363, 2045], + const.FMT_QUAD: [1, 10922, 21843, 32765], +} + +# Exponent anchor values for exp< cases (restricted to be > min_norm_bexp) +EXP_ANCHORS_GT_MIN = { + const.FMT_BF16: [2, 86, 170, 254], + const.FMT_HALF: [2, 11, 20, 30], + const.FMT_SINGLE: [2, 86, 170, 254], + const.FMT_DOUBLE: [2, 683, 1364, 2046], + const.FMT_QUAD: [2, 10923, 21844, 32766], +} + + +def _decimalComponentsToHex(fmt, sign, biased_exp, mantissa): + """Convert sign, biased exponent, and mantissa to 32-bit hex string.""" + b_sign = f"{sign:01b}" + b_exp = f"{biased_exp:0{const.EXPONENT_BITS[fmt]}b}" + b_man = f"{mantissa:0{const.MANTISSA_BITS[fmt]}b}" + b_complete = b_sign + b_exp + b_man + h_complete = f"{int(b_complete, 2):032X}" + return h_complete + + +def _tile_0x5a_pattern(bit_width): + """Create a tiled 0x5A pattern to fill the given bit width.""" + pattern = 0 + for i in range(0, bit_width, 8): + pattern |= 0x5A << i + return pattern & ((1 << bit_width) - 1) + + +def _get_frac_values(fmt): + """Get frac field constants for the format.""" + frac_bits = const.MANTISSA_BITS[fmt] + return { + "0s": 0, + "1s": (1 << frac_bits) - 1, + "00001": 1, + "10000": 1 << (frac_bits - 1), + "any": _tile_0x5a_pattern(frac_bits), + } + + +def _case_1_normal_x_normal(fmt, test_f, cover_f, op): + """Case 1: Normal x Normal (144 vectors per format).""" + count = 0 + fracs = _get_frac_values(fmt) + max_norm_bexp = (1 << const.EXPONENT_BITS[fmt]) - 1 - 1 + + # Exp > cells (3 sig_rel variants) + for sig_rel, frac1, frac2 in [ + ("gt", fracs["any"], fracs["0s"]), + ("<", fracs["0s"], fracs["any"]), + ("=", fracs["0s"], fracs["0s"]), + ]: + for bexp2 in EXP_ANCHORS_LT_MAX[fmt]: + for sign1 in [0, 1]: + for sign2 in [0, 1]: + hex1 = _decimalComponentsToHex(fmt, sign1, max_norm_bexp, frac1) + hex2 = _decimalComponentsToHex(fmt, sign2, 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, + ) + count += 1 + + # Exp < cells (3 sig_rel variants) + for sig_rel, frac1, frac2 in [ + ("gt", fracs["1s"], fracs["any"]), + ("<", fracs["any"], fracs["1s"]), + ("=", fracs["1s"], fracs["1s"]), + ]: + for bexp2 in EXP_ANCHORS_GT_MIN[fmt]: + for sign1 in [0, 1]: + for sign2 in [0, 1]: + hex1 = _decimalComponentsToHex(fmt, sign1, 1, frac1) + hex2 = _decimalComponentsToHex(fmt, sign2, 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, + ) + count += 1 + + # Exp = cells (3 sig_rel variants, same bexp for both operands) + for sig_rel, frac1, frac2 in [ + ("gt", fracs["1s"], fracs["0s"]), + ("<", fracs["0s"], fracs["1s"]), + ("=", fracs["0s"], fracs["0s"]), + ]: + for common_bexp in EXP_ANCHORS[fmt]: + for sign1 in [0, 1]: + for sign2 in [0, 1]: + hex1 = _decimalComponentsToHex(fmt, sign1, common_bexp, frac1) + hex2 = _decimalComponentsToHex(fmt, sign2, common_bexp, 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, + ) + count += 1 + + return count + + +def _case_2_normal_x_subnormal(fmt, test_f, cover_f, op): + """Case 2: Normal x SubNormal (48 vectors per format).""" + count = 0 + fracs = _get_frac_values(fmt) + + for sig_rel, frac1, frac2 in [ + ("gt", fracs["any"], fracs["00001"]), + ("<", fracs["0s"], fracs["00001"]), + ("=", fracs["any"], fracs["any"]), + ]: + for bexp1 in EXP_ANCHORS[fmt]: + for sign1 in [0, 1]: + for sign2 in [0, 1]: + hex1 = _decimalComponentsToHex(fmt, sign1, bexp1, frac1) + hex2 = _decimalComponentsToHex(fmt, sign2, 0, 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, + ) + count += 1 + + return count + + +def _case_3_subnormal_x_normal(fmt, test_f, cover_f, op): + """Case 3: SubNormal x Normal (48 vectors per format).""" + count = 0 + fracs = _get_frac_values(fmt) + + for sig_rel, frac1, frac2 in [ + ("gt", fracs["1s"], fracs["0s"]), + ("<", fracs["any"], fracs["1s"]), + ("=", fracs["any"], fracs["any"]), + ]: + for bexp2 in EXP_ANCHORS[fmt]: + for sign1 in [0, 1]: + for sign2 in [0, 1]: + hex1 = _decimalComponentsToHex(fmt, sign1, 0, frac1) + hex2 = _decimalComponentsToHex(fmt, sign2, 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, + ) + count += 1 + + return count + + +def _case_4_subnormal_x_subnormal(fmt, test_f, cover_f, op): + """Case 4: SubNormal x SubNormal (20 vectors per format).""" + count = 0 + fracs = _get_frac_values(fmt) + + for frac1, frac2 in [ + (fracs["any"], fracs["00001"]), + (fracs["00001"], fracs["any"]), + (fracs["1s"], fracs["10000"]), + (fracs["10000"], fracs["1s"]), + (fracs["any"], fracs["any"]), + ]: + for sign1 in [0, 1]: + for sign2 in [0, 1]: + hex1 = _decimalComponentsToHex(fmt, sign1, 0, frac1) + hex2 = _decimalComponentsToHex(fmt, sign2, 0, 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, + ) + count += 1 + + return count + + +def _case_5_zero_x_normal(fmt, test_f, cover_f, op): + """Case 5: Zero x Normal (32 vectors per format).""" + count = 0 + fracs = _get_frac_values(fmt) + + for frac2 in [fracs["any"], fracs["0s"]]: + for bexp2 in EXP_ANCHORS[fmt]: + for sign1 in [0, 1]: + for sign2 in [0, 1]: + hex1 = _decimalComponentsToHex(fmt, sign1, 0, fracs["0s"]) + hex2 = _decimalComponentsToHex(fmt, sign2, 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, + ) + count += 1 + + return count + + +def _case_7_normal_x_zero(fmt, test_f, cover_f, op): + """Case 7: Normal x Zero (32 vectors per format).""" + count = 0 + fracs = _get_frac_values(fmt) + + for frac1 in [fracs["any"], fracs["0s"]]: + for bexp1 in EXP_ANCHORS[fmt]: + for sign1 in [0, 1]: + for sign2 in [0, 1]: + hex1 = _decimalComponentsToHex(fmt, sign1, bexp1, frac1) + hex2 = _decimalComponentsToHex(fmt, sign2, 0, fracs["0s"]) + run_and_store_test_vector( + f"{op}_{const.ROUND_NEAR_EVEN}_{hex1}_{hex2}_{32 * '0'}_{fmt}_{32 * '0'}_{fmt}_00", + test_f, + cover_f, + ) + count += 1 + + return count + + +def _case_9_zero_x_zero(fmt, test_f, cover_f, op): + """Case 9: Zero x Zero (4 vectors per format).""" + count = 0 + fracs = _get_frac_values(fmt) + + for sign1 in [0, 1]: + for sign2 in [0, 1]: + hex1 = _decimalComponentsToHex(fmt, sign1, 0, fracs["0s"]) + hex2 = _decimalComponentsToHex(fmt, sign2, 0, fracs["0s"]) + run_and_store_test_vector( + f"{op}_{const.ROUND_NEAR_EVEN}_{hex1}_{hex2}_{32 * '0'}_{fmt}_{32 * '0'}_{fmt}_00", + test_f, + cover_f, + ) + count += 1 + + return count + + +def generate_b19_tests(test_f, cover_f, fmt): + """Generate all B19 test vectors for a given format.""" + for op in OPS: + case1 = _case_1_normal_x_normal(fmt, test_f, cover_f, op) + case2 = _case_2_normal_x_subnormal(fmt, test_f, cover_f, op) + case3 = _case_3_subnormal_x_normal(fmt, test_f, cover_f, op) + case4 = _case_4_subnormal_x_subnormal(fmt, test_f, cover_f, op) + case5 = _case_5_zero_x_normal(fmt, test_f, cover_f, op) + case7 = _case_7_normal_x_zero(fmt, test_f, cover_f, op) + case9 = _case_9_zero_x_zero(fmt, test_f, cover_f, op) + + total = case1 + case2 + case3 + case4 + case5 + case7 + case9 + + print(f" {op}: case1={case1}, case2={case2}, case3={case3}, case4={case4}, " + f"case5={case5}, case7={case7}, case9={case9}, total={total}") + + +def main(): + """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 beef381..bd8ab0e 100644 --- a/src/cover_float/testgen/__init__.py +++ b/src/cover_float/testgen/__init__.py @@ -2,5 +2,6 @@ import cover_float.testgen.B9 as B9 import cover_float.testgen.B10 as B10 import cover_float.testgen.B12 as B12 +import cover_float.testgen.B19 as B19 -__all__ = ["B1", "B9", "B10", "B12"] +__all__ = ["B1", "B9", "B10", "B12", "B19"] From 4c78ba64412355a40852216244a552d0db6560d7 Mon Sep 17 00:00:00 2001 From: Sisi Wang Date: Tue, 7 Apr 2026 15:10:27 -0700 Subject: [PATCH 2/8] Add B19 test generator and documentation MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Implement B19 test generator covering all 7 case pairs (Normal×Normal, Normal×SubNormal, SubNormal×Normal, SubNormal×SubNormal, Zero×Normal, Normal×Zero, Zero×Zero) with 4 sign combinations each (100 vectors per format×op, 2500 grand total) - Use seeded random via reproducible_hash for any_frac and any_exp values - Update docs/B19.adoc with revised definitions, case tables, and test count breakdown (removed fixed anchor tables, updated to randomized model) - Enable COVER_B19 in config.svh Made-with: Cursor --- config.svh | 22 +- docs/B19.adoc | 220 +++++++---------- src/cover_float/testgen/B19.py | 416 +++++++++++++++------------------ 3 files changed, 281 insertions(+), 377 deletions(-) diff --git a/config.svh b/config.svh index e891fb2..d52206f 100644 --- a/config.svh +++ b/config.svh @@ -1,27 +1,27 @@ // 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_B17 // `define COVER_B18 -// `define COVER_B19 +`define COVER_B19 // `define COVER_B20 -`define COVER_B21 +//`define COVER_B21 // `define COVER_B22 // `define COVER_B23 // `define COVER_B24 diff --git a/docs/B19.adoc b/docs/B19.adoc index a8cf87b..63839de 100644 --- a/docs/B19.adoc +++ b/docs/B19.adoc @@ -46,7 +46,6 @@ This model checks various possible differences between two inputs. A test-case w *Operations supported:* OP_FEQ, OP_FLT, OP_FLE, OP_MIN, OP_MAX ---- == Implementation @@ -55,82 +54,47 @@ This model checks various possible differences between two inputs. A test-case w [source] ---- bias = (2 ^ (exp_bits - 1)) - 1 -max_bexp = (2 ^ exp_bits) - 1 (all-ones; encodes NaN/Inf — not a valid normal) +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-ones frac = "1s padding") - -0s padding = frac field of all zeros (the frac of MinNorm) -1s padding = frac field of all ones (the frac of MaxNorm) -00..001 = frac = 1 (the frac of MinSubNorm) -10000..000 = frac with only the MSB set -any frac = representative mid-range frac (0x5A tiled pattern, always > 1) -any exp = one of 4 representative normal biased-exponent anchors (see below) -00000 = biased exponent field of 0 (subnormal / zero encoding) -11110 = max_norm_bexp in 5-bit FP16 notation; generalises to max_norm_bexp -00001 = min_norm_bexp = 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) = bit_position_of_leading_1(frac) + (1 - bias - frac_bits) +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]): -This means two subnormals can have exp >, =, or < relationships based on their frac fields. A subnormal with a higher leading-1 position has both a larger effective exponent AND a larger frac value, so exp > always implies sig > and exp < always implies sig <. Only exp = leaves sig free. - -==== 'any exp' anchor values - -For each format, 4 evenly-spaced representative normal biased-exponent values are used: - -[cols="2,3,3,3",options="header"] -|=== -| Format | Full anchors (any exp) | Anchors < max (exp> rows) | Anchors > min (exp< rows) - -| BF16 -| 1, 85, 169, 254 -| 1, 85, 169, 253 -| 2, 86, 170, 254 - -| FP16 -| 1, 10, 19, 30 -| 1, 10, 19, 29 -| 2, 11, 20, 30 - -| FP32 -| 1, 85, 169, 254 -| 1, 85, 169, 253 -| 2, 86, 170, 254 - -| FP64 -| 1, 682, 1363, 2046 -| 1, 682, 1363, 2045 -| 2, 683, 1364, 2046 - -| FP128 -| 1, 10922, 21843, 32766 -| 1, 10922, 21843, 32765 -| 2, 10923, 21844, 32766 -|=== +* `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]. -For exp> rows, anchors are restricted to be strictly less than max_norm_bexp so that bexp1 = max_norm_bexp > bexp2 is always satisfied. Similarly for exp< rows, anchors are strictly greater than min_norm_bexp. +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: (+/+), (+/−), (−/+), (−/−) -* All 4 'any exp' anchors (where applicable) +* All 4 sign combinations: (+/+), (+/-), (-/+), (-/-) -The frac field values are deterministic constants derived from the format (0s, 1s, 00..001, 10000..000, any_frac). The 'any exp' biased-exponent anchors are also deterministic. A seeded random is used only for the bits of 'any frac' where randomisation is appropriate (see implementation). +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 @@ -143,72 +107,68 @@ The frac field values are deterministic constants derived from the format (0s, 1 | > | > | max_norm_bexp -| any exp (< max) +| any exp | any frac -| 0s padding +| all zeros | > | < | max_norm_bexp -| any exp (< max) -| 0s padding +| any exp +| all zeros | any frac | > | = | max_norm_bexp -| any exp (< max) -| 0s padding -| 0s padding +| any exp +| all zeros +| all zeros | < | > | min_norm_bexp -| any exp (> min) -| 1s padding +| any exp +| all ones | any frac | < | < | min_norm_bexp -| any exp (> min) +| any exp | any frac -| 1s padding +| all ones | < | = | min_norm_bexp -| any exp (> min) -| 1s padding -| 1s padding +| any exp +| all ones +| all ones | = | > | any exp | any exp (same) -| 1s padding -| 0s padding +| all ones +| all zeros | = | < | any exp | any exp (same) -| 0s padding -| 1s padding +| all zeros +| all ones | = | = | any exp | any exp (same) -| 0s padding -| 0s padding +| all zeros +| all zeros |=== -*Total per precision:* 9 cells × 4 exp anchors × 4 sign combos = **144** - -==== Impossibility reasoning - -All 9 combinations are achievable. Normal numbers have a freely adjustable biased exponent in [1, max_norm_bexp] and a freely adjustable frac in [0, frac_max], so all three exp relations and all three sig relations can be independently constructed. +*Total per precision:* 9 cells × 4 sign combos = **36** --- @@ -221,21 +181,21 @@ All 9 combinations are achievable. Normal numbers have a freely adjustable biase | > | > | any exp -| 00000 +| 0s | any frac | 00..001 | > | < | any exp -| 00000 -| 0s padding +| 0s +| all zeros | 00..001 | > | = | any exp -| 00000 +| 0s | any frac | any frac @@ -282,13 +242,11 @@ All 9 combinations are achievable. Normal numbers have a freely adjustable biase | |=== -*Total per precision:* 3 cells × 4 exp anchors × 4 sign combos = **48** +*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. The normal's effective exponent ranges from (1 − bias) to bias, while the subnormal's effective exponent ranges from (1 − bias − frac_bits) to (−bias). Since (−bias) < (1 − bias), the subnormal's effective exponent is always strictly less than the normal's. Therefore exp < (normal < subnormal) and exp = are structurally impossible — *only exp > is achievable*. - -For the sig relation: F_input_2 is fixed at 00..001 (= 1, the smallest valid subnormal frac). F_input_1 = any_frac > 1 gives sig >. F_input_1 = 0s (= 0) < 1 gives sig <. F_input_1 = any_frac with F_input_2 = any_frac (same value) gives sig =. +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*. --- @@ -321,21 +279,21 @@ For the sig relation: F_input_2 is fixed at 00..001 (= 1, the smallest valid sub | < | > -| 00000 +| 0s | any exp -| 1s padding -| 0s padding +| all ones +| all zeros | < | < -| 00000 +| 0s | any exp | any frac -| 1s padding +| all ones | < | = -| 00000 +| 0s | any exp | any frac | any frac @@ -362,14 +320,12 @@ For the sig relation: F_input_2 is fixed at 00..001 (= 1, the smallest valid sub | |=== -*Total per precision:* 3 cells × 4 exp anchors × 4 sign combos = **48** +*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*. -For the sig relation: F_input_2 = 0s (= 0) gives frac2 < frac1 = 1s, yielding sig >. F_input_2 = 1s (= frac_max) with F_input_1 = any_frac < frac_max gives sig <. F_input_1 = any_frac = F_input_2 = any_frac gives sig =. - --- === Case 4: ±SubNormal × ±SubNormal @@ -424,7 +380,7 @@ For the sig relation: F_input_2 = 0s (= 0) gives frac2 < frac1 = 1s, yielding si | > | 0s | 0s -| 1s padding +| all ones | 10000..000 | = @@ -432,7 +388,7 @@ For the sig relation: F_input_2 = 0s (= 0) gives frac2 < frac1 = 1s, yielding si | 0s | 0s | 10000..000 -| 1s padding +| all ones | = | = @@ -442,7 +398,7 @@ For the sig relation: F_input_2 = 0s (= 0) gives frac2 < frac1 = 1s, yielding si | any frac |=== -*Total per precision:* 5 cells × 4 sign combos = **20** (no exp anchor axis — both bexp fields are always 0) +*Total per precision:* 5 cells × 4 sign combos = **20** (no exp axis — both bexp fields are always 0) ==== Impossibility reasoning @@ -450,7 +406,7 @@ Both subnormals have a stored biased exponent field of 0. Their _effective_ expo * *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: 1s padding (1111..1) > 10000..000 (1000..0) for sig >, reversed for sig <, and identical fracs for sig =. +* *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. @@ -494,15 +450,15 @@ The cells (>, <), (>, =), (<, >), (<, =) are impossible except the five rows sho | < | 0s | any exp -| 0s +| all zeros | any frac | < | = | 0s | any exp -| 0s -| 0s +| all zeros +| all zeros | = | > @@ -526,7 +482,7 @@ The cells (>, <), (>, =), (<, >), (<, =) are impossible except the five rows sho | |=== -*Total per precision:* 2 cells × 4 exp anchors × 4 sign combos = **32** +*Total per precision:* 2 cells × 4 sign combos = **8** ==== Impossibility reasoning @@ -534,7 +490,7 @@ The cells (>, <), (>, =), (<, >), (<, =) are impossible except the five rows sho * *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 = 0s gives frac1 = frac2 = 0 giving sig =. +* *exp < sig < and exp < sig = are achievable:* frac2 = any_frac > 0 gives sig <; frac2 = all zeros gives frac1 = frac2 = 0 giving sig =. --- @@ -549,7 +505,7 @@ The cells (>, <), (>, =), (<, >), (<, =) are impossible except the five rows sho | any exp | 0s | any frac -| 0s +| all zeros | > | < @@ -562,8 +518,8 @@ The cells (>, <), (>, =), (<, >), (<, =) are impossible except the five rows sho | = | any exp | 0s -| 0s padding -| 0s +| all zeros +| all zeros | < | > @@ -608,7 +564,7 @@ The cells (>, <), (>, =), (<, >), (<, =) are impossible except the five rows sho | |=== -*Total per precision:* 2 cells × 4 exp anchors × 4 sign combos = **32** +*Total per precision:* 2 cells × 4 sign combos = **8** ==== Impossibility reasoning @@ -618,7 +574,7 @@ The cells (>, <), (>, =), (<, >), (<, =) are impossible except the five rows sho * *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 = 0s padding, not any_frac. Both are 0, giving sig =. +* *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 =. --- @@ -688,8 +644,8 @@ The cells (>, <), (>, =), (<, >), (<, =) are impossible except the five rows sho | = | 0s | 0s -| 0s -| 0s +| all zeros +| all zeros |=== *Total per precision:* 1 cell × 4 sign combos = **4** @@ -704,35 +660,31 @@ The 4 vectors come from the 4 sign combinations: (+0,+0), (+0,−0), (−0,+0), == Test Count Breakdown -[cols="1,2,2,1,1,1",options="header"] +[cols="1,2,2,1,1",options="header"] |=== -| Case | Category pair | Achievable cells | Anchor axis | Sign axis | Per (fmt, op) +| Case | Category pair | Achievable cells | Sign axis | Per (fmt, op) | 1 | Normal × Normal | 9 | × 4 -| × 4 -| 144 +| 36 | 2 | Normal × SubNormal | 3 | × 4 -| × 4 -| 48 +| 12 | 3 | SubNormal × Normal | 3 | × 4 -| × 4 -| 48 +| 12 | 4 | SubNormal × SubNormal | 5 -| × 1 | × 4 | 20 @@ -740,29 +692,25 @@ The 4 vectors come from the 4 sign combinations: (+0,+0), (+0,−0), (−0,+0), | Zero × Normal | 2 | × 4 -| × 4 -| 32 +| 8 | 7 | Normal × Zero | 2 | × 4 -| × 4 -| 32 +| 8 | 9 | Zero × Zero | 1 -| × 1 | × 4 | 4 | | | -| | *Total per (fmt, op):* -| *328* +| *100* |=== === Grand Total Breakdown @@ -772,22 +720,22 @@ The 4 vectors come from the 4 sign combinations: (+0,+0), (+0,−0), (−0,+0), | Format | Total vectors | BF_16 -| 328 per op × 5 ops = 1640 +| 100 per op × 5 ops = 500 | FP_16 -| 328 per op × 5 ops = 1640 +| 100 per op × 5 ops = 500 | FP_32 -| 328 per op × 5 ops = 1640 +| 100 per op × 5 ops = 500 | FP_64 -| 328 per op × 5 ops = 1640 +| 100 per op × 5 ops = 500 | FP_128 -| 328 per op × 5 ops = 1640 +| 100 per op × 5 ops = 500 | -| *Grand Total: 8200* +| *Grand Total: 2500* |=== -*Note:* Differs from Aharoni test count. Aharoni reports ~9 E 2 total; our count is higher because we enumerate all 4 sign combinations and 4 representative exponent anchors explicitly, and implement 5 operations separately. +*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. \ No newline at end of file diff --git a/src/cover_float/testgen/B19.py b/src/cover_float/testgen/B19.py index 29219ef..30064f8 100644 --- a/src/cover_float/testgen/B19.py +++ b/src/cover_float/testgen/B19.py @@ -2,294 +2,250 @@ # 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. +# comparison and min/max operations. Test cases are generated for each +# combination of exponent and significand relationship constraints. # -# Total vectors: 8200 (328 per format×op, across 5 formats and 5 operations) +# Total vectors: 2500 (100 per format×op, across 5 formats and 5 operations) +import random from pathlib import Path -from typing import NamedTuple, TextIO +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 -# Operations to test OPS = [const.OP_FEQ, const.OP_FLT, const.OP_FLE, const.OP_MIN, const.OP_MAX] -# Exponent anchor values per format (4 evenly-spaced representatives per format) -EXP_ANCHORS = { - const.FMT_BF16: [1, 85, 169, 254], - const.FMT_HALF: [1, 10, 19, 30], - const.FMT_SINGLE: [1, 85, 169, 254], - const.FMT_DOUBLE: [1, 682, 1363, 2046], - const.FMT_QUAD: [1, 10922, 21843, 32766], -} - -# Exponent anchor values for exp> cases (restricted to be < max_norm_bexp) -EXP_ANCHORS_LT_MAX = { - const.FMT_BF16: [1, 85, 169, 253], - const.FMT_HALF: [1, 10, 19, 29], - const.FMT_SINGLE: [1, 85, 169, 253], - const.FMT_DOUBLE: [1, 682, 1363, 2045], - const.FMT_QUAD: [1, 10922, 21843, 32765], -} - -# Exponent anchor values for exp< cases (restricted to be > min_norm_bexp) -EXP_ANCHORS_GT_MIN = { - const.FMT_BF16: [2, 86, 170, 254], - const.FMT_HALF: [2, 11, 20, 30], - const.FMT_SINGLE: [2, 86, 170, 254], - const.FMT_DOUBLE: [2, 683, 1364, 2046], - const.FMT_QUAD: [2, 10923, 21844, 32766], -} - - -def _decimalComponentsToHex(fmt, sign, biased_exp, mantissa): - """Convert sign, biased exponent, and mantissa to 32-bit hex string.""" - b_sign = f"{sign:01b}" - b_exp = f"{biased_exp:0{const.EXPONENT_BITS[fmt]}b}" - b_man = f"{mantissa:0{const.MANTISSA_BITS[fmt]}b}" - b_complete = b_sign + b_exp + b_man - h_complete = f"{int(b_complete, 2):032X}" - return h_complete - - -def _tile_0x5a_pattern(bit_width): - """Create a tiled 0x5A pattern to fill the given bit width.""" - pattern = 0 - for i in range(0, bit_width, 8): - pattern |= 0x5A << i - return pattern & ((1 << bit_width) - 1) - - -def _get_frac_values(fmt): - """Get frac field constants for the format.""" - frac_bits = const.MANTISSA_BITS[fmt] - return { - "0s": 0, - "1s": (1 << frac_bits) - 1, - "00001": 1, - "10000": 1 << (frac_bits - 1), - "any": _tile_0x5a_pattern(frac_bits), - } - - -def _case_1_normal_x_normal(fmt, test_f, cover_f, op): - """Case 1: Normal x Normal (144 vectors per format).""" + +# --------------------------------------------------------------------------- +# 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}" + f"{bexp:0{const.EXPONENT_BITS[fmt]}b}" + f"{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 × ±Normal. 9 cells × 4 sign combos = 36.""" + min_nb, max_nb, frac_max = _fmt_params(fmt) + Z = 0 # all zeros + O = frac_max # all ones count = 0 - fracs = _get_frac_values(fmt) - max_norm_bexp = (1 << const.EXPONENT_BITS[fmt]) - 1 - 1 - - # Exp > cells (3 sig_rel variants) - for sig_rel, frac1, frac2 in [ - ("gt", fracs["any"], fracs["0s"]), - ("<", fracs["0s"], fracs["any"]), - ("=", fracs["0s"], fracs["0s"]), + + # 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 = ]: - for bexp2 in EXP_ANCHORS_LT_MAX[fmt]: - for sign1 in [0, 1]: - for sign2 in [0, 1]: - hex1 = _decimalComponentsToHex(fmt, sign1, max_norm_bexp, frac1) - hex2 = _decimalComponentsToHex(fmt, sign2, 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, - ) - count += 1 - - # Exp < cells (3 sig_rel variants) - for sig_rel, frac1, frac2 in [ - ("gt", fracs["1s"], fracs["any"]), - ("<", fracs["any"], fracs["1s"]), - ("=", fracs["1s"], fracs["1s"]), + 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 [ + (O, _any_frac(fmt)), # sig > + (_any_frac(fmt), O), # sig < + (O, O), # sig = ]: - for bexp2 in EXP_ANCHORS_GT_MIN[fmt]: - for sign1 in [0, 1]: - for sign2 in [0, 1]: - hex1 = _decimalComponentsToHex(fmt, sign1, 1, frac1) - hex2 = _decimalComponentsToHex(fmt, sign2, 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, - ) - count += 1 - - # Exp = cells (3 sig_rel variants, same bexp for both operands) - for sig_rel, frac1, frac2 in [ - ("gt", fracs["1s"], fracs["0s"]), - ("<", fracs["0s"], fracs["1s"]), - ("=", fracs["0s"], fracs["0s"]), + 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 [ + (O, Z), # sig > + (Z, O), # sig < + (Z, Z), # sig = ]: - for common_bexp in EXP_ANCHORS[fmt]: - for sign1 in [0, 1]: - for sign2 in [0, 1]: - hex1 = _decimalComponentsToHex(fmt, sign1, common_bexp, frac1) - hex2 = _decimalComponentsToHex(fmt, sign2, common_bexp, 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, - ) - count += 1 + 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, test_f, cover_f, op): - """Case 2: Normal x SubNormal (48 vectors per format).""" +def _case_2_normal_x_subnormal(fmt: str, op: str, test_f: TextIO, cover_f: TextIO) -> int: + """Case 2: ±Normal × ±SubNormal. 3 cells × 4 sign combos = 12.""" + af = _any_frac(fmt) + bexp1 = _any_exp(fmt) + lsb = 1 # 00..001 count = 0 - fracs = _get_frac_values(fmt) - for sig_rel, frac1, frac2 in [ - ("gt", fracs["any"], fracs["00001"]), - ("<", fracs["0s"], fracs["00001"]), - ("=", fracs["any"], fracs["any"]), + for frac1, frac2 in [ + (af, lsb), # sig > + (0, lsb), # sig < (all zeros vs 00..001) + (af, af), # sig = (same any_frac for both fields) ]: - for bexp1 in EXP_ANCHORS[fmt]: - for sign1 in [0, 1]: - for sign2 in [0, 1]: - hex1 = _decimalComponentsToHex(fmt, sign1, bexp1, frac1) - hex2 = _decimalComponentsToHex(fmt, sign2, 0, 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, - ) - count += 1 + 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, test_f, cover_f, op): - """Case 3: SubNormal x Normal (48 vectors per format).""" +def _case_3_subnormal_x_normal(fmt: str, op: str, test_f: TextIO, cover_f: TextIO) -> int: + """Case 3: ±SubNormal × ±Normal. 3 cells × 4 sign combos = 12.""" + _, _, frac_max = _fmt_params(fmt) + af = _any_frac(fmt) + bexp2 = _any_exp(fmt) + O = frac_max # all ones count = 0 - fracs = _get_frac_values(fmt) - for sig_rel, frac1, frac2 in [ - ("gt", fracs["1s"], fracs["0s"]), - ("<", fracs["any"], fracs["1s"]), - ("=", fracs["any"], fracs["any"]), + for frac1, frac2 in [ + (O, 0), # sig > (all ones vs all zeros) + (af, O), # sig < + (af, af), # sig = (same any_frac for both fields) ]: - for bexp2 in EXP_ANCHORS[fmt]: - for sign1 in [0, 1]: - for sign2 in [0, 1]: - hex1 = _decimalComponentsToHex(fmt, sign1, 0, frac1) - hex2 = _decimalComponentsToHex(fmt, sign2, 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, - ) - count += 1 + 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, test_f, cover_f, op): - """Case 4: SubNormal x SubNormal (20 vectors per format).""" +def _case_4_subnormal_x_subnormal(fmt: str, op: str, test_f: TextIO, cover_f: TextIO) -> int: + """Case 4: ±SubNormal × ±SubNormal. 5 cells × 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 + O = frac_max # all ones count = 0 - fracs = _get_frac_values(fmt) for frac1, frac2 in [ - (fracs["any"], fracs["00001"]), - (fracs["00001"], fracs["any"]), - (fracs["1s"], fracs["10000"]), - (fracs["10000"], fracs["1s"]), - (fracs["any"], fracs["any"]), + (af, lsb), # exp >, sig > + (lsb, af), # exp <, sig < + (O, msb), # exp =, sig > + (msb, O), # exp =, sig < + (af, af), # exp =, sig = (same any_frac) ]: - for sign1 in [0, 1]: - for sign2 in [0, 1]: - hex1 = _decimalComponentsToHex(fmt, sign1, 0, frac1) - hex2 = _decimalComponentsToHex(fmt, sign2, 0, 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, - ) + 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, test_f, cover_f, op): - """Case 5: Zero x Normal (32 vectors per format).""" +def _case_5_zero_x_normal(fmt: str, op: str, test_f: TextIO, cover_f: TextIO) -> int: + """Case 5: ±Zero × ±Normal. 2 cells × 4 sign combos = 8.""" + af = _any_frac(fmt) + bexp2 = _any_exp(fmt) count = 0 - fracs = _get_frac_values(fmt) - - for frac2 in [fracs["any"], fracs["0s"]]: - for bexp2 in EXP_ANCHORS[fmt]: - for sign1 in [0, 1]: - for sign2 in [0, 1]: - hex1 = _decimalComponentsToHex(fmt, sign1, 0, fracs["0s"]) - hex2 = _decimalComponentsToHex(fmt, sign2, 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, - ) - count += 1 + + 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_7_normal_x_zero(fmt, test_f, cover_f, op): - """Case 7: Normal x Zero (32 vectors per format).""" +def _case_7_normal_x_zero(fmt: str, op: str, test_f: TextIO, cover_f: TextIO) -> int: + """Case 7: ±Normal × ±Zero. 2 cells × 4 sign combos = 8.""" + af = _any_frac(fmt) + bexp1 = _any_exp(fmt) count = 0 - fracs = _get_frac_values(fmt) - - for frac1 in [fracs["any"], fracs["0s"]]: - for bexp1 in EXP_ANCHORS[fmt]: - for sign1 in [0, 1]: - for sign2 in [0, 1]: - hex1 = _decimalComponentsToHex(fmt, sign1, bexp1, frac1) - hex2 = _decimalComponentsToHex(fmt, sign2, 0, fracs["0s"]) - run_and_store_test_vector( - f"{op}_{const.ROUND_NEAR_EVEN}_{hex1}_{hex2}_{32 * '0'}_{fmt}_{32 * '0'}_{fmt}_00", - test_f, - cover_f, - ) - count += 1 + + 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_9_zero_x_zero(fmt, test_f, cover_f, op): - """Case 9: Zero x Zero (4 vectors per format).""" +def _case_9_zero_x_zero(fmt: str, op: str, test_f: TextIO, cover_f: TextIO) -> int: + """Case 9: ±Zero × ±Zero. 1 cell × 4 sign combos = 4.""" count = 0 - fracs = _get_frac_values(fmt) - - for sign1 in [0, 1]: - for sign2 in [0, 1]: - hex1 = _decimalComponentsToHex(fmt, sign1, 0, fracs["0s"]) - hex2 = _decimalComponentsToHex(fmt, sign2, 0, fracs["0s"]) - run_and_store_test_vector( - f"{op}_{const.ROUND_NEAR_EVEN}_{hex1}_{hex2}_{32 * '0'}_{fmt}_{32 * '0'}_{fmt}_00", - test_f, - cover_f, - ) + 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 -def generate_b19_tests(test_f, cover_f, fmt): +# --------------------------------------------------------------------------- +# 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: - case1 = _case_1_normal_x_normal(fmt, test_f, cover_f, op) - case2 = _case_2_normal_x_subnormal(fmt, test_f, cover_f, op) - case3 = _case_3_subnormal_x_normal(fmt, test_f, cover_f, op) - case4 = _case_4_subnormal_x_subnormal(fmt, test_f, cover_f, op) - case5 = _case_5_zero_x_normal(fmt, test_f, cover_f, op) - case7 = _case_7_normal_x_zero(fmt, test_f, cover_f, op) - case9 = _case_9_zero_x_zero(fmt, test_f, cover_f, op) - - total = case1 + case2 + case3 + case4 + case5 + case7 + case9 - - print(f" {op}: case1={case1}, case2={case2}, case3={case3}, case4={case4}, " - f"case5={case5}, case7={case7}, case9={case9}, total={total}") + 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) + c7 = _case_7_normal_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 + c7 + c9 + print( + f" {op}: c1={c1} c2={c2} c3={c3} c4={c4} " + f"c5={c5} c7={c7} c9={c9} total={total}" + ) def main(): From d9232dd63581383742172ffde85fad94530c142f Mon Sep 17 00:00:00 2001 From: Sisi Wang Date: Tue, 7 Apr 2026 15:32:42 -0700 Subject: [PATCH 3/8] fixed linter errors for pre-commit check --- src/cover_float/testgen/B19.py | 93 ++++++++++++++++------------------ 1 file changed, 45 insertions(+), 48 deletions(-) diff --git a/src/cover_float/testgen/B19.py b/src/cover_float/testgen/B19.py index 30064f8..dffec91 100644 --- a/src/cover_float/testgen/B19.py +++ b/src/cover_float/testgen/B19.py @@ -5,7 +5,7 @@ # comparison and min/max operations. Test cases are generated for each # combination of exponent and significand relationship constraints. # -# Total vectors: 2500 (100 per format×op, across 5 formats and 5 operations) +# Total vectors: 2500 (100 per format x op, across 5 formats and 5 operations) import random from pathlib import Path @@ -15,7 +15,6 @@ 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] @@ -23,6 +22,7 @@ # 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 @@ -47,19 +47,17 @@ def _any_exp(fmt: str) -> int: 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}" - f"{bexp:0{const.EXPONENT_BITS[fmt]}b}" - f"{frac:0{const.MANTISSA_BITS[fmt]}b}" - ) + 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: +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", + f"{op}_{const.ROUND_NEAR_EVEN}_{hex1}_{hex2}_{32 * '0'}_{fmt}_{32 * '0'}_{fmt}_00", test_f, cover_f, ) @@ -69,18 +67,19 @@ def _emit(fmt: str, op: str, test_f: TextIO, cover_f: TextIO, s1: int, bexp1: in # Case functions # --------------------------------------------------------------------------- + def _case_1_normal_x_normal(fmt: str, op: str, test_f: TextIO, cover_f: TextIO) -> int: - """Case 1: ±Normal × ±Normal. 9 cells × 4 sign combos = 36.""" + """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 - O = frac_max # all ones + 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 = + (_any_frac(fmt), Z), # sig > + (Z, _any_frac(fmt)), # sig < + (Z, Z), # sig = ]: bexp2 = _any_exp(fmt) for s1 in (0, 1): @@ -90,9 +89,9 @@ def _case_1_normal_x_normal(fmt: str, op: str, test_f: TextIO, cover_f: TextIO) # Exp <: bexp1 = min_norm_bexp, bexp2 = any exp for frac1, frac2 in [ - (O, _any_frac(fmt)), # sig > - (_any_frac(fmt), O), # sig < - (O, O), # sig = + (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): @@ -102,9 +101,9 @@ def _case_1_normal_x_normal(fmt: str, op: str, test_f: TextIO, cover_f: TextIO) # Exp =: bexp1 = bexp2 = any exp (same value) for frac1, frac2 in [ - (O, Z), # sig > - (Z, O), # sig < - (Z, Z), # sig = + (ALL_ONES, Z), # sig > + (Z, ALL_ONES), # sig < + (Z, Z), # sig = ]: bexp = _any_exp(fmt) for s1 in (0, 1): @@ -116,16 +115,16 @@ def _case_1_normal_x_normal(fmt: str, op: str, test_f: TextIO, cover_f: TextIO) def _case_2_normal_x_subnormal(fmt: str, op: str, test_f: TextIO, cover_f: TextIO) -> int: - """Case 2: ±Normal × ±SubNormal. 3 cells × 4 sign combos = 12.""" + """Case 2: +/-Normal x +/-SubNormal. 3 cells x 4 sign combos = 12.""" af = _any_frac(fmt) bexp1 = _any_exp(fmt) - lsb = 1 # 00..001 + lsb = 1 # 00..001 count = 0 for frac1, frac2 in [ (af, lsb), # sig > - (0, lsb), # sig < (all zeros vs 00..001) - (af, af), # sig = (same any_frac for both fields) + (0, lsb), # sig < (all zeros vs 00..001) + (af, af), # sig = (same any_frac for both fields) ]: for s1 in (0, 1): for s2 in (0, 1): @@ -136,17 +135,17 @@ def _case_2_normal_x_subnormal(fmt: str, op: str, test_f: TextIO, cover_f: TextI def _case_3_subnormal_x_normal(fmt: str, op: str, test_f: TextIO, cover_f: TextIO) -> int: - """Case 3: ±SubNormal × ±Normal. 3 cells × 4 sign combos = 12.""" + """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) - O = frac_max # all ones + ALL_ONES = frac_max # all ones count = 0 for frac1, frac2 in [ - (O, 0), # sig > (all ones vs all zeros) - (af, O), # sig < - (af, af), # sig = (same any_frac for both fields) + (ALL_ONES, 0), # sig > (all ones vs all zeros) + (af, ALL_ONES), # sig < + (af, af), # sig = (same any_frac for both fields) ]: for s1 in (0, 1): for s2 in (0, 1): @@ -157,20 +156,20 @@ def _case_3_subnormal_x_normal(fmt: str, op: str, test_f: TextIO, cover_f: TextI def _case_4_subnormal_x_subnormal(fmt: str, op: str, test_f: TextIO, cover_f: TextIO) -> int: - """Case 4: ±SubNormal × ±SubNormal. 5 cells × 4 sign combos = 20.""" + """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 + lsb = 1 # 00..001 msb = 1 << (const.MANTISSA_BITS[fmt] - 1) # 10000..000 - O = frac_max # all ones + ALL_ONES = frac_max # all ones count = 0 for frac1, frac2 in [ - (af, lsb), # exp >, sig > - (lsb, af), # exp <, sig < - (O, msb), # exp =, sig > - (msb, O), # exp =, sig < - (af, af), # exp =, sig = (same any_frac) + (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): @@ -181,14 +180,14 @@ def _case_4_subnormal_x_subnormal(fmt: str, op: str, test_f: TextIO, cover_f: Te def _case_5_zero_x_normal(fmt: str, op: str, test_f: TextIO, cover_f: TextIO) -> int: - """Case 5: ±Zero × ±Normal. 2 cells × 4 sign combos = 8.""" + """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) + 0, # sig = (zero frac=0 == all zeros) ]: for s1 in (0, 1): for s2 in (0, 1): @@ -199,14 +198,14 @@ def _case_5_zero_x_normal(fmt: str, op: str, test_f: TextIO, cover_f: TextIO) -> def _case_7_normal_x_zero(fmt: str, op: str, test_f: TextIO, cover_f: TextIO) -> int: - """Case 7: ±Normal × ±Zero. 2 cells × 4 sign combos = 8.""" + """Case 7: +/-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) + 0, # sig = (all zeros == zero frac=0) ]: for s1 in (0, 1): for s2 in (0, 1): @@ -217,7 +216,7 @@ def _case_7_normal_x_zero(fmt: str, op: str, test_f: TextIO, cover_f: TextIO) -> def _case_9_zero_x_zero(fmt: str, op: str, test_f: TextIO, cover_f: TextIO) -> int: - """Case 9: ±Zero × ±Zero. 1 cell × 4 sign combos = 4.""" + """Case 9: +/-Zero x +/-Zero. 1 cell x 4 sign combos = 4.""" count = 0 for s1 in (0, 1): for s2 in (0, 1): @@ -230,6 +229,7 @@ def _case_9_zero_x_zero(fmt: str, op: str, test_f: TextIO, cover_f: TextIO) -> i # 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: @@ -242,13 +242,10 @@ def generate_b19_tests(test_f: TextIO, cover_f: TextIO, fmt: str) -> None: c7 = _case_7_normal_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 + c7 + c9 - print( - f" {op}: c1={c1} c2={c2} c3={c3} c4={c4} " - f"c5={c5} c7={c7} c9={c9} total={total}" - ) + print(f" {op}: c1={c1} c2={c2} c3={c3} c4={c4} c5={c5} c7={c7} c9={c9} total={total}") -def main(): +def main() -> None: """Main entry point for B19 test generation.""" print("Generating B19 test vectors...") with ( From 1d0863946949b51fa964acead0b6ddb03ffae7c5 Mon Sep 17 00:00:00 2001 From: Sisi Wang Date: Tue, 7 Apr 2026 15:35:36 -0700 Subject: [PATCH 4/8] Add newline at end of B19.adoc --- docs/B19.adoc | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/docs/B19.adoc b/docs/B19.adoc index 63839de..a4e9a2e 100644 --- a/docs/B19.adoc +++ b/docs/B19.adoc @@ -738,4 +738,5 @@ The 4 vectors come from the 4 sign combinations: (+0,+0), (+0,−0), (−0,+0), | *Grand Total: 2500* |=== -*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. \ No newline at end of file +*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. + From 585396c69ded312d8dcb8b9851245e8173c63b8d Mon Sep 17 00:00:00 2001 From: Sisi Wang Date: Tue, 7 Apr 2026 15:40:34 -0700 Subject: [PATCH 5/8] Fix end-of-file formatting in B19.adoc(surely this works now right...) --- docs/B19.adoc | 1 - 1 file changed, 1 deletion(-) diff --git a/docs/B19.adoc b/docs/B19.adoc index a4e9a2e..5e9bbac 100644 --- a/docs/B19.adoc +++ b/docs/B19.adoc @@ -739,4 +739,3 @@ The 4 vectors come from the 4 sign combinations: (+0,+0), (+0,−0), (−0,+0), |=== *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. - From 26094906299abeb3c57bd8faf4efe42406a2a130 Mon Sep 17 00:00:00 2001 From: Sisi Wang Date: Thu, 9 Apr 2026 18:56:38 -0700 Subject: [PATCH 6/8] =?UTF-8?q?Add=20B19=20test=20cases=207=20and=208=20fo?= =?UTF-8?q?r=20Zero=20=C3=97=20Subnormal=20and=20Subnormal=20=C3=97=20Zero?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Rename Case 7 to Case 6 (Normal × Zero) - Add Case 7: Zero × Subnormal (1 cell × 4 sign combos = 4 tests) - Add Case 8: Subnormal × Zero (1 cell × 4 sign combos = 4 tests) - Update test count from 100 to 108 per format/operation - Update total from 2500 to 2700 test vectors - Implement test generation logic for new cases in B19.py Made-with: Cursor --- docs/B19.adoc | 184 +++++++++++++++++++++++++++++++-- src/cover_float/testgen/B19.py | 46 +++++++-- 2 files changed, 215 insertions(+), 15 deletions(-) diff --git a/docs/B19.adoc b/docs/B19.adoc index 5e9bbac..21cd65a 100644 --- a/docs/B19.adoc +++ b/docs/B19.adoc @@ -494,7 +494,7 @@ The cells (>, <), (>, =), (<, >), (<, =) are impossible except the five rows sho --- -=== Case 7: ±Normal × ±Zero +=== Case 6: ±Normal × ±Zero [cols="1,1,1,1,1,1",options="header"] |=== @@ -578,6 +578,160 @@ The cells (>, <), (>, =), (<, >), (<, =) are impossible except the five rows sho --- +=== 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 + +| > +| = +| impossible +| +| +| + +| < +| > +| impossible +| +| +| + +| < +| < +| impossible +| +| +| + +| < +| = +| impossible +| +| +| + +| = +| > +| impossible +| +| +| + +| = +| < +| impossible +| +| +| + +| = +| = +| impossible +| +| +|=== + +*Total per precision:* 1 cell × 4 sign combos = **4** + +==== 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 +| +| +| + +| < +| = +| impossible +| +| +| + +| = +| > +| impossible +| +| +| + +| = +| < +| impossible +| +| +| + +| = +| = +| impossible +| +| +|=== + +*Total per precision:* 1 cell × 4 sign combos = **4** + +==== 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"] @@ -694,12 +848,24 @@ The 4 vectors come from the 4 sign combinations: (+0,+0), (+0,−0), (−0,+0), | × 4 | 8 -| 7 +| 6 | Normal × Zero | 2 | × 4 | 8 +| 7 +| Zero × Subnormal +| 1 +| × 4 +| 4 + +| 8 +| Subnormal × Zero +| 1 +| × 4 +| 4 + | 9 | Zero × Zero | 1 @@ -710,7 +876,7 @@ The 4 vectors come from the 4 sign combinations: (+0,+0), (+0,−0), (−0,+0), | | | *Total per (fmt, op):* -| *100* +| *108* |=== === Grand Total Breakdown @@ -720,22 +886,22 @@ The 4 vectors come from the 4 sign combinations: (+0,+0), (+0,−0), (−0,+0), | Format | Total vectors | BF_16 -| 100 per op × 5 ops = 500 +| 108 per op × 5 ops = 540 | FP_16 -| 100 per op × 5 ops = 500 +| 108 per op × 5 ops = 540 | FP_32 -| 100 per op × 5 ops = 500 +| 108 per op × 5 ops = 540 | FP_64 -| 100 per op × 5 ops = 500 +| 108 per op × 5 ops = 540 | FP_128 -| 100 per op × 5 ops = 500 +| 108 per op × 5 ops = 540 | -| *Grand Total: 2500* +| *Grand Total: 2700* |=== *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/testgen/B19.py b/src/cover_float/testgen/B19.py index dffec91..573150c 100644 --- a/src/cover_float/testgen/B19.py +++ b/src/cover_float/testgen/B19.py @@ -5,7 +5,7 @@ # comparison and min/max operations. Test cases are generated for each # combination of exponent and significand relationship constraints. # -# Total vectors: 2500 (100 per format x op, across 5 formats and 5 operations) +# Total vectors: 2700 (108 per format x op, across 5 formats and 5 operations) import random from pathlib import Path @@ -197,8 +197,8 @@ def _case_5_zero_x_normal(fmt: str, op: str, test_f: TextIO, cover_f: TextIO) -> return count -def _case_7_normal_x_zero(fmt: str, op: str, test_f: TextIO, cover_f: TextIO) -> int: - """Case 7: +/-Normal x +/-Zero. 2 cells x 4 sign combos = 8.""" +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 @@ -215,6 +215,38 @@ def _case_7_normal_x_zero(fmt: str, op: str, test_f: TextIO, cover_f: TextIO) -> 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 + + for frac2 in [ + af, # sig < (zero frac=0 < any_frac) + ]: + 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 + + for frac1 in [ + af, # sig > (any_frac > zero frac=0) + ]: + 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 @@ -239,10 +271,12 @@ def generate_b19_tests(test_f: TextIO, cover_f: TextIO, fmt: str) -> None: 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) - c7 = _case_7_normal_x_zero(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 + c7 + c9 - print(f" {op}: c1={c1} c2={c2} c3={c3} c4={c4} c5={c5} c7={c7} c9={c9} total={total}") + 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: From 59ca9d657e5141a8c41b7a871819465d64928a91 Mon Sep 17 00:00:00 2001 From: Sisi Wang Date: Fri, 10 Apr 2026 10:47:46 -0700 Subject: [PATCH 7/8] adjusted the B19.py slightly for better coverage (changes to case 2,3 and 7,8), and changed adoc accordingly Made-with: Cursor --- docs/B19.adoc | 26 +++++++++++++------------- src/cover_float/testgen/B19.py | 24 +++++++++++++++++++----- 2 files changed, 32 insertions(+), 18 deletions(-) diff --git a/docs/B19.adoc b/docs/B19.adoc index 21cd65a..87b5d66 100644 --- a/docs/B19.adoc +++ b/docs/B19.adoc @@ -189,15 +189,15 @@ The frac field values are deterministic constants derived from the format (all z | < | any exp | 0s -| all zeros | 00..001 +| any frac | > | = | any exp | 0s -| any frac -| any frac +| all zeros +| 10...000 | < | > @@ -295,8 +295,8 @@ A normal number has biased exponent ≥ 1, while a subnormal has biased exponent | = | 0s | any exp -| any frac -| any frac +| 10...000 +| all zeros | = | > @@ -600,10 +600,10 @@ The cells (>, <), (>, =), (<, >), (<, =) are impossible except the five rows sho | > | = -| impossible -| -| -| +| 0s +| 0s +| all zeros +| 10...000 | < | > @@ -698,10 +698,10 @@ Subnormal numbers have effective exponents that are strictly negative, while zer | < | = -| impossible -| -| -| +| 0s +| 0s +| 10...000 +| all zeros | = | > diff --git a/src/cover_float/testgen/B19.py b/src/cover_float/testgen/B19.py index 573150c..84711bd 100644 --- a/src/cover_float/testgen/B19.py +++ b/src/cover_float/testgen/B19.py @@ -17,7 +17,6 @@ OPS = [const.OP_FEQ, const.OP_FLT, const.OP_FLE, const.OP_MIN, const.OP_MAX] - # --------------------------------------------------------------------------- # Format helpers # --------------------------------------------------------------------------- @@ -52,7 +51,16 @@ def _build(fmt: str, sign: int, bexp: int, frac: int) -> str: def _emit( - fmt: str, op: str, test_f: TextIO, cover_f: TextIO, s1: int, bexp1: int, frac1: int, s2: int, bexp2: int, frac2: int + 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) @@ -120,11 +128,12 @@ def _case_2_normal_x_subnormal(fmt: str, op: str, test_f: TextIO, cover_f: TextI 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 > - (0, lsb), # sig < (all zeros vs 00..001) - (af, af), # sig = (same any_frac for both fields) + (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): @@ -140,12 +149,13 @@ def _case_3_subnormal_x_normal(fmt: str, op: str, test_f: TextIO, cover_f: TextI 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 < - (af, af), # sig = (same any_frac for both fields) + (msb, 0), # sig = (same any_frac for both fields) ]: for s1 in (0, 1): for s2 in (0, 1): @@ -219,9 +229,11 @@ def _case_7_zero_x_subnormal(fmt: str, op: str, test_f: TextIO, cover_f: TextIO) """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): @@ -235,9 +247,11 @@ def _case_8_subnormal_x_zero(fmt: str, op: str, test_f: TextIO, cover_f: TextIO) """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): From 2e7c083fbc436739af5e67dedba70ae1ab577dda Mon Sep 17 00:00:00 2001 From: Sisi Wang Date: Mon, 20 Apr 2026 23:53:23 -0700 Subject: [PATCH 8/8] Updated B19 coverage, test generation, and adoc. Coverage @ 87.16% --- coverage/covergroups/B19.svh | 40 ++++++++++++++++++------------------ docs/B19.adoc | 26 +++++++++++------------ 2 files changed, 33 insertions(+), 33 deletions(-) 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 index 87b5d66..d90b22a 100644 --- a/docs/B19.adoc +++ b/docs/B19.adoc @@ -647,7 +647,7 @@ The cells (>, <), (>, =), (<, >), (<, =) are impossible except the five rows sho | |=== -*Total per precision:* 1 cell × 4 sign combos = **4** +*Total per precision:* 2 cells × 4 sign combos = **8** ==== Impossibility reasoning @@ -724,7 +724,7 @@ Subnormal numbers have effective exponents that are strictly negative, while zer | |=== -*Total per precision:* 1 cell × 4 sign combos = **4** +*Total per precision:* 2 cell × 4 sign combos = **8** ==== Impossibility reasoning @@ -856,15 +856,15 @@ The 4 vectors come from the 4 sign combinations: (+0,+0), (+0,−0), (−0,+0), | 7 | Zero × Subnormal -| 1 +| 2 | × 4 -| 4 +| 8 | 8 | Subnormal × Zero -| 1 +| 2 | × 4 -| 4 +| 8 | 9 | Zero × Zero @@ -876,7 +876,7 @@ The 4 vectors come from the 4 sign combinations: (+0,+0), (+0,−0), (−0,+0), | | | *Total per (fmt, op):* -| *108* +| *116* |=== === Grand Total Breakdown @@ -886,22 +886,22 @@ The 4 vectors come from the 4 sign combinations: (+0,+0), (+0,−0), (−0,+0), | Format | Total vectors | BF_16 -| 108 per op × 5 ops = 540 +| 116 per op × 5 ops = 580 | FP_16 -| 108 per op × 5 ops = 540 +| 116 per op × 5 ops = 580 | FP_32 -| 108 per op × 5 ops = 540 +| 116 per op × 5 ops = 580 | FP_64 -| 108 per op × 5 ops = 540 +| 116 per op × 5 ops = 580 | FP_128 -| 108 per op × 5 ops = 540 +| 116 per op × 5 ops = 580 | -| *Grand Total: 2700* +| *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.