Введение. Что такое утверждение?

Введение

Утверждения описывают поведение системы. В основном они используются для проверки правильности поведения проекта. Также с помощью утверждений можно оценить полноту функционального покрытия. Метод верификации на основе утверждений подразумевает расстановку внутри моделируемого кода “закладок”, проверяющих работу тех или иных функций по мере их срабатывания, не дожидаясь распространения следствия данного срабатывания на выход схемы. Полная управляемость и наблюдаемость внутренних цепей проекта, обеспечиваемая верификацией с помощью утверждений, значительно, сокращает время отладки. Процент ошибок, который удается обнаружить, используя утверждения, в наибольшей степени зависит от умения выделять в RTL-описании критические участки для проверки с помощью утверждений. Количество написанных утверждений тоже немаловажно.

Что такое утверждение?

Утверждение (Assertion) – это сжатое описание желательного или нежелательного поведения устройства. Рассмотрим в качестве примера взаимодействие двух устройств (см. рис. 1).

Рис. 1. Упрощенная структурная схема взаимодействия двух устройств

Взаимодействие между устройствами начинает ведущий, когда выставляет команду CMD и адрес ADDR. Если это команда записи, то вместе с командой и адресом ведущий выставляет данные для записи WDATA. Команда удерживается на шине до тех пор, пока ведомый не выставит сигнал CMD_ACCEPT, подтверждая то, что он принял команду. Если транзакция прошла успешно, то ведомый выставляет сигнал RESPONSE. При обработке команды чтения, вместе с сигналом RESPONSE, выставляются данные для чтения RDATA. Для правильной работы необходимо, чтобы ведомый выставил сигнал CMD_ACCEPT в течение трех тактов после того, как ведущий выставил команду на шине CMD (см. рис. 2).

Рис. 2. Диаграмма, описывающая желательное поведение устройства: сигнал CMD_ACCEPT должен прийти в течение трех тактов после появления команды на шине CMD

На рис. 2 был показан пример желательного поведения устройства. Для этой же диаграммы можно составить утверждение, описывающее нежелательное поведение устройства. Например, адрес и данные не должны меняться, пока не появится сигнал CMD_ACCEPT.
Утверждение для диаграммы, приведенной на рис. 2, на языке Verilog выглядит следующим образом:

//Verilog assertion
assign cmd_active = (CMD != `IDLE) ;
 
always @(posedge cmd_active)
begin
    repeat (1) @(posedge Clk)
    fork: cmd_accept_wait
    begin
        @(posedge CMD_ACCEPT)
        $display("SUCCESS: CMD_ACCEPT arrived in time\n", $time);
        disable cmd_accept_wait;
    end
    begin
        repeat (3) @(posedge Clk)
        $display("ERROR: CMD_ACCEPT did not arrive in time\n", $time);
        disable cmd_accept_wait;
    end
    join
end

Данное утверждение можно написать и с использованием языка C++, но дело в том, что Verilog и C++ не создавались, как языки для написания утверждений, поэтому то же самое утверждение на SystemVerilog выглядит гораздо более лаконично:

//SystemVerilog assertion
 
cmd_accept_wait:
assert property (@(posedge Clk)
(CMD != `IDLE) |-> ##[1:3] CMD_ACCEPT);