Типы утверждений

Существует 2 типа утвреждений:

  • Immediate — основаны на событиях и выполняются только в процедурном коде;
  • Concurrent — основаны на тактах и могут выполняться как в процедурном коде, так и в модулях, интерфейсах, program-блоках.

Immediate утверждения используются только при динамической симуляции. По своей сути они близки к конструкции «if...else» — проверяют выполнение условного выражения. Отличие состоит в том, что если условное выражение принимает значения X, Z или 0, то выводится сообщение об ошибке.

 always @(posedge clk)
    if (state == ACCESS ) begin
        assert (addr_1 == addr_2)
            $display ("OK. addr_1 equals addr_2");
        else
            $error("**ERROR: Invalid address");
    end			

Обратите внимание, что проверка равенства адресов addr_1 и addr_2 будет происходить только по событию «state == ACCESS».
Concurrent утверждения используются как средствами формальной верификации, так и динамической. Они могут выполняться в процедурном коде (always- и initial-блоки), как immediate утверждения, но обычно используются в модулях, интерфейсах и program-блоках, как отдельные параллельные блоки. Свойство property с одной из директив assert, assume или cover — это concurrent утверждение, которое будет проверяться на всем протяжении симуляции.

Директивы

Директивы описывают, как должно использоваться свойство. Пока к свойству не применена директива, проверка выполнения свойства не начинается. В SystemVerilog поддерживаются следующие директивы:

  • assert – при применении данной директивы свойство используется как проверочный блок (checker), который выдает сообщения о каждом выполнении свойства (успешном или неуспешном);
  • assume – предполагает, что свойство выполняется в процессе верификации. По умолчанию выдаются только сообщения об ошибке выполнения свойства;
  • cover - свойство используется, как сборщик статистики о том, сколько было предпринято попыток выполнить это свойство (при этом они не обязательно должны завершиться успешно), какое количество было успешным и неуспешным.

При использовании директив assert или assume сообщения выдаются в процессе симуляции. Статистика, собираемая директивой cover, выводится в конце симуляции. Есть еще одна директива expect, схожая с assert, но которая должна выполняться только в процедурном блоке (включая always, initial блоки, подзадачи task и функции). Используется эта директива, как оператор wait, только в качестве условия здесь выступает свойство. Пока свойство не выполнится (успешно или неуспешно), дальнейшее выполнение блока не происходит. Пример:

program test_prog;
initial begin
    repeat (8) @(posedge clk);
    expect( @(posedge clk) start_sig )
    else
        $error( "**ERROR: No start_sig" );
    ...
end
endprogram