frontend/testfloat_expr の設計

設計目標

Berkeley TestFloat¹1 J. R. Hauser, Berkeley TestFloat and Berkeley SoftFloat, release 3e. は、SoftFloat リファレンス実装から、すべての形式・丸め方向・極小性（tininess）モードについて IEEE 754 の 2 進算術のテストベクトルを生成します。このパッケージはそのようなベクトルを bin_float に対して実行し、結果と例外フラグをビット単位で正確に比較します。これは bin_float の適合性における IEEE 754 に関する主張の根拠です。パッケージは純粋であり、ベクトルの生成とプロセスのオーケストレーションは tools/ にあります。

数学的背景

形式と符号化

幅 $k$、精度 $p$、最大指数 $e_{\max}$ を持つ 2 進交換形式（binary16: $(16, 11, 15)$、binary32: $(32, 24, 127)$、binary64: $(64, 53, 1023)$、binary128: $(128, 113, 16383)$、ただし $e_{\min} = 1 - e_{\max}$）は、$\pm 0$、非正規化数、正規化数、$\pm\infty$、NaN を表現します。その符号化 $\operatorname{enc} : \mathbb{F} \to \{0,1\}^k$ は NaN 以外の値に対して単射であり、$+0$ と $-0$ を区別します。TestFloat はオペランドと結果を $\operatorname{enc}$ の 16 進表記で書きます。

正しく丸められた演算とフラグ

演算 $\mathrm{op}$ とオペランド $x$ に対し、IEEE 754 は、形式へ方向 $\rho$ で 1 回だけ丸めた結果 $r = \circ_\rho(\mathrm{op}(x))$ と、次の例外の集合を要求します²2 IEEE 754-2019 の第 7 節（例外）、第 7.5 節（アンダーフローと 2 つの極小性規則）、第 3.4 節（2 進交換形式の符号化）。 。

• 意味のある結果を持たない演算に対する invalid（たとえば $\infty \cdot 0$、$\sqrt{-1}$、signaling NaN のオペランド、範囲外の整数変換）。
• 有限のオペランドから正確な無限大の結果が得られた場合の division by zero。
• 非有界な指数で丸めた結果が最大の有限数を超える場合の overflow。
• 結果が極小かつ不正確な場合の underflow。極小性は 丸め前（$0 < |\mathrm{op}(x)| < 2^{e_{\min}}$）または 丸め後（$0 < |\circ_\rho^{\,p,\infty}(\mathrm{op}(x))| < 2^{e_{\min}}$、非有界な指数で $p$ ビットに丸める）のいずれかで検出されます。
• $r \ne \mathrm{op}(x)$ の場合の inexact。

SoftFloat はこれらをマスク $\text{inexact} = 1$、$\text{underflow} = 2$、$\text{overflow} = 4$、$\text{infinite} = 8$、$\text{invalid} = 16$ として報告し、2 桁の 16 進数で出力します。BinaryFlags::to_testfloat_bits は同じマスクを生成します。

合格規則

$\hat r$ を format.context(rounding~, tininess~) で計算した bin_float の結果、$\hat F$ をそのフラグ、$(e, M)$ を期待される符号化とマスクとします。算術演算では、実行器は $\hat r$ を形式で再符号化して $\operatorname{enc}(\hat r)$ とフラグ $F_{\mathrm{enc}}$ を得て、次の場合にベクトルが合格します。

$$\Bigl( \bigl(e \text{ is a NaN} \wedge \hat r \text{ is a quiet NaN}\bigr) \vee \operatorname{enc}(\hat r) = e \Bigr) \;\wedge\; \operatorname{mask}(\hat F \cup F_{\mathrm{enc}}) = M .$$

整数変換では、値の検査が次のものに置き換わります。$16 \in M$ ならば変換は invalid を報告しなければならず、そうでなければビットパターンが $e$ である整数を返さなければなりません。比較演算では真偽値の等価性です。フラグのマスクは常に等しくなければなりません。

設計上の判断

ビット単位で正確な結果と、クラスによる NaN の判定

