Все знают про язык программирования C, поменьше — про язык программирования F, кое‑кто про B, предшественник C, а вот знаете ли вы про язык «e»? Их кстати два — один с большой буквы «E», а другой с маленькой «e».

Вы наверное подумали, что это еще один безызвестный язык от какого‑нибудь аспиранта провинциального европейского университета. Однако интерпретатор маленького «e» под названием Specman продали в 2005 году большой компании Cadence Design Systems за $315 милионов долларов. Причем президента продающей компании Verisity звали Гаврилов. Также можно нагуглить, что этот язык использовали внутри компании Intel. Что же в нем такого, что вызвало интерес у толстых богатых корпораций?

От "e" и верилога к SystemVerilog

Язык «e» относится к так называемым языкам верификации аппаратуры — Hardware Verification Languages (HVL). «e» был первым успешным языком среди HVL, но потом его находки вобрал в себя появившийся после 2001 года SystemVerilog.

SystemVerilog стал гибридом из:

1. Языка описания аппаратуры Verilog (Hardware Description Language — HDL), который используется для логического синтеза схем — код на нем превращается в граф из логических элементов, а потом в дорожки и транзисторы микросхемы на фабрике;

2. Расширения верилога под названием Superlog (оттуда SV вобрал сложные типы — структуры итд);

3. HVL под названием Vera (откуда SV взял объектно‑ориентированность и некоторые аналоги черт из «e»);

4. Языка PSL (Property Specification Language), который возник чуть раньше и влиял на развитие SystemVerilog Assertions (SVA). PSL и SVA относятся к Hardware Assertion Languages, языкам высказываний темпоральной логики.

Главным драйвером развития SystemVerilog была компания Synopsys, которая купила и Superlog за ~$30 миллионов долларов и Vera за $26 миллионов.

Synopsys, вместе с Cadence, Mentor Graphics и представителями крупных электронных компаний занимались стандартами для всего этого хозяйства через комитет Accellera, на котором пришлось пару раз позаседать и автору этой заметки.

Помимо вышеперечисленных языков был еще HVL под названием Rave, который канул в Лету, а также Jeda — язык, который создали бывшие работники стартапа, с которым Synopsys купил Веру, по поводу чего Synopsys тревожил их с помощью юристов, после чего в Jeda боялись инвестировать и он тоже канул в Лету.

До HVL были HDL

В 1980 годы людям надоело рисовать схемы карандашом на бумаге или возить мышкой по экрану. В конце десятилетия случилась революция логического синтеза и схемы стали проектировать с помощью написания кода на языках описания аппаратуры Verilog и VHDL. Были еще PALASM, Abel и Cupl, а также iHDL — секретный внутренний HDL в Intel. Все эти языки быстро вымерли и середина 1990-х проходила под холиваром Verilog и VHDL.

В начале 1990-х ряд компаний пытался насадить VHDL, но инженеры сопротивлялись его противным фичам. Например если вам нужно сложить A+B, то в верилоге вы могли написать просто C=A+B. А в VHDL приходилось писать что‑нибудь типа:

с <= std_logic_vector (resize (signed (a), 9) + resize (signed (b), 9));

Потом Verilog победил, но VHDL до сих пор остался в разных неочевидных местах, например графический процессор внутри Apple iPhone, который Apple изначально лицензировал у Imagination Technologies - был написан на VHDL.

Рост сложности, нудности и дороговизны ошибки

И у Verilog, и у VHDL не все было хорошо с тестированием получившихся схем. Пока схемы были маленькими, на уровне сложности советской игры 1985 года «Ну, погоди!» (она не была написана на HDL, я привожу ее просто как уровень сложности), с тестированием особой проблемы не было. Люди писали код в духе:

a = 2;
b = 2;

# 10   // Подождать 10 микросекунд

if (sum != 4)
begin
    $display ("Сумматор не суммирует!");
    $finish;
end

Такие прямолинейные тесты так и называются: direct test («прямой тест»).

Однако в начале 1990-х годов размер микросхем быстро рос. Я до сих пор помню, с какими расширенными глазами мне маркетер из Mentor Graphics рассказывал про «гиганский ASIC на 100 тысяч вентилей» от его японского клиента, который «невозможно верифицировать» за разумное время. Сейчас счет вентилей в ASIC‑ах идет на миллиарды, и это никого так не пугает.

Дело в том, что помимо увеличения количества элементов увеличивалась и микроархитектурная сложность. Вместо микрокода 1970-х и простых конечных автоматов проектировщики стали конструировать конвейерные схемы, и были просто задавлены количеством частных случаев, которые им приходилось разгребать. Инженеры‑тестировщики (верификация в начале 1990-х стала оформляться как отдельная профессия) — очень страдали от нудности процесса и сбегали сначала в программирование GUI для виндоус, а потом в возникший в середине 1990-х веб‑дизайн.

Росла и стоимость ошибки — фиксированный платеж за re‑spin микросхемы на фабрике стал стоить сотни тысяч долларов, а потери выручки от задержки выпуска микросхемы стали исчисляться десятками миллионов (сейчас все выросло еще на порядок).

