検証と不毛な場合分け

IEEE 754 double準拠のFPUの正しさを検証できる論理学的な手法って存在する／し得るのかな？ ある特定のビットパターンの入力ではand/or素子の列を伝播する誤差が最後の1桁に消えずに残る，みたいなことを防ぎたい．別の言い方をすれば「このときはこうなる」程度の根拠しか持たない場合分けのお化けをどう扱うのか，ってこと．列挙すると2^64通り，またはその自乗！ かと言ってnaiveなHoare風assertionが立てられるとも思えない（むしろバグが混入しやすそうだ）．初期型PentiumのFPUのバグというのは割り算のSRT法というアルゴリズムで使う初期値表が誤っていたせいだそうな．