Alloy による組み合わせ回路のモデリング

alloy_combilogic.als

// ************************************
//   組み合わせ回路のモデル
// ************************************

// ------------------------------------
//   組み合わせ回路の性質
// ------------------------------------

// 回路の構成要素
abstract sig Element {
    source : set Element  // 自分の上流側に接続されている要素
}

// 入力信号と出力信号
sig Input, Output extends Element {}

// 基本論理ゲート (NOT, OR, AND)
abstract sig Gate extends Element {}
sig NotGate, OrGate, AndGate extends Gate {}

// 各要素の接続に関する制約
fact circuitLayout {
    // 組み合わせ回路は状態を保持しないため、接続は循環しない
    no e : Element  | e in e.^source
    // 出力以外の要素は他の要素の入力となる
    all e : Element - Output | some source.e
    // 出力は他の要素の入力にならない
    all o : Output  | source.o = none
    // 入力は上流側要素を持たない
    all i : Input   | i.source = none
    // 出力は上流側要素をちょうど 1 個持つ
    all o : Output  | one o.source
    // NOT ゲートは上流側要素を 1 個だけ持つ
    all n : NotGate | one n.source
    // OR, AND ゲートは上流側要素をちょうど 2 個持つ
    all g : OrGate + AndGate | #g.source = 2
}

// 各構成要素への真偽値の割り当て
sig State {
    true  : set Element,  // 真になっている要素の集合
    false : set Element   // 偽になっている要素の集合
}

// 真偽値の割り当てに関する制約
fact booleanAssignment {
    // 各要素は真 / 偽のうちどちらか一方の状態を取る
    all s : State {
        s.true & s.false = none
        s.true + s.false = Element
    }
    /*
     * 生成公理 : 入力としてすべての割り当てが生じる
     * 今回はスコープに exactly を付加することで対処
     * このため、Input を存在量化する場合は disj 指定が必須
     */
    all disj s1, s2 : State | s1.true & Input != s2.true & Input
}

// 論理演算に関する制約
fact gateOprations {
    all s : State {
        // 出力値が真 <=> 出力の上流要素が真
        all o : Output  | o in s.true <=> o.source in s.true
        // NOT ゲートが真 <=> ゲートの上流要素が真でない
        all n : NotGate | n in s.true <=> n.source not in s.true
        // OR ゲートが真 <=> ゲートの上流要素の少なくともひとつが真
        all o : OrGate  | o in s.true <=> o.source & s.true != none
        // AND ゲートが真 <=> ゲートの上流要素がすべて真
        all a : AndGate | a in s.true <=> a.source in s.true
    }
}


// ------------------------------------
//   具体的な回路の設計
// ------------------------------------

// XOR 回路
pred xor {
    some disj in1, in2 : Input, out : Output | all s : State {
        (in1 in s.true  && in2 in s.true ) => out in s.false
        (in1 in s.true  && in2 in s.false) => out in s.true
        (in1 in s.false && in2 in s.true ) => out in s.true
        (in1 in s.false && in2 in s.false) => out in s.false        
    }
}
run xor for 4 Gate,  exactly 2 Input, exactly 1 Output, exactly 4 State

// 2 bit デコーダ
pred decoder {
    some disj in1, in2 : Input, disj out0, out1, out2, out3 : Output |
        all s : State {
            (in1 in s.false && in2 in s.false) => Output & s.true = out0
            (in1 in s.true  && in2 in s.false) => Output & s.true = out1
            (in1 in s.false && in2 in s.true ) => Output & s.true = out2
            (in1 in s.true  && in2 in s.true ) => Output & s.true = out3
        }
}
run decoder for 6 Gate, exactly 2 Input, exactly 4 Output, exactly 4 State

// 半加算器
pred halfAdder {
    some disj in1, in2 : Input, disj ans, cOut : Output | all s : State {
        (in1 in s.true  && in2 in s.true ) => (ans in s.false && cOut in s.true )
        (in1 in s.true  && in2 in s.false) => (ans in s.true  && cOut in s.false)
        (in1 in s.false && in2 in s.true ) => (ans in s.true  && cOut in s.false)
        (in1 in s.false && in2 in s.false) => (ans in s.false && cOut in s.false)
    }
}
run halfAdder for 4 Gate, exactly 2 Input, exactly 2 Output, exactly 4 State

// 全加算器
pred fullAdder {
    some disj in1, in2, cIn : Input, disj ans, cOut : Output | all s : State {
        (in1 in s.true  && in2 in s.true  && cIn in s.true )
            => (ans in s.true  && cOut in s.true )
        (in1 in s.true  && in2 in s.true  && cIn in s.false)
            => (ans in s.false && cOut in s.true )
        (in1 in s.true  && in2 in s.false && cIn in s.true )
            => (ans in s.false && cOut in s.true )
        (in1 in s.true  && in2 in s.false && cIn in s.false)
            => (ans in s.true  && cOut in s.false)
        (in1 in s.false && in2 in s.true  && cIn in s.true )
            => (ans in s.false && cOut in s.true )
        (in1 in s.false && in2 in s.true  && cIn in s.false)
            => (ans in s.true  && cOut in s.false)
        (in1 in s.false && in2 in s.false && cIn in s.true )
            => (ans in s.true  && cOut in s.false)
        (in1 in s.false && in2 in s.false && cIn in s.false)
            => (ans in s.false && cOut in s.false)
    }
}
run fullAdder for 9 Gate, exactly 3 Input, exactly 2 Output, exactly 8 State

alloy_combilogic.thm

<?xml version="1.0"?>
<alloy>

<view nodetheme="Martha" edgetheme="Martha">

<projection> <type name="State"/> </projection>

<defaultnode color="White"/>

<defaultedge color="Black"/>

<node>
   <type name="Element"/>
   <type name="Gate"/>
   <type name="Int"/>
   <type name="State"/>
   <type name="String"/>
   <type name="univ"/>
   <type name="seq/Int"/>
   <set name="$decoder_in1" type="Input"/>
   <set name="$decoder_in2" type="Input"/>
   <set name="$decoder_out0" type="Output"/>
   <set name="$decoder_out1" type="Output"/>
   <set name="$decoder_out2" type="Output"/>
   <set name="$decoder_out3" type="Output"/>
</node>

<node color="Green">
   <set name="true" type="Element"/>
</node>

<node color="Red">
   <set name="false" type="Element"/>
</node>

<node shape="Box">
   <type name="Input"/>
   <type name="Output"/>
</node>

<node shape="Inv House">
   <type name="AndGate"/>
</node>

<node shape="Inv Trapezoid">
   <type name="OrGate"/>
</node>

<node shape="Parallelogram">
   <type name="NotGate"/>
</node>

<edge layout="yes">
   <relation name="source"> <type name="Element"/> <type name="Element"/> </relation>
</edge>

</view>

</alloy>