Перейти к содержанию
    

Привет!

Начал изучать SVA, некоторые простые вещи стали получаться. Сейчас встала задача, которую не могу решить; нужна помощь.

 

Задача:

Есть условие для проверки A |=> ##0 B.

Но! при этом нужно в проверке опустить момент, когда стоит RESET, после чего нужно пропустить два появления строба C, и только после этого начинать проверку.

 

У меня уже получаются простые вещи вида

property pB;
  @(posedge CLK) disable iff(RESET)  A |=> ##0 B;
endproperty

apB: assert property (pB);

 

Попытался вставить сюда секвенцию RESET-C-C

sequence sC
  @(posedge CLK) $rose(RESET)  ##[0:$]  $rose(C)   ##[0:$] $rose(C);
endsequence

property pB;
  @(posedge CLK) disable iff(RESET  | sC.triggered )  A |=> ##0 B;
endproperty

apB: assert property (pB);

Это не работает. Ай нид хелп )

Поделиться сообщением


Ссылка на сообщение
Поделиться на другие сайты

Есть условие для проверки A |=> ##0 B.

Хреновое условие. Наверное, предполагалось A |=> B

То, для чего используют ##0, имеет смысл в event queue в симуляторе. На начальном этапе лучше с этим не играть, т.к это источник потенциально трудно выловимых Gotchas :laughing:

 

Но! при этом нужно в проверке опустить момент, когда стоит RESET, после чего нужно пропустить два появления строба C, и только после этого начинать проверку.

sequence skip_double_c;

(C |=> !C)[*2]; //assuming 1 cycle strobe for C

endsequence

 

sequence b_next_to_a;

A |=> B;

endsequence

 

property pB;

@(posedge CLK) disable iff (RESET)

skip_double_c |=> !c throughout b_next_to_a;

endproperty

Поделиться сообщением


Ссылка на сообщение
Поделиться на другие сайты

Спасибо!

Но есть вопрос:

Если я правильно понимаю, то skip_double_c |=> !c throughout b_next_to_a; это -

сначала ждем однократный сиквенс skip_double_c , а затем в интервале сиквенса b_next_to_a ожидаем !c. Конструкцию throughout я еще не использовал.

Непонятно здесь следующее: этот сиквенс будет ловить однократное RESET-C-C-A |=>B, или же он будет ловить RESET-C-C а затем все повторяющиеся события A |=> B (как нужно мне)?

Попробую погонять на эмуляторе, спасибо еще раз!

Поделиться сообщением


Ссылка на сообщение
Поделиться на другие сайты

Если я правильно понимаю, то skip_double_c |=> !c throughout b_next_to_a; это -

Написано буквально такое: При каждом положительном фронте клока, исключая время, когда RESET выставлен в высокий уровень, симулятор проверяет первое условие (precondition) в виде skip_double_c. Как только sequence skip_double_c выполняется successfully (конечно же, это происходит на положительном фронте клока в момент Х), на следующем фронте (X+1) симулятор проверяет второе условие (consequent).

Второе условие буквально такое: на каждом положительном фронте клока ПОСЛЕ того, как skip_double_c выполнился ХОТЯ БЫ ОДНАЖДЫ, сигнал _с_ должен быть ВСЕ ВРЕМЯ на низком уровне, когда выполняется sequence b_next_to_a.

 

Если провести аналогию с дизайном, этот assertion аналогичен такому: Q || F&&D, только с той разницей, что F&&D будет проверяться ТОЛЬКО после того, как Q выполниться ХОТЯ БЫ РАЗ :laughing:

 

Recommended Readings (в нашей компании - это MUST READ для Verification Engineers)

1. Basic--->Middle: Srikanth_Vijayaraghavan,_Meyyappan_Ramanathan-A_Practical_Guide_for_SystemVerilog_Assertions-Springer

2. Middle --> Advanced: Eduard Cerny, Surrendra Dudani, John Havlicek, Dmitry Korchemny The Power of Assertions in SystemVerilog

 

Попробую погонять на эмуляторе, спасибо еще раз!

Наверное, в симуляторе, а не эмуляторе. Последний - это совсем не то, что наверняка подразумевается в топике. Хотя на FPGA Emulation Tools тоже есть возможность имплементировать assertions, даже synthesizable assertions, результаты которых можно наблюдать на определенных pins ASIC или FPGA

Поделиться сообщением


