サクッと書いてサクッと検証？

「サクッと書いてサクッと検証」，富士通九州が米Cadenceの形式検証を評価

Tech-On!の記事より。

現場の人が本当にそう思っているかどうかはちょっと疑問ですが。

この自動チェック機能は設計者に評判がよく，リピータが出たほどと由利氏は述べた。
一方で，プロパティを書くことには，大半の設計者が難色を示していると同氏は述べている。

実際のところこのあたりがネックになってくるんだろう。

設計者をどのように教育していくか？

最終的には自分を助けることにもつながるので、プロパティ記述は設計者も積極的に取り入れたほうが良いと思う。
取り入れることができる環境にあるならばの話だけど。

ただ、状態爆発を起こさないレベルの大きさのモジュール単位でフォーマル検証を使って確実に抑えておくという考え方は確かに正しい。

発見される問題は突き詰めてみると単一のモジュールで閉じてしまっているということがほとんどだからだ。

そこさえ押さえておけば、あとはインタフェースを標準化（規格でもいいし、社内独自のものでもいいだろう）することで生産性はかなり上がると思う。

フォーマル検証が使えなくても、数百行程度のモジュールレベルのRTLであればそれほど時間をかけずに徹底的に動的な検証することもできるだろう。

ただし、設計段階で各モジュールに的確な機能分けを行なって、モジュール間の依存関係をできるだけ小さくしておかないと上記の方法もあまり意味が無くなってしまう。

デザインによって、検証労力も雲泥の差が出てくる。