Решение ситуации, часть первая: повышаем уровень абстракции с сигналов до транзакций

И вот тогда возникло несколько идей для повышения производительности верификатора:

1. Повысить уровень абстракции - вместо проверки сигналов проверять так называемые транзакции. Примеры транзакции:

   • передаваемый за N тактов сетевой пакет;

   • запись строки из кэша процессора в память по заданному адресу и с заданным содержимым;

   • координаты и цвета вершин треугольника в GPU;

2. Проверять поведение блока, спроектированого на верилоге, против модели, которая работает на уровне последовательности транзакций и ничего не знает о тактовом сигнале.
   
   Такую модель гораздо проще написать, чем потактовую модель - ее программист может вообще не знать, как организован конвейер и как проектируется хардвер на уровне регистровых передач. Более того, писание такой модели можно аутсорсить. Или купить готовую - скажем симулятор процессора на уровне инструкций.

3. Для превращения транзакции в сигналы и сигналов в транзакции стали использовать особого вида программу под названием функциональная модель шины (Bus Functional Model - BFM). Опять же, писание BFM можно аутсорсить или вообще купить уже готовую модель - скажем шины AXI, SATA или PCI Express и приспособить под свои нужды.

Решение ситуации, часть вторая: делаем ограниченно-случайный генератор транзакций чтобы создавать сценарии, которые не приходили нам в голову

Использование транзакций в комбинации с BFM повышает производительность труда даже для написания прямых тестов, но все равно тысячи прямых тестов писать тягостно. Кроме этого, некоторые сценарии могут просто не приходить в голову.

Можно генерировать транзации, наполняя структуру транзакции (или класс транзакции) просто случайными числами, но тогда 99% транзакций могут быть просто внутренне противоречивыми, такими, которые никогда не увидит аппаратный блок в реальной жизни. Например запрос на чтение строки в кэш из памяти с атрибутом «атомарный».

Чтобы повысить качество генерации случайных транзакций, языки верификации аппаратуры ввели специальный механизм, который называется «решатель ограничений» (constraint solver). Он напоминает функциональные языки программирования: вы задаете отношения между объектами, и для вас автоматически генерируется транзакция, которая удовлетворяет этим ограничениям.

Причем (!) если у вас есть правило «если A находится в множестве { 1, 4, 8 } то B находится в диапазоне [5:10]» — то это правило будет работать в две стороны:

1. Если вы потом ограничите A == 4, то оно будет генерить только значения B, которые не вступают в конфликт с этим правилом, то есть генерить только B = 6, 7, 5, но не B = 13.

2. Но если вы ограничите B == 13, то оно будет генерить A = 10 или 0, но не такие A, чтобы B нарушало правила:

Вот как это выглядит на SystemVerilog:

class simple_transaction;

  rand [7:0] a;
  rand [7:0] b;

  constraint a_versus_b
  {
       a inside { 1, 4, 8 }
    -> b inside { [5:10]  };
  }

На тему ограниченно‑случайного генератора транзакций было последнее занятие на Школе Синтеза Цифровых Схем. Вот его видео, сайт и телеграм‑канал:

Решение ситуации, часть третья: проверяем, что известные нам интересные сценарии действительно случились во время симуляции - с помощью групп функционального покрытия

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

Да что там генератор случаных транзакций. Даже человек, который писал прямые тесты, может забыть или полениться реализовать часть тестового плана, а потом сказать "все сделано" и уехать в отпуск. Как проверить, что действительно все сделано?

Для этого в SystemVerilog есть два механизма: группы функционального покрытия (covergroups) и последовательности выражений темпоральной логики для функционального покрытия (cover properties).

И о первых, и о вторых мы поговорим на следущем занятии Школы Синтеза, которое состоится в эту субботу 25 марта. Занятие будет вести Сергей Чусов, Инженер по верификации аппаратного обеспечения лаборатории НИЛ-ЭСК МИЭТ

Идея cоvergroups: это структуры данных, которые состоят из так называемых точек функционального покрытия, coverpoints, которые соотвествуют переменным или выражениям. Для каждого из них есть группа "корзинок", cover bins. Когда симулятор видит какое-нибудь интересное значение, он увеличивает счетчик соотвествующей "корзинки":

В SystemVerilog есть подъязык описания этих корзинок и выглядит это так:

covergroup cvr @ (posedge clk iff ~ rst);

    coverpoint push
    {
      // Мы видели такты с сигналом вталкивания в очередь (push)
      bins push    = { 1 };
      // и видели такты без этого сигнала
      bins no_push = { 0 };
    }
    
    // Мы видели все четыре комбинации сигналов вталкивания и выталкивания
    cross push, pop;

