Jump to content

    
Sign in to follow this  
Shivers

Вопрос по SVA

Recommended Posts

Привет!

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

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

Share this post


Link to post
Share on other sites
Есть условие для проверки 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

Share this post


Link to post
Share on other sites

Спасибо!

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

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

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

Share this post


Link to post
Share on other sites
Если я правильно понимаю, то 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

Share this post


Link to post
Share on other sites

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

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

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

Share this post


Link to post
Share on other sites

Привет!

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

 

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

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

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

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

4 ... ?

 

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

 

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

 

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

Share this post


Link to post
Share on other sites
4. используйте "bind" Почитайте SystemVerilog Assertions Design Tricks and SVA Bind Files

Спасибо!

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

 

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

Share this post


Link to post
Share on other sites

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

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

Share this post


Link to post
Share on other sites

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

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

Share this post


Link to post
Share on other sites
Я могу провести для вашей компании такой тренинг для команды до 10 человек.

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

Share this post


Link to post
Share on other sites
...

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

...

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

Share this post


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

 

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

Share this post


Link to post
Share on other sites

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

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

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

Share this post


Link to post
Share on other sites
лучше на хороший тул деньги потратить.

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

 

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

 

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

 

Share this post


Link to post
Share on other sites

Join the conversation

You can post now and register later. If you have an account, sign in now to post with your account.

Guest
Reply to this topic...

×   Pasted as rich text.   Paste as plain text instead

  Only 75 emoji are allowed.

×   Your link has been automatically embedded.   Display as a link instead

×   Your previous content has been restored.   Clear editor

×   You cannot paste images directly. Upload or insert images from URL.

Sign in to follow this