2005.11

システム設計とRTLでの検証も可能な 論理等価性検証ツール

Advertisement 　全く新しい論理等価性検証ツールが、設計者の注目を集めている。米CALYPTO社が2005年4月に発売した「SLEC（Sequential Logic Equivalence Checker）」である。現在、ルネサステクノロジ、米Freescale社が採用を明らかにしている。このツールが注目を集めているポイントは、フリップフロップ（FF）などの構成が異なる回路においても、機能の等価性が検証できる点である。 　このツールの等価性検証の手法は従来のものとは全く異なる。対象となる設計ブロックにおいてユーザーが検証したい出力信号を指定すると、その出力に関する全ブロックの入力信号値を切り替えていき、出力値の一致をチェックしていく。当然膨大なチェックが必要となるが、同社独自の簡略化手法により、実行が可能になった。結果はテストベンチおよびVCD（Value Change Dump）ファイルとして出力される。 　従来のツールでは、RTLやネットリストにおいて、FFの対応をチェックしていた。そして全てのFFの対応が確認できた後、FF間の論理同士で、等価性をチェックしていた。そのため、例えば高速動作に向けたパイプライン化を行った場合にはFFのチェック時点で対応が取れず、等価ではないという結果が出力されていた。検証時に変更内容を入力して回避する方法もあったが、入力ミスの危険性も指摘されていた。 　純粋な論理の比較ができるようになったことで、SystemCなどで記述されたシステム設計とRTLとの論理等価性検証も可能になった。これまでは、シミュレーション結果の一致で論理が等価であるとしていたが、大規模回路ではシミュレーションの実行時間が膨大なうえに検証カバレッジ（回路全体に対する、等価性が確認できた回路の比率）を上げることが非常に困難だった。等価性検証ができれば検証カバレッジは100％といえる。 　ただし、従来ツールとの置き換えを行った場合実行時間は増加する。機械的に全FFの対応を取り、その間の論理を比較していた従来ツールの約2〜3倍かかるという。しかし同社は「確かに論理等価性検証としての時間は増える。だがそれによって削減できるシミュレーション時間を考えれば、どちらが効率的かは明らかだろう」という。そしてさらに、「SLECはこれまでできなかった検証が可能になった全く新しいツールだ。従来と同じ検証に使用するのであれば、むしろ従来のツールを使用することを推奨する」と言い切った。同社によると、現在SLECを使用している設計者は、主にRTL修正前後の論理等価性検証に使用しているという。だが、「このツールの最大の特長は、あくまでもシステム設計とRTLで等価性検証が可能な点」であり、「現在広まりつつあるC言語設計において、この機能の真価が発揮できる」と同社は語っている。 （鴨川 学） 図1　SLECの検証フロー 図2　SLECで可能になる等価性検証