符号化を比較することで、ゼロの符号、非正規化数とゼロのどちらになるか、オーバーフローの正確な境界が、すべてのテストの対象になります。NaN は例外です。IEEE 754 は無効演算によって生成される NaN のペイロードと符号を実装に委ねている（SoftFloat の既定 NaN は独自のパターンを持つ）ため、期待値が NaN の場合、実際の結果は quiet NaN でありさえすればよいとします。結果が signaling NaN であれば不合格となり、これは IEEE の要求どおりです。

フラグマスクの完全一致

マスクの比較は等価性の判定なので、inexact の欠落や余分な underflow があればベクトルは不合格になります。再符号化ステップのフラグを合わせることで、bin_float が形式で正確に保持できない値を返した場合に、符号化のフラグがそれを明らかにします。

無効な変換はフラグのみで判定する

無効な整数変換に対して、SoftFloat はプラットフォーム依存の番兵整数を返しますが、bin_float は整数の結果がないことを示すために None を返します。そのため実行器は、期待されるマスクに invalid ビットがある場合にちょうど None を要求し、番兵値は無視します。それ以外の変換はすべて整数のビットパターンとして比較されます。

ドキュメントごとに 1 つの仕様

TestFloat の 1 回の実行は、1 つの関数、丸めモード、極小性モード、正確性についてのベクトルを生成します。これらを TestFloatSpec に一度だけ記録することで、ベクトルの行を TestFloat 自身の形式のまま保てるため、testfloat_gen のファイルを変更せずに使用できます。

ベクトルの添字によるシャーディング

ベクトル $k$ はシャード $k \bmod n$ に属します。gda_expr の設計と同様に、シャードは互いに素でファイル全体を覆い、サイズは $\lceil (N-i)/n \rceil$ であり、各ベクトルの結果は他のベクトルから独立しているため、統合したシャードのカウントは逐次実行のカウントと等しくなります。

正しさ／不変条件

合格の健全性。 期待されるベクトルが正しければ、算術ベクトルが合格することは、NaN のペイロードを除いて、bin_float が正しく丸められ正しく符号化された結果を返し、IEEE の例外を過不足なく発生させたことを示します。

カウンタの恒等式。 選択されたすべてのベクトルが実行されます。$\text{selected} = \text{passed} + \text{failed}$ であり、$\text{total} = N$ はドキュメント中のベクトル数です。

全域性。 解析はすべての行をベクトルまたは診断に変換します。アリティは演算に対して検査されるため、実行時にオペランド数の誤ったベクトルに出会うことはありません。

計算量。 ベクトルあたり 1 回の bin_float 演算と 1 回の符号化であり、ベクトル数に対して線形です。

却下した代替案

• 復号した値を数値的に比較すること。 $+0$ に対して $-0$ を受け入れてしまい、非正規化数における符号化の誤りを隠してしまいます。
• SoftFloat の NaN パターンを要求すること。 それは IEEE 754 ではなく、SoftFloat の実装上の選択をテストすることになります。
• SoftFloat の無効変換の番兵値を要求すること。 番兵値はプラットフォームによって異なり、無効な結果を None として報告する API では意味を持ちません。

境界

• binary16/32/64/128 と TestFloatOperation の 18 個の演算のみを扱います。形式間の変換、10 進文字列との相互変換、整数からの変換はありません。
• IEEE の 5 つの丸め方向のみを扱います。TestFloat の round-to-odd は TestFloatSpec::parse によって拒否されます。
• NaN のペイロードと符号は比較されません。
• ファイルの読み取り、ベクトルの生成、宣言されたマトリクスは cli/testfloat_expr_cli と tools/run_binfloat_interpreter.py が扱います。

Footnotes

1. J. R. Hauser, Berkeley TestFloat and Berkeley SoftFloat, release 3e. ↩

2. IEEE 754-2019 の第 7 節（例外）、第 7.5 節（アンダーフローと 2 つの極小性規則）、第 3.4 節（2 進交換形式の符号化）。 ↩