情報証明論 第4章 ハードウェアの論理的正しさ  

第2節 状態遷移図のMizarによる論理検証

目次


第1節 論理回路のMizarによる表現

第2節 状態遷移図のMizarによる論理検証


テスト

Logをみる

Back
 

第4章 ハードウェアの論理的正しさ 第2節 状態遷移図のMizarによる論理検証

 順序回路と呼ばれる、記憶をもった論理回路は、状態遷移図(state transition diagram)で表すことができます。例えば下図のような図です。

 2重丸をつけた0という状態は初期状態であることを示します。

 またelseというのは他の状態へ遷移する条件以外の条件、という意味です。例えば状態1のところのelseは、状態2へ遷移する条件 A=0 & B=0 と、状態4へ遷移する条件A=1 & B=0 以外の条件ですので、not(A=0 & B=0 or A=1 & B=0) という論理式で表せる条件を指します。

これは次のようなブロック図の回路を想定しています。

 出力fについては遷移図に書きこまれていませんが、状態によって一意に定まる適当な値です。例えば奇数状態なら1、偶数状態なら0などと定めることができます。

 この回路にはCpと書いたクロックパルスが入力されています。つまり「同期式 synchrobous」と呼ばれる順序回路です。入力はA,Bの2本です(クロックのパルスCpが立ち下がるときに入力A,Bがサンプリングされ、パルスが立ちあがるときに状態が変わり同時に出力もそのタイミングで変わるとします)。

 またRstという入力はリセット用で、これを1とすると状態は初期状態0になります。 

状態遷移図が正しい、というのはどういうことか考えてみましょう。まずシステムがこのようにいくつかの状態をもったものと考えるのが適切であるか、という意味論的な問題があります。それはまた別の機会に論じるとして、ここでは状態遷移図の論理的正しさを考えることにしましょう。

 1)状態遷移はあいまいでない。つまりある入力の組み合わせに対し一意に次の状態が決まる。

 2)どの状態も到達可能である。つまり任意の状態sに対して、ある入力列を入力すると初期状態からsに何段階かを経て到達する。

1)に対しては、どの状態をとっても、そこから各状態へ遷移する条件は「互いに排反 はいはん mutually disjoint」でなくてはいけません。条件gと条件hが互いに排反というのは g and h = False となる、ということです。

elseの付いたところは、それ以外ということで、他へ遷移する条件をorでつないで、全体にnotをつけたものなので、特にチェックはいりません。

 状態0からは1に遷移するだけなので、問題無し。状態2,3,4も問題無し。状態1だけが2へ遷移する場合と、状態4へ遷移する場合があります。従って、それらの遷移条件をandで結んだものがFalseであればいいことになります。即ち、

   (A=0 & B=0)&(A=1 & B=0) = False

が言えればいいのです。これをMizarの形式で書きますと、

(($A iff contradiction)&(($B iff contradiction))&(($A iff not contradiction)&($B iff contradiction)) iff contradiction;

をチェックすればいいのです。あるいは

   (not $A & not $B)&($A & not $B) iff contradiction;

をチェックしてもいいのです。これらはチェックするまでもなく明らかでしょうが、遷移図がより複雑になったときはMizarによるチェックは有効になります。

 2)に対しては遷移図を一目見て、孤立した状態群(矢印を辿っては入れない状態)が無ければまずは合格です。しかし、矢印があって一見遷移できるように見えても、「入力条件 input condition」というものがあるときがあって、入力の組み合わせにある種のものは現れない、ということが分かっている場合もあります。すなわち入力はある条件 ic を満たしている、という場合です。

 例えば入力条件が ic=A or B としましょう。そのとき状態1から状態2へ遷移する条件 (A=0 & B=0)は成立しません。それは

  ($A or $B)&(not $A & not $B) iff contradiction;

がノーエラーになることから分かります。このときのチェックは「エラーが出なければおかしい」という今までと逆のものです。例えば

状態1から状態4へ遷移する条件については、

  ($A or $B)&($A & not $B) iff contradiction;

は*4のエラーが出ますので、ちゃんと遷移しうる、ということが分かります。

 この場合状態2と状態3は図に描かれていても、取られることの無い状態である、ということになります。これは回路を複雑にするだけで意味がない、ということですが、それ以上に、何か考え違いがある可能性がある、ということです。

 Mizarでは恒真命題はエラー0の正しい命題として判断できます。従ってnotをつければ恒偽命題も判断できます。それ以外はnotを付けても付けなくてもエラーとして表示されるので、恒真でも恒偽でもない、と判断できるわけです。