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

第1節 状態遷移方程式

目次


第1節 状態遷移方程式

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

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


テスト

Logをみる

Back
 

第5章 ハードウェアの意味論的正しさ 第1節 状態遷移方程式

 Flip−Flop(T−Flip−Flop)と呼ぶ回路は次のような状態遷移図で表せます。

この場合、2つしか状態が無いので、状態変数sというものを導入するとsの真理値によって今の状態がどちらであるか分かります。つまりs=0なら状態は0、s=1なら状態は1であると分かります。

 そうしますと、上の状態遷移図は次のような1つの論理式で表せます。

(s=0 imp (T=0 imp s+ =0)&(T=1 imp s+ =1))&(s=1 imp (T=0 imp s+ =1)&(T=1 imp s+ =0)) ...(1)

ここでs+ というのは、「次の状態」を表す変数です。

 上の式の意味は理解できますか? 言葉で言った方が分かりやすいでしょう。

 「状態が0のとき、入力Tが0なら次の状態は0、Tが1なら次の状態は1になる。また状態が1のとき、入力Tが0なら次の状態は1、Tが1なら次の状態は0になる」。 

という言葉を論理式にしたものです。

 その論理式を簡単化しますと(& は and)、

(s or (T or not s+)&(not T or s+))& (not s or (T or s+)&(not T or not s+))

=(s or T & s+ or not s+ & not T)&(not s or T & not s+ or s+ & not T)

=(s or (T eqv s+))&(not s or not(T eqv s+))

=s xor (T eqv s+)

= s xor not(T xor s+)

= not s xor (T xor s+)

= not s xor T xor s+

となります。

 not s xor T xor s+ = True

というのが状態遷移図を表す式です。しかしこの両辺にs+をexclusive or しますと、

 not s xor T xor s+ xor s+ = True xor s+

そして

 not s xor T xor (s+ xor s+) = not s+

従ってまた

 not s xor T xor (False) = not s+

よって

 not s xor T = not s+

両辺にnotを付けると

s+ = not(not s xor T)=not(s eqv T)=s xor T

となります。この

 s+ = s xor T

がこの状態遷移図を表す方程式なのです。状態遷移方程式(state transition equation)あるいは特性方程式(characteristic equation)などと言います。

 試しに、

(not $s implies (not $T implies not $sp)&($T implies $sp))&

($s implies (not $T implies $sp)&($T implies not $sp))

iff ($sp iff $s & not $T or not $s & $T);

という式をMizarでチェックさせますと、エラーは0です(変数s,sp,Tをset型として宣言しておかなくてはなりませんが。またs+ はsp に、= は iff に置き換えました)。

 このことは、状態遷移図を性格付ける言葉を論理式にした長たらしい論理式と状態遷移方程式は同値なのです。

 次の図はJKフリップフロップと呼ばれるものです。出力はQとその否定(Qバー)です。

これの状態遷移方程式または特性方程式は

 Q+ = not Q and J or Q and not K

です。Jがセット端子にあたり、Kがリセット端子にあたります。つまり出力Qが0のときJ=1とすると出力は次に1に変わります。また出力Qが1のときK=1とすると出力は次に0に変わります。

例1 次の回路図の働きはどのようにして解析できるか?

解)3つのJKフリップフロップが使われている。それらの特性方程式と、それぞれのF.F.のJ,K端子へ入力されるゲートの論理式を書き並べる。

Q3+ =not Q3 and J3 or Q3 and not K3;
Q2+ =not Q2 and J2 or Q2 and not K2;
Q1+ =not Q1 and J1 or Q1 and not K1;
J3=not Q1 and Q2;
K3=not(Q1 or Q2);
J2=Q1 and not Q3;
K2=Q1 and Q3;
J1=not(Q2 xor Q3);
K1=(Q2 xor Q3);

ここで (Q3,Q2,Q1) に0と1の組を代入すると上の9つの方程式から (Q3+,Q2+,Q1+) の組が求まる。それが回路の遷移の様子を表すことになる。