[warrior-2001 0]

Доброе время суток.

 

warrior-2001, делали ли вы оценку покрытия и какие цифры удавалось?

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

 

Платформой Questa мы не пользуемся, но он интересен наличием библиотеки QVL.

Cadence предлагает в своем портфолио ABVVIP для системных шин AMBA/OCP и контроллеров памятей, остальные VIP только для динамики. В библиотеке QVL имеется хороший набор последовательных интерфейсов.

Если проверяли последовательные интерфейсы каких усилий стоит получение статусных состояний по всему набору утверждений? Использовалась ли гибридная верификация (формальный анализ + динамическая симуляция)?

 

Если честно - мне результаты не понравились. И проблема именно в трудозатратах. Дело в том, что для формальной проверки проект должен быть изначально на это ориентирован. И когда в компании уже есть большое кол-во СФ блоков, разработанных и отлаженных ранее, то когда они вставляются в проект - они выпадают из области покрытия и результирующие цифры уж очень не красивые. Если же тестировать отдельно СФ блок - то в большинстве случаев удается проверить его работу так сказать по полному графу. То есть перебрать весь набор входных воздействия и сравнить с эталоном.

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

По поводу гибридной верификации - мы пишем тестовые окружения на SV и занимаемся верификаций в QuestaSim. Отдельно моделировать проекты смысла нет.

[radigast 0]

Приветствую коллег в этой ветке!

 

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

Если использованием ABV в динамике сейчас никого не удивишь (SVA/OVL активно используются), то вот про опыт промышленного применения формальных подходов слышно не так часто.

Последний раз, когда мы пробовали на базе ABV формально верифицировать блоки сложнее АЛУ натыкались на логичную проблему комбинаторного взрыва. Чтобы процесс сошёлся при жизни запускающего его инженера требовалось задавать слишком уж жёсткие ограничения, что негативно сказывается на достигаемом покрытии.

Собственно вопрос (если не секрет): именно в «боевых» проектах блоки какой сложности удавалось проверить формально на базе ABV/model checking, какие тулы при этом использовались (может у кого есть опыт работы с теми же ABVVIP от Cadene?)

[Poluektovich 0]

НИИСИ использовали Jasper для проверки connectivity на системном уровне, регистрового пространства.

см JasperGold Applications Approach for Verification Workflow of SRISA Project

[radigast 0]

НИИСИ использовали Jasper для проверки connectivity на системном уровне, регистрового пространства.

см JasperGold Applications Approach for Verification Workflow of SRISA Project

 

Да, мы видели такое приложение (APP как они его называют). Но на мой скромный взгляд это самое тривиальное из того что можно доказать формально, собственно поэтому вопросов к работоспособности и масштабируемости именно этого приложения практически нет. А вот случаи посложнее, типа доказательства соответствия RTL реализации заданному протоколу для всех возможных воздействий, такой уверенности пока не вселяли. Подозреваю, что там есть множество ограничений.

Более того, приложение проверки коннективити, насколько я понял (если не прав - поправьте), использует сторонний файл с описанием требуемой карты связности (который создаётся ручками). В таком случае от двойной ошибки и в списке связности и в RTL вызванной непониманием особенностей взаимодействия блоков страховки все равно нет. Ещё один момент — текущий уровень автоматизации создания систем. Многие блоки сейчас поставляются с IP-XACT ( ссылка_ip_xact) описанием, в котором, в том числе возможно функциональное объединение пинов в интерфейсы, которые на системном уровне подключаются друг у другу автоматически. Современные средства сборки СнК позволяют задавать каркас будущей системы, её карту памяти и теоретически такая система в части связности должна быть корректна от рождения. Во всяком случае серьёзных проблем именно с картой памяти или подключением стандартных интерфейсов в таких системах я не помню. Т.е. приложение то рабочее, но не самое эффектное с точки зрения влияния формалки на маршрут верификации.

 

На прошедшей в 2016 году конференции МЭС была целая секция посвящённая функциональной верификации, на которой в том числе обсуждались и теоретические аспекты формальной верификации (МЭС. расписание секции функциональной верификации). Один из орг выводов — русскоязычного сообщества верификаторов пока нет, а в силу скорости развития этого направления лучше держаться вместе.

Данный форум — это площадка для живого обсуждения практических вопросов и обмена материалами и мнениями. Кроме того мы создали на FaceBook группу с пафосным названием «Российское сообщество верификаторов» (ссылка на группу). Пока она работает в режиме новостной ленты с информацией о научных и практических конференциях или событиях, связанных с функциональной верификацией. Если у кого есть интерес — подписывайтесь.

[Мур 1]

:smile3009: спешите!!!!

Вот учебник по параллельному программированию ПЛИС

 

https://arxiv.org/abs/1805.03648