Утверждения (SVA)

Подходы к применению SVA

Разработка утверждений, которые бы в полной мере проверяли поведение устройства, задача нетривиальная. Одно дело, когда пишутся утверждения для таких распространенных протоколов, как PCI, AMBA, OCP. Зачастую, спецификации к таким протоколам уже содержат описания проверок, которые необходимо реализовать с помощью утверждений, и в дальнейшем требуется только реализация. Если же встала...

Read more...

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

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

Read more...

Объявление SystemVerilog утверждений

SystemVerilog утверждения могут быть объявлены напрямую в модуле, program-блоке или интерфейсе. Многие разработчики не любят включать отладочный код в исходное RTL-описание. Для предотвращения такой ситуации, в SystemVerilog поддерживается привязка одного модуля (program-блока или интерфейса) к другому с помощью команды bind. Рассмотрим RTL-описание устройства 2, изображенного на рис. 1: module...

Read more...

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

Типы утверждений Существует 2 типа утвреждений: Immediate — основаны на событиях и выполняются только в процедурном коде; Concurrent — основаны на тактах и могут выполняться как в процедурном коде, так и в модулях, интерфейсах, program-блоках. Immediate утверждения используются только при динамической симуляции. По своей сути они близки к конструкции «if...else» — проверяют выполнение...

Read more...

Свойства. Импликация.

Свойства Свойства определяют отношение между логическими выражениями и последовательностями. Фактически, свойства описывают то, как будет проверяться выполнение последовательности или логического выражения: синхронно или асинхронно; не осуществлять проверку при наличии запрещающего сигнала (например, при активном сигнале сброса); осуществлять проверку только по условию (импликация). В коде программы свойства описываются ключевыми словами property, endproperty: property stable_addr;@(posedge Clk) disable...

Read more...

Последовательности

Последовательности описывают поведение проекта во времени и строятся на основе логических выражений. Выражение «(CMD != `IDLE)» – это простая последовательность, состоящая из одного логического выражения. Сложные последовательности строятся с использованием временных задержек, которые задаются с помощью оператора «##». Рассмотрим построение сложных последовательностей на примере взаимодействия сигналов «a» и «b»:...

Read more...

Структура языка SVA

Язык SVA представляет некое подмножество языка SystemVerilog, что дает возможность применять метод верификации на основе SVA без полного изучения SystemVerilog. Семантика языка SVA схожа с PSL, но есть и ряд новых, по сравнению с языком PSL, возможностей. Структура языка SVA нагляднее всего представляется, как показано на рис. 3. В основе...

Read more...

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

Введение Утверждения описывают поведение системы. В основном они используются для проверки правильности поведения проекта. Также с помощью утверждений можно оценить полноту функционального покрытия. Метод верификации на основе утверждений подразумевает расстановку ...

Read more...