Ссылка на сообщение
Поделиться на другие сайты

Покрутил, не заработало, пришлось немного изменить. Получилось следующее:

sequence skip_double_c;
  (C ##[0:$] !C)[*2]; //assuming 1 cycle strobe for C
endsequence 

sequence a_next_to_skip;
  skip_double_c ##[0:$] A;
endsequence

property pB;
@(posedge CLK) disable iff (RESET)
a_next_to_skip |=> ##[0:$] B;
endproperty

Конструкции [0:$] ставил, поскольку в тесте все сигналы асинхронные, и задержки постоянно меняются.

 

В общем, работает, но моделирование стало ощутимо тормозить. Моделирование идет примерно в два раза медленнее при отсутствии фоновых задач (Система CoreI5, 16gb, linux64, QuestaSim 6.6C).

 

Есть еще вопрос - в чем лучше всего отлаживать assertions, в каком каде? В квесте можно видеть ассершн, но нельзя (у меня не вышло) выводить на вейвформу отдельные синквенс и проперти.

 

p.s.

Спасибо!

Basic--->Middle: Srikanth_Vijayaraghavan,_Meyyappan_Ramanathan-A_Practical_Guide_for_SystemVerilog_Assertions-Springer

это как раз сейчас и изучаю, первую редакцию

Поделиться сообщением


Ссылка на сообщение
Поделиться на другие сайты

Привет!

Перефразирую предыдущий вопрос - в чем лично вы привыкли моделировать код с проверкой покрытия используя SVA?

 

Вопрос номер два: как лучше всего вставлять ассершны? Я вижу несколько вариантов:

1. вставлять прямо в исходный rtl (если написан на верилоге), поменяв расширение на .sv

2. делать прямо в теле модулей инклуды файлов с ассершнами

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

4 ... ?

 

Я попробовал пойти по пути номер 1 - код быстро стал нечитабельным. Для варианта 3 я слишком ленив ... иду по пути 2. Мне интересно, как поступают профи

 

И еще третий вопрос, тоже задам аккуратно, чтобы избежать холиваров: в каком редакторе вы работаете?

 

У меня сейчас eclipse + veditor+sysveditor, в целом доволен, но все же эти эклипсные модули сыроваты.

Поделиться сообщением


Ссылка на сообщение
Поделиться на другие сайты

4. используйте "bind" Почитайте SystemVerilog Assertions Design Tricks and SVA Bind Files

Спасибо!

Прочитал, попробую. Правда, я так и не понял как работает второй способ бинда, когда вызов производится не из тестбенча, а прямо в коде. Выглядит как обычный вызов модуля, как тогда система понимает что этот файл нужно биндить?

 

Или во втором способе нужно все использумые сигналы передавать через порты, а не только входы/выходы? Вроде в тексте такого не видел

Поделиться сообщением


Ссылка на сообщение
Поделиться на другие сайты

Наверное, все эти вопросы ко мне, так что я постараюсь быть кратким.

Перефразирую предыдущий вопрос - в чем лично вы привыкли моделировать код с проверкой покрытия используя SVA?

На данный момент assertions поддерживают только 3 ASIC симулятора, так что выбор небольшой. Пользуйся тем, который может себе позволить твоя компания.

Вопрос номер два: как лучше всего вставлять ассершны? Я вижу несколько вариантов:

В SOC Microsystems дизайнеры сами пишут assertions. Т.е есть Design Assertions и Verification Assertions. :rolleyes:

Design Assertions могут быть даже synthesizable и мэпяться на external pins.

Я требую от дизайнеров, чтобы они использовали assertions вместе коментов и у них это уже неплохо получается :a14:

Что касается Verification Engineers, они вставляют assertions в Interfaces, в RTL (bind или напрямую - зависит от нескольких факторов), пишут checkers и затем складывают их в Reusable Libraries, которые конечно же по полной используются в следующих проектах.

 

Вообще, в нашей компании верификация и hardware-software co-simulation начинается задолго до самого RTL дизайна, когда checkers пишутся на абстрактном Assertion Language и при помощи их идет Interface Validation между блоками high-level model или BFMs :laughing:

 

И еще третий вопрос, тоже задам аккуратно, чтобы избежать холиваров: в каком редакторе вы работаете?

gvim + куча скриптов под bash, tcl/tk и emacs

 

Судя по всему, ты один из немногих дизайнеров, который занимается ASIC Design/Verification. Verification and Assertions есть своего рода art, которому учаться у других, по крайней мере на ранних стадиях.

 

Тебе лично нужен тренинг. Тебе и другим инженерам в вашей команде. Такой, где инструктор введет в курс дела, профессионально, последовательно покажет, расскажет, объяснит почему. Тренинг, на котором будет куча примерчиков, theory и labs.

 

Я могу провести для вашей компании такой тренинг для команды до 10 человек. Соответсвенно, могу покрыть SV, OVM, UVM, Assertions, Coverage, Verification Metrics, разные виды тулзов, примеры скриптов и опыт ведущих компаний, дать руководителям оценку по времени и трудозатратам для каждого метода, оценить time-to-market и т.д

 

По вопросам стоимости и условий пиши в приват.

Industry Average стоимость и условия можно посмотреть тут: http://www.sutherland-hdl.com/workshop-pricing-terms.php

Поделиться сообщением


Ссылка на сообщение
Поделиться на другие сайты

Огромное спасибо за столь исчерпывающий ответ! Очень много информации к размышлению. К сожалению, в РФ дизайнерские фирмы лишь недавно начали приходить к мысли о необходимости верификации, но поскольку информации по этой тематике практически нет, а стоимость 2-3 перезапусков закладывается в бюджет изначально, то топологии отправляются на завод по старинке, т.с. с божьей помощью ) А фактически, верификацию я вообще както даже и не слышал, что в РФ кто то делает, разве только аутсорсеры вроде спирита или телума .. элвис вроде еще интересовался верификацией. Остальные же отправляют сырые кристаллы прямо так, по нескольку раз - российская специфика.

