Дополнительные конструкции языка SVA

Дополнительные конструкции языка SVA

Динамический контроль

SystemVerilog включает системные вызовы для контроля проверки выполнения утверждений в процессе симуляции. Они позволяют остановить ($assertoff), перезапустить ($asserton), отменить ($assertkill) проверку утверждений. Динамический контроль может использоваться для того, чтобы отключить проверку утверждений во время сброса. Пример:

  1. module device2_control();
  2. initial begin : disable_assertions_during_reset
  3. @(posedge tb_top.input_intf.reset) //active high reset
  4. $assertoff(0, tb_top.slave);
  5. @(negedge tb_top.input_intf.reset)
  6. $asserton(0, tb_top.slave);
  7. end
  8. endmodule : device2_control
  9.  
  10.  
  11. module tb_top();
  12. ...
  13. //Объявление модуля device2
  14. device2 slave (
  15. .clk(clock),
  16. .rst(input_intf.reset),
  17. .CMD(input_intf.command),
  18. ...
  19. );
  20. //Объявление модуля device2_control
  21. device2_control device2_control_inst();
  22. ...
  23. endmodule : tb_top

В этом примере проверка утверждений отключается на время сброса. Для этого вызывается системный вызов $assertoff. Первым параметром в него передается количество уровней иерархии ниже того модуля, в котором мы хотим отключить проверку утверждений. В нашем случае таких уровней 0. Вторым параметром передается имя экземпляра модуля для отключения проверки утверждений. Т.к. контроль проверки выполнения утверждений находится в отдельном модуле, то приходится писать полный иерархический путь (tb_top.slave). Вместо имени модуля можно передавать имена утверждений. Остальные системные вызовы ($asserton и $assertkill) используют те же параметры.

Статический контроль

Статический контроль утверждений реализуется возможностями препроцессора:

  1. `ifdef CMD_ACCEPT
  2. assert property (@(posedge Clk)
  3. (CMD != `IDLE) |-> ##[1:3] CMD_ACCEPT);
  4. `endif

Проверка выполнения утверждения будет выполняться, только если в данной реализации протокола передачи сигнал CMD_ACCEPT используется. Другой способ статического контроля – это использование конструкции generate. Здесь утверждения компилируются, но не рассматриваются до этапа elaboration (завершения обработки во время трансляции):

  1. generate
  2. if (cmd_accept_on) begin
  3. assert property (@(posedge Clk)
  4. (CMD != `IDLE) |-> ##[1:3] CMD_ACCEPT);
  5. end
  6. endgenerate
  7.  
  8. //cmd_accept_on может быть параметром или константой

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

Сообщения

Нарушение утверждения сопровождается автоматическим выводом симулятором сообщения об ошибке. Если требуется вывести дополнительное сообщение, то используются следующие системные вызовы:

  • $info (информационное сообщение);
  • $warning (предупреждение);
  • $error (сообщение об ошибке);
  • $fatal (сообщение о сбое или отказе в работе).

Утверждение может содержать сообщения для случаев успешного и неудачного выполнения:

  1. assert property (@(posedge Clk)
  2. (CMD != `IDLE) |-> ##[1:3] CMD_ACCEPT)
  3. $info("CMD_ACCEPT arrived in time");
  4. else
  5. $error("CMD_ACCEPT did not arrive in time");

Системные функции языка SystemVerilog утверждений

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

  • $rose – возвращает ‘1’, если сигнал или самый младший бит вектора перешел из ‘0’ в ‘1’ в промежутке времени между текущим и предыдущим тактом;
  • $fell – возвращает ‘1’, если сигнал или самый младший бит вектора перешел из ‘1’ в ‘0’ в промежутке времени между текущим и предыдущим тактом;
  • $stable – возвращает ‘1’, если значение сигнала или вектора не изменилось по сравнению с предыдущим тактом;
  • $past – возвращает значение сигнала или вектора, которое было на предыдущем такте;
  • $onehot – возвращает ‘1’, если только один бит вектора в ‘1’;
  • $onehot0 – возвращает ‘1’, если только один бит вектора в ‘0’;
  • $isunknown – возвращает ‘1’, если значение сигнала или вектора равно ‘X’ или ‘Z’;
  • $countones – возвращает количество ‘1’ в векторе (значения ‘X’ и ‘Z’ не считаются).

Share this post