等価性チェックのCalyptoが「SLEC」をバージョンアップ-ランタイムが6倍高速に:追記あり

2011年1月10日、シーケンシャル・アナリシス技術でEDA製品を展開する米Calypto Design Systems社は、等価性検証ツール「SLEC」のバージョンアップを発表した。
発表によると新たにリリースされた「SLEC バージョン5.1」では、新しい「deep-loop and stall verification」技術と「"symbolic" memory modeling」技術によりランタイムを6倍に高速化。これにより、これまで時間単位で必要だった検証時間を分単位に短縮することが出来るようになる。
「deep-loop and stall verification」技術とは、Calyptoが「LoopInduction機能」と呼ぶもので、高位合成ツールの合成前後の機能等価性をチェックする際に利用する。これまで信号処理系の回路の等価性検証には、「deep-loop」を考慮した制限や複雑なツール設定が必要であったが、この「LoopInduction機能」を使えばプッシュ・ボタン式に機能等価性を検証する事ができる。
「LoopInduction機能」は、高位合成ツール側からの情報を必要としており、まずはCadenceの高位合成との連携を先行して進めていると昨年のDACの時点で聞いていたが、機能としては汎用的なものであり、特に高位合成ツールを選ぶものではない。
また、「"symbolic" memory modeling」技術とはメモリの抽象化技術で、今回のバージョンアップによって、これまではSLECで取り扱う事が出来なかった大きなメモリを意識することなく容易に取り扱えるようになった。

通常メモリは、フォーマル検証ツールにとっては取り扱いにくい代物でブラック・ボックスとして扱う場合が多いが、SLECはシーケンシャル・アナリシスを行う上でメモリを取り扱うべく抽象化技術に取り組んできた。今回リリースした「"symbolic" memory modeling」技術は、その集大成と言えるもので、「LoopInduction機能」と組み合わせて利用すれば、取り扱えるデザインの幅をかなり広げる事ができる。
プレスリリースにはランタイムが6倍と記載されているが、高速化よりも取り扱えるデザイン規模が大きくなり、更にその幅(種類)も広がったという点が高位合成ユーザーにとっては大きなインパクトとなる。

= EDA EXPRESS 菰田 浩 =
(2011.01.11 )