[2026年7月29日提出]

PDFを表示 HTML（実験的）

概要:リタイミングに続く追加の逐次再合成ステップの検証は既存ツールにとって依然として困難であり、アグレッシブな最適化を制限している。一般的に用いられる等価性検証ツールは内部の再合成操作と、異なるモデルチェッカの誤りやすいオーケストレーションに依存しており、認証を困難あるいは不可能にしている。我々は、リタイミングを前処理ステップとして用い、シミュレーションによって疑似不変条件を生成するIC3ベースの手法を提示する。本手法は、リタイミングおよび任意の強さの逐次再合成下での逐次等価性問題を効率的に検証し、さらに証明書を生成するという特徴を持つ。リタイミングおよび再合成されたオープン回路設計の選定事例における結果は、我々の比較的単純なアプローチが、一般目的の認証付きモデルチェッカの代表として最新のHardware Model Checking Competitionの優勝者ポートフォリオ全体を大幅に上回ることを示している。ABCの成熟した等価チェッカのような非認証アプローチと比較しても、相補的な強みを加えて依然として競争力がある。

提出履歴

投稿者: Tobias Seufert [メールを表示]
[v1] 2026年7月29日 水曜日 22:29:27 UTC (349 KB)