SVA: как SystemVerilog внедряет темпоральную логику в верификацию цифровых схем

SVA: как SystemVerilog переносит темпоральную логику в код верификации

SVA — встроенный в SystemVerilog подъязык для формальной и динамической верификации цифровых схем. Он переводит абстракции темпоральной логики (LTL) в исполняемый код, привязанный к тактам синхронизации, многозначной логике сигналов (0, 1, X, Z) и событиям на фронте тактового сигнала.

Время в SVA измеряется только в тактах: ##1 — следующий такт, ##[2:5] — задержка от 2 до 5 тактов. Все утверждения должны быть привязаны к фронту такта (@(posedge clk)), иначе они не выполнятся.

От темпоральной логики к инженерной практике

В классической булевой логике условие либо истинно, либо ложно здесь и сейчас. В темпоральной логике добавляется измерение времени: формулы вроде «всегда, если A, то рано или поздно B» (G(A → F B) в LTL) удобны для математиков, но не для инженеров, работающих с сигналами и регистрами.

SVA решает эту проблему, адаптируя темпоральную логику под реалии синхронной цифровой схемотехники:

• Время = такты: нет наносекунд или миллисекунд.
• Многозначная логика: учитываются не только 0 и 1, но и X (неопределённость), Z (высокий импеданс).
• Событийная модель: все утверждения привязаны к событиям — например, к переднему фронту такта.

Формула «если req, то через 1–3 такта должен быть ack» записывается так:

property handshake;
    @(posedge clk) req |-> ##[1:3] ack;
endproperty
assert property (handshake);

Это работает как математическая формула, но с привязкой к реальным сигналам.

Три кита SVA: последовательности, свойства, директивы

SVA строится на трёх взаимосвязанных блоках.

1. Последовательности (Sequences)

Описывают паттерны сигналов во времени. Примеры:

• a ##1 b — сигнал a активен сейчас, b — на следующем такте.
• req [*3:5] — сигнал req должен удерживаться 3–5 тактов подряд.
• req ##[1:3] ack — после req сигнал ack должен появиться через 1–3 такта.

Без SVA такие проверки приходилось кодировать вручную, что приводило к громоздким и ненадёжным конструкциям.

2. Свойства (Properties)

Задают правила поведения устройства. Два оператора импликации:

• |-> (overlapped implication) — условие выполняется в том же такте.
• |=> (non-overlapped implication) — условие выполняется в следующем такте.

Пример на реальном требовании к контроллеру памяти:

property mem_protocol;
    @(posedge clk) disable iff (!rst_n)
    read_en |-> !$isunknown(data_bus) ##2 ack;
endproperty
assert property (mem_protocol);

Здесь проверяется, что при активации read_en шина data_bus не в состоянии X, а ack приходит ровно через 2 такта.

3. Директивы (Directives)

Управляют тем, что делать с утверждениями:

• assert — обязательная проверка: если условие нарушается, симулятор останавливается с ошибкой.
• cover — сбор статистики: показывает, срабатывало ли утверждение вообще (полезно для оценки полноты тестов).
• assume — ограничение для входных сигналов: используется в формальной верификации, чтобы отсечь заведомо невозможные состояния.

Практический пример: контроллер памяти и неопределённость на шине

Инженер получает требование: «Сигнал чтения не должен быть активен, если шина данных в состоянии X; подтверждение должно прийти ровно через 2 такта после запроса».

Первая версия кода:

property mem_rule;
    @(posedge clk) disable iff (!rst_n)
    read_en |-> !$isunknown(data_bus) ##2 ack;
endproperty
assert property (mem_rule);

В симуляции на 1234‑м такте срабатывает ошибка: data_bus был в состоянии X в момент активации read_en. Диагностика показывает, что проблема в нестабильности тактового сигнала — шина данных иногда «заикается» из-за неверной синхронизации.

Инженер добавляет синхронизацию и перезапускает симуляцию. Ошибка исчезает.

Что это даёт:

• SVA ловит ошибку раньше, чем она проявится в кремнии.
• SVA локализует проблему ближе к источнику — не на выходе, а на входе.
• SVA сокращает время отладки, так как не нужно вручную мониторить все сигналы.

Границы применимости SVA

SVA игнорируется синтезом — утверждения не влияют на RTL-код. За это приходится платить: все утверждения должны быть синхронизированы с тактовым сигналом, иначе они просто не сработают.

Кроме того, SVA не поддерживает непрерывное время: если нужно проверить задержку в 10 нс, придётся пересчитывать её в такты с учётом частоты. Это может быть неочевидно для инженеров, привыкших работать с физическими единицами времени.

Когда SVA выигрывает, а когда подводит

Главное преимущество SVA — компактность и ясность кода. Без SVA проверка простого handshake может занимать 10–15 строк в Verilog. С SVA то же самое:

assert property (@(posedge clk) req |-> ##[1:3] ack);

— одна строка, понятная и проверяемая.

Но SVA не заменяет полноценные тестбенчи. Например, проверка кросс-доменных переходов или глюков в пределах одного такта требует дополнительных immediate утверждений или ручного кодирования в RTL.

Дополнительные инструменты и операторы

SVA поддерживает системные функции и операторы для работы с сигналами:

• $rose, $fell, $stable, $past(expr, n) — анализ изменений сигналов.
• $isunknown, $onehot, $countones — проверка состояний.
• Операторы задержки: ##n, ##[m:n]; повторения: [*n], [->n], [=n].

Пример с использованием $past:

property no_spikes;
    @(posedge clk) $stable($past(data, 1)) |-> data == $past(data, 1);
endproperty

Интеграция с инструментами

SVA активно используется в симуляции и формальной верификации. Примеры интеграции:

• Verilator: установка на Ubuntu 22.04:

  git clone https://github.com/verilator/verilator
  git checkout v4.102
  autoconf
  ./configure
  make -j $(nproc)
  make test
  sudo make install
  

• RISC-V GCC: кросс-компилятор для тестирования микроконтроллерных ядер (например, SCR1).

SVAUnit: декомпозиция тестов

Для более гибкого управления тестами можно использовать библиотеку SVAUnit. Она позволяет отделить логику проверки утверждений от генерации стимулов:

class SVAUnit_Test extends SVAUnit_Test;
    function void test();
        // Генерация стимулов
        // Проверка утверждений
    endfunction
endclass

Это упрощает поддержку тестов и их повторное использование.

Уровни логирования (severity)

Для управления выводом сообщений об ошибках используются уровни логирования:

• $info — информационные сообщения.
• $warning — предупреждения.
• $error — ошибки.
• $fatal — критические ошибки.

Пример:

assert property (handshake) else $error("Handshake failed!");

Вывод: SVA как мост между спецификацией и реализацией

SVA переводит неявные требования спецификации в исполняемый код, который одновременно документирует дизайн, проверяет его корректность и упрощает отладку. Однако его эффективность зависит от понимания границ применимости: SVA выигрывает в задачах, связанных с синхронными протоколами, но не подходит для непрерывного времени или сложных кросс-доменных сценариев.