加藤＠ＯＤＮです．

In article <3990498news.pl@rananim.ie.u-ryukyu.ac.jp>, Shinji KONO wrote:
>河野真治 @ 琉球大学情報工学です。
>> 新城です。loop invariant は、けっこう厳しい。

>> ハードウェアの設計では、形式的な証明の技術を使っているのですか。
>
>まず、作成したLSIの歩止まりを判定しなければならないので、一
>通り(回路毎)のテストを生成する必要があります。LSI設計の限界
>は、それで決まると言われているようですね。
>
>もう一つは、ハードは修正が高く付くことが多いので、ハードは修
>正せずにソフトで対処する... じゃなくて、モデル検証などを使っ
>ても元が取れます。Intel はPentinumの乗算器のミスで痛い目にあ
>ったので力を入れているようですね。

専門家ではありませんが，「使っているのですか」などというレベルではな
く，河野さんが書かれている程度，あるいはそれ以上に重要視されていると
思います．また，自動合成も（部分的ですが）かなり前から使われていま
す．例えば E. E. Times の↓の記事には

http://www.edtn.com/story/OEG20010621S0080

>Intel developed its own tools for debugging the Pentium 4 
>processor, the first project of its kind to which the chip giant 
>applied formal verification on a large scale, said Bob Bentley, 
>manager of presilicon validation for CPU design at Intel's 
>operation in Hillsboro, Ore. 

という一節があります．また，IBM には Verification Laboratory があり
ますし，Intel もイスラエルに同様の研究施設を持っていたと記憶していま
す．
-- 
Hideki Kato <mailto:katoh@pop12.odn.ne.jp>