Z言語(記法)

　ふとトランスピュータのことを調べていたらここに当たった。
http://members.jcom.home.ne.jp/1355/Transputer.htm

「注目すべき点としてTransputerの設計上のバグは全く見られなかったことであります。」　なんですと！？

Z言語 - Wikipedia
http://it.impressbm.co.jp/e/2009/10/02/1329
Formal Methods Wiki | FANDOM powered by Wikia

　Z記法による仕様書記述から誤りなく実装できるのか。わからんが経験した大規模なLSI設計ではこんな感じだった。仕様書が最初に作製され、それを元に回路図が作られる。これはまだディレイ改善などの工夫を入れていない、設計者が理解しやすい図面である。これを元に実際の論理回路が組まれる。仕様と最初の回路図との違いや実際の論理回路との違いは設計者が図面チェックといって蛍光ペンで塗りつぶしていた。そして論理シミュレータでたくさんのテストパターンを流して検証した。論理シミュレーションをやっているとどうしても100%の検証にはならないことがわかる。反例が1つでも出たら間違いなのだ。
　他には形式検証(フォーマル・ベリフィケーション)を使った。これは元となる回路といじった回路をシミュレーションではなく構造を比較して一致しているかどうかを調べるものだった。できたばかりでよく記憶保護例外起こしてたけど。
　最終的な検証は論理シミュレータをぶん回してこれだけやりました！ってことでOKと判断していたのだが、最近は変わったのだろうか？(脳筋な人々だから変わってない方に五百点)

〈ANIMEX1300 Song Collection シリーズ〉(5)ぼくらのマジンガーZ