设计实验：从规格到三输入多数表决电路

实现之前先固定条件

设计一个电路：三个输入 a、b、c 中至少两个为 1时，y=1。这里规定输入是稳定的 0/1，各输入权重相等，并且不记忆过去的输入。“恰好两个”和“至少两个”在 111 时是不同函数。

三个项分别表示某两个输入同时为 1。同一功能也可提取公因式写为 $y=ab+c(a+b)$。哪一种更快取决于单元及输入到达时间。

多数表决等于全加器的进位

在下方，将 cin 视为第三个输入 c。cout 就是这里的 y，sum 则表示输入中 1 的个数是否为奇数^{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 ns 内工作。

改变规格并寻找反例

加入输出使能 e 后，得到 $y=e(ab+ac+bc)$。此时有四个输入，穷举检查需要 16 种组合。还应单独检查 e=0 时必须忽略 a、b、c 的不变式^{i不变式 所有允许的执行过程中都必须始终成立的条件。例如，深度为 4 的 FIFO 中，存储条目数必须始终在 0 到 4 之间。了解更多}。