Лично моя задача сейчас - освоить азы SVA и доказать эффективность руководству фирмы. Если получится, выйдем на новый уровень: будут учиться и другие.

Поделиться сообщением


Ссылка на сообщение
Поделиться на другие сайты

Я могу провести для вашей компании такой тренинг для команды до 10 человек.

Эти классы для особой категории "инженеров". За день или два этому арту не научишся а бабла надо выкладывать ... - лучше на хороший тул деньги потратить.

Поделиться сообщением


Ссылка на сообщение
Поделиться на другие сайты

...

Design Assertions могут быть даже synthesizable и мэпяться на external pins.

...

Возник вопрос: а с какой целью делаются синтезируемые assertions, если в кристалл и так встраиваются scans/mbist/jtag-tap? Это нужно для отладки внешних интерфейсов, или и ядра тоже?

Поделиться сообщением


Ссылка на сообщение
Поделиться на другие сайты

Возник вопрос: а с какой целью делаются синтезируемые assertions, если в кристалл и так встраиваются scans/mbist/jtag-tap? Это нужно для отладки внешних интерфейсов, или и ядра тоже?

 

В параграфе 7.2 немного на эту тему. Я думаю что добавлять синтезируемуе assertions это дополнительный гиморой -спроси синтезис поддержку, спроси про формальную верификацию поддержку. Если нечем заниматься на работе то можно синезировать assertions.

Поделиться сообщением


Ссылка на сообщение
Поделиться на другие сайты

Молодцы, я только начинаю учить и применять SVA.

Планирую его под QuestаSim использовать.

С другой стороны, для ПЛИС цена ошибки ниже, чем для ASIC.

Поделиться сообщением


Ссылка на сообщение
Поделиться на другие сайты

лучше на хороший тул деньги потратить.

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

 

Если нечем заниматься на работе то можно синезировать assertions.

 

Во всяком случае это лучше чем просиживать недели напролет в лаборатории и дебагать дизайн с chip scopе и прочей хренью

 

Поделиться сообщением


Ссылка на сообщение
Поделиться на другие сайты

Присоединяйтесь к обсуждению

Вы можете написать сейчас и зарегистрироваться позже. Если у вас есть аккаунт, авторизуйтесь, чтобы опубликовать от имени своего аккаунта.

Гость
Ответить в этой теме...

×   Вставлено с форматированием.   Вставить как обычный текст

  Разрешено использовать не более 75 эмодзи.

×   Ваша ссылка была автоматически встроена.   Отображать как обычную ссылку

×   Ваш предыдущий контент был восстановлен.   Очистить редактор

×   Вы не можете вставлять изображения напрямую. Загружайте или вставляйте изображения по ссылке.

×
×
  • Создать...