等価性チェック とは何ですか？

等価性チェック には、3つの基本的な手順があります：

1. 設定
2. マッピング
3. 比較

セットアップへの入力には、検証済みのリファレンスデザイン、ライブラリ要素、および修正済みのデザインが含まれます。このステップでは、これらの入力を読み込み、後続のステップを円滑に進めるためのデータ構造を作成します。

マッピングでは、設計の重要なポイントがマッピングされ、比較されます。比較ポイントを整理するには、通常、ロジックコーンが使用されます。ロジックコーンとは、比較ポイントを駆動する組み合わせ論理回路のブロックです。ロジックコーンへの入力には、レジスタの出力ピン、プライマリ入力ポート、およびブラックボックスの出力ピンが含まれます。比較ポイントには、レジスタ、プライマリ出力ポート、およびブラックボックスの入力ピンが含まれます。

「比較」処理では、マッピングされたキーポイントが、等価か、非等価か、あるいは反転等価かを判定するために検証されます。判定結果が不明確な設計部分については、より詳細な検証を再度実行することで、問題を解決することができます。

以下の図は、そのプロセスを示しています：

等価性チェック あらゆる設計フローに強力な機能を追加します。形式手法を用いて設計の一貫性を検証できることで、テストベンチの網羅性に依存しない、結果の品質に関する洞察が得られます。具体的なメリットは以下の通りです：

• 効率の向上。処理速度の遅いゲートレベルシミュレーションへの依存度の低減。
• 信頼性が高まります。ツールチェーンやECOによって、気づかないうちにエラーが混入してしまうという懸念が軽減されます。
• 品質の向上。この手法により、設計における不適切なRTLコーディングを浮き彫りにすることができます。
• 予測精度が向上。バグを見逃す可能性が低くなります。

論理等価性チェック （LEC）は、設計の組み合わせ構造を分析し、2つの異なる実装の構造が同じ挙動を示すかどうかを判断します。リタイミングなどの操作が設計に適用された場合、2つの表現間の設計構造の対応関係は失われます。

シーケンス等価性チェック（SEC）は、タイミングを考慮に入れ、複数のクロックサイクルにわたって2つの設計表現の等価性を検証する。

シノプシス 提供 Formality 等価性チェック これは、形式的および静的な手法を用いて、設計の2つのバージョンが機能的に同等であるかどうかを判定するものです。