[Shivers 0]

Привет!

Начал изучать 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);

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

[mttphreak 0]

Есть условие для проверки 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

[Shivers 0]

Спасибо!

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

Если я правильно понимаю, то 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 (как нужно мне)?

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

[mttphreak 0]

Если я правильно понимаю, то 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

[Shivers 0]

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

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

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

[Shivers 0]

Привет!

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

 

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

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

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

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

4 ... ?

 

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

 

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

 

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

[agate 0]

4 ... ?

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

[Shivers 0]

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

Спасибо!

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

 

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

[mttphreak 0]

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

Перефразирую предыдущий вопрос - в чем лично вы привыкли моделировать код с проверкой покрытия используя 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

[Shivers 0]

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

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

[agate 0]

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

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

[Shivers 0]

...

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

...

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

[agate 0]

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

 

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

[myq 0]

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

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

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

[Mad_kvmg 0]

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

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

 

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

 

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