ルネサス システムデザインは、マイコン内の周辺回路の論理機能検証漏れの撲滅を狙って、フォーマルベリファイアー（形式検証ツール）用の検証IPを開発した。その効果や今後の課題について、54th Design Automation Conference（DAC 2017、6月18日～22日、米国Austin）で発表した。講演タイトルは「End-to-End Formal Verification Method for Communication IP Including S/W」（講演番号40.3）である。
登壇した福澤史隆氏によれば、同社では主力製品であるマイコンの設計向けに多数のオンチップ周辺回路を開発している。その論理機能検証において、検証漏れがないようにフォーマルベリファイアーを使う。市場には複数のフォーマルベリファイアーがあり、それに対応可能という検証IPがある。ある程度の論理回路ならば、それを使って、入力パターンの作成なしで、機能検証ができる。
しかし、同氏らの実施したい周辺回路の機能検証は、EDAベンダーが想定するものよりも複雑だ。すなわち、周辺回路のロジック単体の検証ではなく、ファームウエアで制御しながらRTLロジックの機能検証漏れの撲滅を目指す。しかも、RTLロジックはサイクルアキュレートで稼働させるというものだ。こうした検証に対応した検証IPは見当たらず、自ら開発することにした。
今回、モチーフにした周辺回路は2つある。共に小規模な通信回路で、1つが7Kゲート。もう1つが10Kゲートである。開発した検証IPは2種類ある。1つは通信処理を検証するもので、通信プロトコルごとに別の検証IPが必要だという。もう1種類は、ファームエウア（バス）からDUT（検証対象回路）を制御するための検証IPで、バスアーキテクチャー（現在は同社独自のマイコン用オンチップバス）が変わらない限り再利用できるとする。
