MUX の検証：全数検査とプロパティ

何をもって正しいとするか

1 ビットの a・b と選択信号 sel には、全部で 8 組あります。この規模なら全数確認が効率的です。幅 W の MUX^{iマルチプレクサ 選択信号に従い、複数の入力から一つを出力に接続する組合せ回路です。選択ビットと入力番号の対応を仕様で定めます。 詳しく見る} 全体を単純に全数検査すると、選択信号も含めて $2^{2W+1}$ 組になり、少し広くなるだけで別の戦略が必要です。

出力幅 W の各ビットの選択規則は、次の式です。

誤りの種類に合わせて刺激を選ぶ

テスト数が多いだけでは良い検証にはなりません。何の不具合を検出したいか説明できる必要があります。

下は a と b が異なる場合だけの比較です。各列は一つのテストベクトルです。選択を逆にした式は、四列すべてで期待値と反対になります。

参照モデルは実装から独立に作る

DUT のコードをそのままコピーすると、同じ誤りを二度実装する場合があります。仕様の真理値表^{i真理値表 可能な入力組合せをすべて列挙し、各組合せの出力を記した表です。時間に伴う変化は波形で別途確認します。 詳しく見る}やインデックス選択から期待値を作り、q は以前の取込み状態を別に追跡します。不一致が出たら、失敗を保つ最短の入力列へ縮め、原因を説明します。

最終状態だけを比較せず、各観測点の実値・期待値・入力を記録します。この記録が「シミュレーションを実行した」と「仕様を満たした」を区別する根拠になります。