설계 실습: 명세에서 3입력 다수결 회로까지

구현 전에 동작 조건을 정합니다

세 입력 a,b,c 중 둘 이상이 1이면 y=1인 회로를 만듭니다. 여기서는 입력이 안정된 0/1이고, 각 입력의 가중치는 같으며, 이전 입력을 기억하지 않는다고 정합니다. “정확히 둘”과 “둘 이상”은 입력이 111일 때 출력이 다릅니다.

세 항은 각각 두 입력이 동시에 1임을 뜻합니다. 같은 기능을 $y=ab+c(a+b)$로 인수분해할 수도 있습니다. 어느 쪽이 빠른지는 사용하는 셀과 입력 신호의 도착 시간에 따라 달라집니다.

다수결은 전가산기의 carry와 같습니다

아래에서 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의 값과 관계없이 출력이 0이어야 한다는 불변식^{i불변식 모든 허용 실행에서 항상 참이어야 하는 조건입니다. 예를 들어 깊이 4인 FIFO의 저장 개수는 항상 0 이상 4 이하입니다. 자세히 보기}도 따로 검사하세요.