IP価値を高める「フォーマル・ベリフィケーション・ツール」

EETimes からViewpoint: Maximizing the value of your IPという記事の要約を紹介．これは，Jasper Design Automation Inc.のフォーマル・ベリフィケーション・ツールの広告記事．

現状，RTLの再利用が加速している（現在チップの3分の1，これが，2015年には50％まで増加すると予測されている）．そこで問題になるのは，レガシーRTLの検証工数過小見積もりによる，工数爆発．仕様書やテストベンチがあるが，結局信用できるのはコード（RTL）そのもの．

既存のテストベンチの問題点については，「RTLそのものよりもデカい検証環境がそんざいすることはよくあること」と書かれている．

there typically exists an enormous verification environment that is larger than the RTL itself

これは，私の経験でも実際見てきた．RTLも巨大だったが，テストベンチのコードは超大盛りのスパゲッティであった．

RTLに手を入れる必要があるときに，そんなテストベンチと格闘するのは無駄．代わりにフォーマル・ベリフィケーション・ツールを使って，RTLの動作が変わっていないことを保証すべし．これが実現できれば，IPの再利用は格段にやりやすくなる．つまり，IPの資産価値が高まる，というわけ．

A revolutionary approach to answering these time-wasting reuse questions is to decouple the RTL from the large, unwieldy, constrained-random simulation testbench and extract answers from the design itself, through a new application of formal verification technology called Behavioral Indexing.

私の感想
私の前職で，ビデオ・コーデックの開発に関わっていたときには，フォーマル・ベリフィケーションは一部で使用されていたにすぎない．まあ，ほとんどのモジュールが新規だったので，そうなるのもしかたない．でも，実際にあのIPを再利用するために，フォーマル・ベリフィケーションにかけたとしても，時間がかかりすぎて，使い物にならないだろう．RTLそのものも，検査性を考えた設計にしていかねば，効率のいい開発は望めないだろう．この辺は，ソフトウェア開発と同じだ．