情報証明論 第5章 ハードウェアの意味論的正しさ

第1節 状態遷移方程式

目次


第1節 状態遷移方程式

 第2節 カウンタ回路の正しさ

 第3節 場合の数が多すぎるときは証明を


テスト

Logをみる

Back
 

第5章 ハードウェアの意味論的正しさ 第2節 カウンタ回路の正しさ

 前節の状態遷移図で表したT−Flip−Flopを考えます。これを下図のブロック図のように4つ並べてみます。

下位のFlip−Flopの出力(それは状態の値です)を上位のFlip−Flopの入力線(変数Tで表せる)に何らかの回路を通して繋いで入力させます。

 すると、0000,0001,0010,0011,0100,0101,0110,0111,1000,1001,1010,1011,1100,1101,1110,1111,0000

のような順で、クロックパルスを入れて、最下位のT入力に1を与える度に、カウントアップしてゆくでしょうか? 各桁の値は各Flip−Flopの状態値であるとします。

 s0+=s0 xor T

  (s1=0 imp (s0=1 & T=1 imp s1+ =1)&(not(s0=1& T=1) imp s1+=0))&
  (s1=1 imp (s0=1 & T=1 imp s1+ =0)&(not(s0=1& T=1) imp s1+=1))
この式は前節の、Flip−Flopの働きを説明した(1)式と似ています。(1)式のT=1 の代わりにs0=1& T=1 を代入すれば同じになります。従って同じような式の変形により

s1+=s1 xor (s0 & T)

という方程式が得られます。これは右から2番目のFlip−FlopのT−入力端子には、最下位の出力s0と最下位への入力Tとのand をとって入力させなさい、ということを表します。

 同様に考えますと(3番目のFlip−Flopの状態が変わるのは、T,s0,s1,s2がみな1のとき)、

 s2+=s2 xor (s1 & s0 &T)

また4番目は、

 s3+=s3 xor (s2 & s1 & s0 & T)

となります。これを回路にしますと下図のようになります。

これが正しくカウントアップするかどうか、やはりMizarで確かめましょう。ここで ${} はFalse の役をします。Mizarではcontradiction がFalse なのですが、長いのでGATE_1 で${} が代わりに使えるようになっています。Trueは not ${} とするしかありません。またand ゲートの出力を右からa0,a1,a2 としています。

($s3 iff ${}) & ($s2 iff ${}) & ($s1 iff ${}) 
                    & ($s0 iff ${}) & ($T iff ${}) &
 ($sp0 iff $s0 & not $T or not $s0 & $T) & 
 ($a0 iff $s0 & $T) &
 ($sp1 iff $s1 & not $a0 or not $s1 & $a0) &
 ($a1 iff $s1 & $s0 & $T) &
 ($sp2 iff $s2 & not $a1 or not $s2 & $a1) &
 ($a2 iff $s2 & $s1 & $s0 & $T) &
 ($sp3 iff $s3 & not $a2 or not $s3 & $a2)
 implies
 ($sp3 iff ${}) & ($sp2 iff ${}) & ($sp1 iff ${}) & ($sp0 iff ${});

これはエラー0となります。つまり出力が0000のとき入力T が0である限り、出力も0000であることを表しています。

 そこで今度はTを1にしてみます。

($s3 iff ${}) & ($s2 iff ${}) & ($s1 iff ${}) 
       & ($s0 iff ${}) & ($T iff not ${}) &
 ($sp0 iff $s0 & not $T or not $s0 & $T) & 
 ($a0 iff $s0 & $T) &
 ($sp1 iff $s1 & not $a0 or not $s1 & $a0) &
 ($a1 iff $s1 & $a0) &
 ($sp2 iff $s2 & not $a1 or not $s2 & $a1) &
 ($a2 iff $s2 & $a1) &
 ($sp3 iff $s3 & not $a2 or not $s3 & $a2)
 implies
 ($sp3 iff ${}) & ($sp2 iff ${}) & ($sp1 iff ${}) & ($sp0 iff not ${});

 これもノーエラーです。つまり T=1 なら 0000 の次は 0001 になります。

 同様に 0111 の次は 1000 ということと、 1111 の次は 0000 を続けてチェックしましょう。

($s3 iff ${}) & ($s2 iff not ${}) & ($s1 iff not ${}) 
       & ($s0 iff not ${}) & ($T iff not ${}) &
 ($sp0 iff $s0 & not $T or not $s0 & $T) & 
 ($a0 iff $s0 & $T) &
 ($sp1 iff $s1 & not $a0 or not $s1 & $a0) &
 ($a1 iff $s1 & $a0) &
 ($sp2 iff $s2 & not $a1 or not $s2 & $a1) &
 ($a2 iff $s2 & $a1) &
 ($sp3 iff $s3 & not $a2 or not $s3 & $a2)
 implies
 ($sp3 iff not ${}) & ($sp2 iff ${}) & ($sp1 iff ${}) & ($sp0 iff ${});

($s3 iff not ${}) & ($s2 iff not ${}) & ($s1 iff not ${}) 
       & ($s0 iff not ${}) & ($T iff not ${}) &
 ($sp0 iff $s0 & not $T or not $s0 & $T) & 
 ($a0 iff $s0 & $T) &
 ($sp1 iff $s1 & not $a0 or not $s1 & $a0) &
 ($a1 iff $s1 & $a0) &
 ($sp2 iff $s2 & not $a1 or not $s2 & $a1) &
 ($a2 iff $s2 & $a1) &
 ($sp3 iff $s3 & not $a2 or not $s3 & $a2)
 implies
 ($sp3 iff ${}) & ($sp2 iff ${}) & ($sp1 iff ${}) & ($sp0 iff ${});

どちらにもエラーが出ませんので、これもOKです。このようにして2の4乗×2回(Tが0と1の場合がある)=32回チェックすればいいことになります。

 Mizarにとっては32回チェックすることは容易なことです。しかし手で入力しているとタイプミスが入り易いといえます。この種のチェックにはなるべく人手が入らないような工夫が必要です。例えばLSIの設計CADに入力されている論理式をプログラムなどで自動的にMizarの形式に落とす、などがいいでしょう。

 その変換プログラムにバグがあったら何にもならないのですが、もしバグがあれば変換された式をMizarに入れたときにおかしなエラーがでるでしょうから、気づく公算は大きいのです。