News Center

回路構成ではなく機能をチェックする、
全く新しい論理等価性検証ツール
—システム設計とRTLでの検証も可能

[issued: 2005.10.05]

この記事を : 印刷する

ブックマーク

メールで送る

　全く新しい論理等価性検証ツールが、業界に受け入れられつつある。米CALYPTO社が2005年4月に発売した「SLEC(Sequential Logic Equivalence Checker)」である。このツールが注目を集めているポイントは、フリップフロップ(FF)などの構成が異なる回路においても、機能の等価性検証が可能な点。
　このツールの等価性検証の手法は従来のものとは全く異なる。対象となる設計ブロックにおいてユーザーが検証したい出力信号を指定すると、ブロックの入力信号値を切り替えていき、出力値の一致をチェックしていく。当然膨大なチェックが必要となるが、同社独自の簡略化手法により、実行が可能になった。結果はテストベンチおよびVCD(Value Change Dump)ファイルとして出力される。

図1　SLECの検証フロー

　RTLおよびネットリストに対してチェックを行っていた従来のツールでは、まず等価性のチェックを行う2つの設計間でFFの対応をチェックする。そして全てのFFの対応が確認できたあとでそのFF情報を全て取り払った設計情報(FF間の論理)同士で、等価性をチェックしていた。そのため、例えば高速動作に向けたパイプライン化を行った場合にはFFのチェック時点で対応が取れず、その結果、等価ではないという結果が出力されていた。検証時に変更内容を入力して回避する方法もあったが、その入力時のミスで正しい結果が得られない危険性も指摘されていた。
　純粋な論理の比較ができるようになったことで、SystemCなどで記述されたシステム設計とRTLとの論理等価性検証も可能になった。これまでは、シミュレーション結果の一致で論理が等価であるとしていたが、大規模回路ではシミュレーションの実行時間が膨大なうえに検証カバレッジ(回路全体に対する、等価性が確認できた回路の比率)を上げることが非常に困難だった。等価性検証ができれば検証カバレッジは100％といえる。

図2　SLECで可能になる等価性検証

　ただし、従来ツールとの置き換えを行った場合、実行時間は増加する。機械的に全FFの対応を取り、その間の論理を比較していた従来のツールにの約2～3 倍かかるという。しかし同社は「確かに論理等価性検証としての時間は増える。だがそれによって削減できるシミュレーション時間を考えれば、どちらが効率的かは明らかだろう」という。そしてさらに、「SLECはこれまでできなかった検証が可能になった全く新しいツールだ。機能強化に向けてRTLを変更した場合の検証や、システム設計とRTLとの等価性検証で威力を発揮する。従来と同じ検証に使用するのであれば、むしろ従来のツールを使用することを推奨する」と言い切った。
　CAPYPTO社によると、現在SLECを使用している設計者は、主にRTL修正前後の論理等価性検証に使用しているという。だが、「このツールの最大の特長は、あくまでもシステム設計とRTLで等価性検証が可能な点」であり、「現在広まりつつあるC言語設計において、この機能の真価が発揮できる」と同社は語っている。
　提供されているツールは「SLEC SYSTEM」と「SLEC RTL」の2種類。SLEC SYSTEMはSystemCで記述したシステム設計やVerilog、VHDLによる設計において等価性検証が可能。C++はSystemCのラッパ (C++で書かれた関数を呼び出す、SystemC記述の関数ブロック)をかぶせることで対応可能。SLEC RTLはVHDL、Verilogで記述された設計における検証が可能で、その機能はすべてSLEC SYSTEMに包含されている。SystemVerilogは今後対応予定。
　現在、ルネサステクノロジ、米Freescale社がSLECの採用を明らかにしている。活用事例報告なども行われる、CAPYPTO社のセミナー「Sequential Equivalence Checking in RTL Verification」は、2005年10月7日に東京都千代田区のジャフコ本社にて行われる。
(鴨川　学)