設計実習：仕様から 3 入力多数決回路へ

実装前に条件を固定します

三つの入力 a・b・c のうち、二つ以上が 1 なら y=1 となる回路を作ります。入力は安定した 0/1、各入力の重みは等しく、以前の入力は記憶しないと定めます。「ちょうど二つ」と「二つ以上」は、111 で異なる関数です。

三つの項は、それぞれ二つの入力が同時に 1 であることを表します。同じ機能を $y=ab+c(a+b)$ と因数分解することもできます。どちらが速いかはセルと到着時刻によります。

多数決は全加算器のキャリーと同じです

下の cin を第三の入力 c として読んでください。cout が今回の y で、sum は奇数パリティ^{iパリティ 1 のビット数が奇数か偶数かを表す値です。パリティ検査は奇数個のビット誤りを検出しますが、偶数個の誤りを見逃す場合があります。 詳しく見る}です。001 と 111 を比較すると、パリティを多数決として使う誤りが見えてきます。

仕様を基に、実装とは独立した検査基準を作ります

(a & b) | (a & c) | (b & c) と同じ式を参照モデルにコピーすると、同じ間違いを持ち込むおそれがあります。仕様の「1 が二つ以上」を整数で計算する基準を使います。

module voter3(input logic a, b, c, output logic y);
  assign y = (a & b) | (a & c) | (b & c);
endmodule

module tb;
  timeunit 1ns;
  timeprecision 1ps;
  logic a, b, c, y;
  int ones;
  voter3 dut(.*);
  initial begin
    for (int v = 0; v < 8; v++) begin
      {a, b, c} = v[2:0];
      #1;
      ones = int'(a) + int'(b) + int'(c);
      assert (y === (ones >= 2))
        else $fatal(1, "voter mismatch at %03b", {a,b,c});
    end
    $finish;
  end
endmodule

各ビットを int に拡張したのは、1 ビット演算の幅による混乱を避けるためです。#1 はこのテストの組合せ論理が更新される時間を与えるもので、実チップが 1 ns で動く証拠ではありません。

仕様を変えて反例を探す

出力を許可する enable e を追加すると、$y=e(ab+ac+bc)$ になります。入力は四つになり、全数検査には 16 組必要です。e=0 のとき a・b・c をすべて無視するという不変条件^{i不変条件 許可されたすべての実行で、常に真でなければならない条件です。例えば深さ 4 の FIFO の格納数は常に 0 以上 4 以下です。 詳しく見る}も、別に検査してください。