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

    

radigast

Участник
  • Публикаций

    7
  • Зарегистрирован

  • Посещение

Репутация

0 Обычный
  1. Довольно узкая задача, но иногда возникает при разработке ASIC – экспресс моделирование нетлиста блока, подготавливаемого, например, как хардмакро, для интеграции в топологию более высокого уровня. С помощь CB очень удобно управлять временными разбежками между клоком и данными. Во всяком случае это намного проще, чем для каждого сигнала в отдельности внедрять линии задержки. Некоторые сторонние модели, с которыми мы работали, имели особенности поведения при наличии гонок сигналов. Для них также наиболее простым способом было просто настроить задердку в CB. В остальном при штатном цифровом моделировании (если нет необходимости явным образом играться с задержками клок - данные) кроме дополнительной инкапсуляции наверное бонусов особых нет, зато есть ряд дополнительных проблем при отладке агентов, поскольку сигнал интерфейса не равен сигналу внутри клокинг блока.
  2. Вставлю свои пять копеек в эту тему. Есть следующие основные подходы к моделированию аппаратуры до выпуска тестового чипа: высокоуровневая TLM/ISS модельсобственно RTLПЛИСускорители/эмуляторы RTL является непосредственном источником для дальнейшего проектирования ИС (если вы не используете HLS, который, на мой взгляд, пока применим только для отдельных подблоков, преимущественно аппаратных акселераторов какой-либо сложной математики). Поэтому хочешь - не хочешь, а RTL перед отправкой на финальный синтез моделировать придется. Также как потом придется моделировать и полученные нетлисты. Причем, даже при условии, что все уже было проверено в ПЛИС (как уже упоминалось, прототип в ПЛИС и RTL под синтез в ИС это не одно и тоже и, как минимум, придется перепроверять подключение макро памятей и физики) Что касается дополнительного использования трёх оставшихся способов моделирования, то тут очень все зависит от типа устройства, ресурсов и времени, которые выделены на этот проект. TLM/ISS на этапе проработки архитектуры хороши: можно поисследовать утилизацию архитектуры на реальных задачах, прикинуть разбиение алгоритма на HW/SW. Но реальные цифры по производительности на ней не получишь, реальный драйвер тоже не отладишь. Все-таки в RTL слишком много особенностей реализации, которые сложно учесть на этом этапе проектирования, а они бывает существенно сказываются на результатах работы ПО. Потактовые модели ядер для данного уровня бывают, но это уже оптимизированные модели, сделанные для готового и апробированного RTL, который продается как IP. И тут речь уже идет скорее не о разработке таких моделей, а об экстракции из RTL и дальнейшей оптимизации (свободные тулы для этого — verilator, слышал о такой конторе как Carbon, которые профессионально этим занимаются). С другой стороны моделирование RTL является слишком медленным для реальных задач, без которого не будет обратной связи по производительности, удобству программирования, и останется риск пропуска архитектурных и «хитрых» ошибок. В этом контексте ПЛИС идеально подходят для прототипирования: вычислительных ядеракселераторовсложной, но стандартной периферии, типа ethernet со встроенным алгоритмами обработки пакетов, и.т.п Моделирование RTL, при этом, все равно никуда не уходит. Ставить непроверенный RTL в ПЛИС и тратить сутки на пересинтез и дебаг мелких багов, которые можно отловить за минуты/часы моделирования RTL — удовольствие ниже среднего. При этом ПЛИС почти неприменимы для прототипирования периферии с собственной физикой. Серьезные сложности возникают при попытке прототипировать целиком проекты больших СнК. Для последней задачи как раз можно пользоваться эмуляторами. К слову в эмуляторах типа Palladium уже ставят не ПЛИС, а специализированные ASICи. Правда практика показывает, что для больших проектов эмуляторы супер скоростей не показывают, это в лучшем случае десятки — сотни килогерц для больших систем. Жирные западные компании, как правило, имеют целые здания забитые серверами, число которых стремится к бесконечности и счетное число эмуляторов. В таких условиях запустить тысячи симуляций RTL может оказаться более быстрым способом проверки, чем использование эмулятора. Так, что с эмуляторами тоже не все так однозначно — все определяется теми возможностями, которые есть у компании. Опять же, для больших проектов возни с ПЛИС и эмуляторами может быть очень много.
  3. Цитата(Poluektovich @ Nov 16 2016, 18:22) Пока нигде не учат. Но планируется курс по верификации в рамках магистратуры МИЭТ. А на какой кафедре планируете читать? На ИЭМС, к примеру, уже читается курс "разработка и верификция СФ-блоков", в рамках которого в том числе читается и введение в UVM.
  4. Лично не работал, но среди симуляторов на слуху ещё QEMU. Он в отличии от IMPERAS полностью свободный и также позволяет настраивать архитектуру эмулируемой системы. Вот тут (видео на ютубе) есть видео доклада, в котором он используется для отладки ПО перед запуском на железе.
  5. Цитата(Poluektovich @ Nov 14 2016, 14:33) НИИСИ использовали Jasper для проверки connectivity на системном уровне, регистрового пространства. см JasperGold Applications Approach for Verification Workflow of SRISA Project Да, мы видели такое приложение (APP как они его называют). Но на мой скромный взгляд это самое тривиальное из того что можно доказать формально, собственно поэтому вопросов к работоспособности и масштабируемости именно этого приложения практически нет. А вот случаи посложнее, типа доказательства соответствия RTL реализации заданному протоколу для всех возможных воздействий, такой уверенности пока не вселяли. Подозреваю, что там есть множество ограничений. Более того, приложение проверки коннективити, насколько я понял (если не прав - поправьте), использует сторонний файл с описанием требуемой карты связности (который создаётся ручками). В таком случае от двойной ошибки и в списке связности и в RTL вызванной непониманием особенностей взаимодействия блоков страховки все равно нет. Ещё один момент — текущий уровень автоматизации создания систем. Многие блоки сейчас поставляются с IP-XACT ( ссылка_ip_xact) описанием, в котором, в том числе возможно функциональное объединение пинов в интерфейсы, которые на системном уровне подключаются друг у другу автоматически. Современные средства сборки СнК позволяют задавать каркас будущей системы, её карту памяти и теоретически такая система в части связности должна быть корректна от рождения. Во всяком случае серьёзных проблем именно с картой памяти или подключением стандартных интерфейсов в таких системах я не помню. Т.е. приложение то рабочее, но не самое эффектное с точки зрения влияния формалки на маршрут верификации. На прошедшей в 2016 году конференции МЭС была целая секция посвящённая функциональной верификации, на которой в том числе обсуждались и теоретические аспекты формальной верификации (МЭС. расписание секции функциональной верификации). Один из орг выводов — русскоязычного сообщества верификаторов пока нет, а в силу скорости развития этого направления лучше держаться вместе. Данный форум — это площадка для живого обсуждения практических вопросов и обмена материалами и мнениями. Кроме того мы создали на FaceBook группу с пафосным названием «Российское сообщество верификаторов» (ссылка на группу). Пока она работает в режиме новостной ленты с информацией о научных и практических конференциях или событиях, связанных с функциональной верификацией. Если у кого есть интерес — подписывайтесь.
  6. Приветствую коллег в этой ветке! С момента последнего сообщения прошло уже 4 года, за это время тулы и методики формальной верификации заметно подросли. В этой связи позволю себе освежить тему вопросом по статусу практического опыта использования формальных методов верификации. Если использованием ABV в динамике сейчас никого не удивишь (SVA/OVL активно используются), то вот про опыт промышленного применения формальных подходов слышно не так часто. Последний раз, когда мы пробовали на базе ABV формально верифицировать блоки сложнее АЛУ натыкались на логичную проблему комбинаторного взрыва. Чтобы процесс сошёлся при жизни запускающего его инженера требовалось задавать слишком уж жёсткие ограничения, что негативно сказывается на достигаемом покрытии. Собственно вопрос (если не секрет): именно в «боевых» проектах блоки какой сложности удавалось проверить формально на базе ABV/model checking, какие тулы при этом использовались (может у кого есть опыт работы с теми же ABVVIP от Cadene?)
  7. Цитата(_Ivan_33 @ Oct 6 2016, 18:22) Questasim Спасибо за мнение, но. Как раз у меня случай с авионикой. DO-254, 10^-9 вероятность отказа и прочее. И если ошибка - погибнут люди. А я потом спать не буду и все такое. Сейчас примерно смотрю - у меня по code coverage - переходы автомата из состояния в IDLE состояние по резету нету покрытия и default в автомате. Но так как там еще будет вотчдог, то наверное придется рушить автомат для покрытия этого и смотреть. В любом случае uvm это дело очень сильно упрощает и если я раньше думал что это гвозди микроскопом, то сейчас мне кажется при reusability модулей тестбенча это все весьма прекрасно. Я бы даже больше сказал. На моей практике у правила «то что не проверено - не работает» исключений практически не было. Поэтому если блок является критическим узлом будущей системы лучше к нему отнестись с должным уважением. Последнее время мы стараемся доводить такие блоки до 100% покрытия (да, осознанные исключения отдельных состояний могут иметь место, особенно если речь идёт про стиль RTL, учитывающий X пессимизм, см. «The Dangers of Living with an X») Более того, надо понимать, что покрытие кода это не панацея. Если есть непокрытый участок кода — у вас точно дыра в тестах. Если у вас 100% покрытие кода, это ещё не гарантия того, что все ошибки фиксируются. Примеры: Тест на фичу при исполнении фоном дёргаёт сигналы устройства, которые явно не завязаны на результат работы данного теста, но являются важными для другой фичи, на которую теста ещё нет. Анализ покрытия в этом случае может оказаться слишком оптимистичным. (Лечится совмещением CDC подхода, классического тестового плана и функционального покрытия).Тест может быть написан, но при прохождении неполноценно контролировать результат. (методы борьбы — дополнительные assertions, методы анализа качества тестов на базе проверки фиксации ошибок в коде см. средства типа Synopsys certitude)Сложные автоматы типа блоков управления конвейером процессоров без функционального покрытия вообще небезопасно проверять (тут также 100% покрытие кода лишь первый шаг). Понятно что это идеальная картина и в реальных проектах и жёстких сроках не всегда достижимая. Где-то могут помочь изначально заданные ограничения условий применения блока/устройства и или четко определенные сценарии использования, которые могут снизить требования к покрытию. Некоторые блоки не имеют критической важности для проекта и муштровать их до потери пульса смысла нет. Но стремиться к идеалу надо, особенно если речь идёт об ASIC и серьёзных проектах.