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

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

目次


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

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


テスト

Logをみる

Back
 

第4章 ハードウェアの論理的正しさ 第1節 論理回路のMizarによる表現

 Mizarの論理式の処理能力を使うと、証明、という大げさなものでなく、単にMizarの形式で論理式を記述するだけで、論理回路の正しさのチェックができます。

 そのもとになる理論は、GATE_1 というMizarの論文(=ファイル)です。そこでは論理式の変数は$a,$b,$cのようにアルファベット(あるいは英数字の文字列)の頭に$ をつけて表すようになっています。

 とにかく例をみましょう。

例1 a and b or not a は not a or b と簡単化できるか?

解) これは論理学で公式として習ったので答えはyes だが、Mizarで次のようにして確かめる。

environ
 vocabulary BOOLE, GATE_1;
 notation XBOOLE_0,GATE_1;
 constructors XBOOLE_0;
 clusters XBOOLE_0;
 requirements BOOLE;
begin
reserve a,b,c,d,e,f for set;

$a & $b or not $a iff not $a or $b;

これをチェックさせてエラーが出なければ答えはyes である。実際出ない。もし

$a & $b or not $a iff $a or $b;

とすると *4 のエラーが出る。

なお、環境部はGATE_1.MIZ のものに、GATE_1をnotation部に付け加えたものである。

変数が2つの論理式のときは真理値表を書いても簡単に確かめられますが、変数が10,20となったようなときはMizarによるチェックが役立ちます。

例2 a imp b imp c imp d imp a を簡単化するとTrue か?

解)これをMizarの式にすると

(((($a implies $b) implies $c) implies $d) implies $a) iff not contradiction;

となる。True はnot contradiction になる(False はcontradiction)。またimplies の両側には括弧が必要である。これをチェックすると*4 のエラーが出る。従って答えはno である。

 それでは、例2の簡単化された式は何でしょう? 

 残念ながら、Mizarには論理式を自動的に簡単化する力はないのです。しかし簡単化のための計算式をチェックさすことはできます。

例3 例2の式を簡単化せよ。

解) a imp b imp c imp d imp a 
  =not(a imp b imp c imp d) or a
    = (a imp b imp c)& not d or a
    = (not(a imp b) or c)& not d or a
    = (a & not b or c)& not d or a
    = a & not b & not d or c & not d or a
    = a or c & not d;
実際、

 (((($a implies $b) implies $c) implies $d) implies $a) 
        iff $a or $c & not $d

を チェックさせるとエラーは出ない。

 もしエラーが出るようなら、上の式の変形のどこかで間違っているのだが、それがどこかは上の変形式を6個の等式に分けて書き、一度にチェックさせればよい。間違った箇所にはエラーが出る。

 論理回路の場合、各ゲートを論理演算式に置き換え、全体として最初の仕様通りかチェックすればいいわけです。

例4 a=1 かつ b=1 かつ d=0 のとき出力 f=0 であり、a=0 かつ b=1 かつ d=1 のとき出力 f=1 であり,

a=1 かつ b=0 かつ d=0 のとき出力 f=1 であるような回路を

 f=not b or d

の論理回路で実現した。この回路は正しいか?

解)次の式をチェックすればよい。

 ($f iff not $b or $d) implies
 (($a iff not contradiction) & ($b iff not contradiction)& 
 ($d iff contradiction)implies ($f iff contradiction)) & 
 (($a iff contradiction) & ($b iff not contradiction)& 
 ($d iff not contradiction)implies ($f iff not contradiction)) & 
 (($a iff not contradiction) & ($b iff contradiction)& 
 ($d iff contradiction)implies ($f iff not contradiction));
 a=1 という式は $a iff not contradiction という式に対応します。=は使えません。代わりにiffを使います。1はTrueのことですが、not contradiction

が対応します。

 この回路の正しさは、論理式の同値をいうのでなく、特殊な入力の組み合わせとそのときの出力の指定されて、その通りに設計された回路は働くか、ということが検証されます。つまり、don’t careという、どうでもいい入力の組み合わせに対する出力は無視されます。従って、指定された仕様をみたす回路は複数ありえます。少なくても

 f=not b or d

という論理式に従う回路は仕様を満たす、ということなのです。これが、チェックの式が今までのように同値の式でなく、impliesという包含の式になっている理由です。