設計實作：從規格到三輸入多數決電路

實作前先固定條件

設計一個電路：三輸入 a、b、c 中至少兩個為 1時，y=1。這裡規定輸入為穩定 0/1、各輸入權重相同，而且不記憶前次輸入。「恰好兩個」與「至少兩個」在 111 時是不同函數。

三項各表示兩個輸入同時為 1。相同功能也可因式分解為 $y=ab+c(a+b)$。哪一種較快，取決於元件與到達時間。

多數決就是全加器的 carry

將下方 cin 視為第三個輸入 c。cout 就是我們的 y，sum 是奇同位值^{i同位性（parity）表示值為 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 組。也要另外檢查不變量^{i不變量是在所有允許的執行過程中都必須成立的條件。例如，深度為 4 的 FIFO，其儲存數量必須一直介於 0 至 4。 詳細內容}：e=0 時必須忽略全部 a、b、c。