Практикум проектирования: от спецификации к трёхвходовому большинству

Зафиксируйте условия до реализации

Построим схему, в которой y=1, если минимум два из входов a,b,c равны 1. Входы — устойчивые 0/1, веса одинаковы, предыдущие входы не запоминаются. «Ровно два» и «минимум два» — разные функции при 111.

Каждый из трёх членов означает одновременную единицу на двух входах. Ту же функцию можно факторизовать как $y=ab+c(a+b)$. Какая форма быстрее, зависит от ячеек и времени прихода сигналов.

Большинство совпадает с переносом полного сумматора

Считайте cin ниже третьим входом c. cout — наш y, sum — нечётная чётность^{iЧётность указывает, чётно или нечётно число единичных битов. Проверка чётности обнаруживает ошибки в нечётном числе битов, но может пропустить ошибки в чётном числе. Подробнее}. Сравнение 001 и 111 выявляет ошибочную подмену большинства паритетом.

Независимый критерий выводите из спецификации

Если скопировать (a & b) | (a & c) | (b & c) в эталон, можно повторить ту же ошибку. Используйте целочисленный подсчёт по требованию «как минимум две единицы».

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 комбинаций. Отдельно проверяйте инвариант^{iИнвариант — условие, которое должно выполняться при любом допустимом выполнении. Например, число хранимых элементов FIFO глубиной 4 всегда находится между 0 и 4 включительно. Подробнее}: при e=0 значения a,b,c не должны влиять на выход.