Формальная верификация

В отличие от комбинационных схем, где выход зависит исключительно от текущих входов, последовательностная логика оперирует состояниями. Это вносит следующие изменения в подход к верификации:

  1. Чтобы проверять секвенциальную логику, необходимо сопоставлять текущие значения сигналов с их значениями в прошлом. Для этого используются системные функции:

    • $past(сигнал) возвращает значение сигнала на 1 такт назад.

    • $stable(сигнал) эквивалентен проверке сигнал == $past(сигнал).

    • $rose(сигнал)/$fell(сигнал) фиксируют переход сигнала в логическую единицу или ноль относительно предыдущего такта.

  2. Солвер пытается найти уязвимость, инициализировав регистры любыми возможными значениями. Без явных ограничений начального состояния проверка может стартовать с недостижимых в реальности конфигураций. Для самых простых случаев достаточно явно указать значения внутренних триггеров равными 0 (что обычно мы подразумеваем при проектировании). В иных случаях, можно анализировать только те, случаи, которые следуют после деактивации сигнала сброса rst.

Обратите внимание, что ограничения assume накладываются на все проверяемые свойства assert.

  1. Если для комбинационной логики достаточно проверки на глубину в 1 такт, то для последовательностных схем требуется индивидуальный подбор параметра depth. Избыточная глубина увеличивает время работы солвера, а недостаточная — не позволяет покрыть целевые сценарии.

Разберём верификацию уже известного нам модуля sum_reduce:

src/06-sequential-logic/formal-verification/sum_reduce_fv.sv
module sum_reduce_fv #(
    parameter int COUNT_OF_BITS = 4
) (
    input logic clk,
    input logic rst,
    input logic [COUNT_OF_BITS-1:0] num,
    output logic [COUNT_OF_BITS-1:0] sum
);

  logic [COUNT_OF_BITS-1:0] acc;

  always_comb begin
    sum = acc + num;
  end

  always_ff @(posedge clk) begin
    if (rst) begin
      acc <= 'b0;
    end else begin
      acc <= sum;
    end
  end

`ifdef FORMAL
  logic past_valid = 1'b0;  (1)
  always @(posedge clk) begin
    past_valid <= 1'b1;
  end

  initial begin  (2)
    assume (rst);
  end

  always @(posedge clk) begin  (3)
    if (past_valid && $past(rst)) begin
      assert (acc == '0 && sum == num);
    end
  end

  always @(posedge clk) begin  (4)
    if (past_valid && !rst && !$past(rst)) begin
      cover (sum == $past(sum) + num && num > 0);
    end
  end

  localparam logic [COUNT_OF_BITS-1:0] MAX_VAL = '1;
  always @(posedge clk) begin  (5)
    if (past_valid && !rst && !$past(rst)) begin
      if ($past(acc) == MAX_VAL && $past(num) > 0) begin
        assert (acc == $past(num) - 1'b1);
      end
    end
  end
`endif
endmodule
1 Поскольку в самый первый такт работы схемы у сигналов ещё нет информации о прошлом состоянии, то оператор $past() вернёт неопределённое значение. Данный флаг позволяет нам пропустить данное состояние при верификации.
2 Принудительно заставляем начинать анализ из состояния сброса (rst) (например, чтобы избежать значения acc не равным 0 на первом такте).
3 Проверка, что если на предыдущем такте был активен сигнал rst, то на текущем такте внутренний acc должен обнулиться, а выход sum — принять текущее значение num.
4 Поиск цепочки сигналов, при которой в отсутствие сброса текущая сумма корректно складывается из предыдущей суммы и нового входного значения num.
5 Проверка переполнения при достижении максимального значения (MAX_VAL).

Запустив SymbiYosys в режиме bmc с depth 20, получим ожидаемый результат PASS. Теперь посмотрим на трассу, сгенерированную в режиме cover:

initial  (1)
assume (= [$auto$async2sync.cc:107:execute$85] false)
assume (= [$auto$async2sync.cc:116:execute$89] true)
assume (= [_witness_.anyinit_procdff_64] false)
assume (= [_witness_.anyinit_procdff_65] #x1)
assume (= [acc] #x0)
assume (= [past_valid] false)

state 0  (2)
assume (= [clk] false)
assume (= [num] #x1)
assume (= [rst] true)

state 1  (3)
assume (= [clk] false)
assume (= [num] #x0)
assume (= [rst] false)

state 2  (4)
assume (= [clk] false)
assume (= [num] #x1)
assume (= [rst] false)

state 3
assume (= [clk] false)
assume (= [num] #x1)
assume (= [rst] false)
1 Начальное состояние регистров, выбранное SMT-солвером для выполнения условий cover. Yosys на этапе подготовки создал необходимые переменные для работы. Нам интересны регистры acc и past_valid, которым присвоены значения 0, false (это ожидаемые нами значения, но так солвер подбирает не всегда).
2 Первый такт: солвер устанавливает сигнал rst в true для выполнения условий ограничений.
3 Второй такт: сигнал сброса деактивируется, но $past(rst) = 1. num = 0, acc = 0 ⇒ sum = 0.
4 Третий такт: $past(rst) теперь равен 0. num = 1, acc = 0 ⇒ sum = 1, то есть выражение в cover истинно. Но как и с триггерами, результат будет зафиксирован на следующем фронте клока[1].
Не забывайте про упражнения.