ルネサス エレクトロニクスは、マイコンの多品種並行開発をフォーマル検証で効率化していることに関して、検証技術の専門セミナー「Verify2013」（2013年9月27日に新横浜で開催）で講演した。登壇したのは、同社の清水徹氏（第一事業本部グローバル事業戦略統括部 主幹技師長）である。
マイコン事業では、ベースとなる製品から少し仕様が異なる派生品を多数そろえる、いわゆるシリーズ展開が一般的である（図１）。プロセサ・コアやDMAコントローラやバスなどは共通しているが、メモリ容量や周辺回路が異なる。パンフレットやWebサイトに載っている全品種がそれぞれ異なるダイというわけではないが、それでも似たようなダイを多数開発する必要がある。
設計作業は、いわゆるプラットフォーム化、IPコア化で効率化が図られている（図2）。すなわち、ベースとなる製品を設計する際に、全派生品で共通となるプラットフォーム（プロセサ・コアやDMAコントローラなど）、およびいくつかの派製品で使う周辺回路をIPコア（タイマーやUART、CAN、USBなど）としてライブラリに登録していく。これらを組み合わせることで、多数の派製品を短期間で設計する。
厄介なのが、派製品の検証である（図3）。それぞれが1つの製品として、きちんと動作するかどうかを検証しなければならない（図4）。IPコアの追加や削減を行った際、IPコア間が単に接続されているかどうかは容易にチェックできる。しかし、IPコアを追加したり削減したりすれば、チップ全体の割り込み処理やバスの制御などに影響が出る。バスで衝突が発生しないか、割り込み処理が仕様通りに実行されるかなどをチェックしなければならない。
さらに、ルネサスならではの事情もある。ルネサスはNEC、日立製作所、三菱電機の半導体部門が統合して誕生した会社。開発元が異なるIPコアを1チップに載せるケースはよく発生し、間違いを起こさない製品を提供するために、IPコアを統合した後のチェックは重要度が高い。