А вот как мы можем применять корзинки и группы корзинок для фиксации появления различных данных: индивидуальных значений, групп значений, диапазона данных или шаблона:

    write_data_specific: coverpoint write_data
    iff (push)
    {
      bins          equal_12                      = {   8'h12 };
      bins          equal_12_or_20                = {   8'h12 , 8'h20   };
      bins          from_12_till_20               = { [ 8'h12 : 8'h20 ] };
      bins          from_12_till_20_in_3_bins [3] = { [ 8'h12 : 8'h20 ] };
      ignore_bins   to_ignore                     = { [ 8'h17 : 8'h18 ] };
      bins          mixed                         = { [ 8'h12 : 8'h20 ] , 8'h30 };
      wildcard bins binary_xx1x1x1x               = {   8'b??1?1?1? };
      wildcard bins hex_2X                        = {   8'h2? };
    }

Также мы можем создавать корзинки для последовательности изменений значений в нескольких тактах:

    push_transitions: coverpoint push
    {
      bins push_010             = ( 0 => 1 => 0 );
      bins push_101_or_1001     = ( 1 => 0 => 1 ), ( 1 => 0 => 0 => 1 );
      bins push_10001           = ( 1 => 0 [* 3] => 1 );
    }

Еще можно средствами обычного кода на верилоге записывать номера тактов, в которых случились разные события и потом делать корзинки по разнице событий по времени (в смысле по тактам). Это полезный прием, который я часто использую.

Еще инструмент для верификатора: выражения темпоральной логики

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

Мы не будем разбирать формальную верификацию в этом цикле Школы Синтеза, но на субботнем занятии concurrent assertions и cover properties будут.

Пример concurrent assertions на тему протокола valid / ready, который мы разбирали во время одного из прошлых занятий Школы Синтеза:

  keep_valid_high_until_ready: assert property
    ( @ (posedge clock) disable iff (reset)
        valid & ~ ready |-> ##1 valid );

Смысл этого выражения: симулятор считывает значения сигналов valid и ready на положительном фронте тактового сигнала clock, кроме случаев, когда мы находимся в сбросе (reset). При этом: если на фронте в текущем такте valid был выставлен в 1, но ready стояло 0, то в следующем такте valid должен продолжать стоять. А иначе симулятор выдаст ошибку.

Такое простое правило покрывает все случаи использования valid и ready: valid перед ready, valid после ready или одновременно:

Вот другой пример высказывания темпоральной логики, для очереди FIFO:

  three_pushes_without_pops_result_in_cnt_3_and_non_empty:
    assert property
      (@ (posedge clk) disable iff (rst | depth < 3)
       ~ pop throughout (empty and push [*3]) |-> ##1 ~ empty & cnt == 3);

Оно значит: если FIFO сначало было пустое, а потом мы сделали три вталкивания, и все это время не было ни одного выталкивания, то потом мы получим счетчик элементов FIFO равным трем и признак пустоты empty=0.

Такие же выражения можно использовать для проверки функционального покрытия, но в них нужно опустить следование / импликацию предикатов, то есть "|->":

  observed_three_pushes_without_pops:
    cover property
      (@ (posedge clk) disable iff (rst | depth < 3)
       (~ pop) throughout (empty and push [*3]));

что означает: "во время симуляции видел три вталкивания подряд без выталкивания".

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

В субботу 25 марта на Школе Синтеза это все будет детально. Она сейчас проходит в офлайне на 12 площадках, но даже если вы до этого не ходили на Школу, но знаете основы верилога, вы можете получить инструкции по софтверу в телеграм-канале и потом смотреть все на ютюбе.

UPD: Трансляция занятия на YouTube в 12:00 в субботу 25 марта по московскому времени:

Краткое содержание:

Технология проверки функционального покрытия хорошо дополняет технологию генерации ограниченно-случайных транзакций, которую мы обсудили на предыдущем занятии Школы.

Такие методы, как "корзинки" покрытия (covergroups/coverpoints/cover bins), а также покрытие последовательностей, заданных выражениями темпоральной логики (cover properties) - позволяют проверить, что при симуляции со случайными транзакциями произошли все интересные сценарии, которые инженер-верификатор запланировал в плане тестирования.

Тандем "генерация ограниченно случайных транзакций + проверка покрытия плана тестирования" повышает качество, делает верификацию более предсказуемой, и одновременно менее нудной для разработчика, превращая создание таких сред в своего рода искусство.

Выражения темпоральной логики можно использовать не только для оценки покрытия. Если соединить их с импликацией предикатов ("если произошло A, а через N тактов B, то затем можно ожидать С") то такие выражения можно использовать для нахождения ошибок в схеме - как при симуляции, так и с помощью программ формальной верификации / автоматического доказательства утверждений. В SystemVerilog эта часть языка называется concurrent assertions - "параллельные утверждения". Это полезный инструмент как для инженера-верификатора, так и для проектировщика.

На занятии в субботу 25 марта мы разберем функциональное покрытие и параллельные утверждения, а на занятии 1 апреля - свяжем всю верификацию в законченную картину вместе с моделями интерфейсов шины (Bus Functional Model) - программ, которые связывают сигналы и транзакции.