Главная         Авторы   Статьи   Год проведения   Тематика   Организации        Конференция МЭС

Практические аспекты формальной верификации проектов блоков сетевых СБИС
Авторы
	Сохацкий А.А.
Год публикации
	2018
DOI
	10.31114/2078-7707-2018-2-16-22
УДК
	519.714
Аннотация
	Формальная верификация в наши дни становится важной составляющей верификации проектов цифровых блоков в особенности в областях, предъявляющих повышенные требования к качеству проверки. Так сетевые СБИС должны фунционировать безошибочно без перерывов в течении длительного времени, при том, что перепроектирование и повторное изготовление этих коплексных микросхем требует существенных затрат. Довольно сложно проверить функционирование на всех возможных входных последовательностях путем моделирования при наличии множества граничных условий связанных с различной длиной и выравниванием пакетов, комбинациями значений входных настроечных портов и регистров. Формальные методы должны помочь достичь полноту проверки и сократить время разработки , но это требует: - правильной стратегии выбора блоков и модулей проекта для формальной верификации, а также метода формальной верификации; - применения решений для ответа на проблему экспотенциального роста времени формального доказательства в зависимости от глубины доказательства; - последовательной методологии для обеспечения верификационного покрытия и сокращения затрат. В статье рассматриваются аспекты формальной верификации на основе опыта работы автора в компании Сиско Системс Инк. и консультаций поставщика услуг формальной верификации компании OSKI Technology. Излагаются следующие аспекты: 1) Краткий обзор применений формальной верификации. При этом статья фокусируется на задаче полной (sign-off) сквозной проверки (end-to-end check) отдельных модулей проекта. Рассатриваются вопросы выбора модулей для формальной веривикации; 2) Структура простого окружения для формальной верификации; 3) Методы, позволяющие увеличить глубину доказательства, в частности, использование символических переменных, символического выбора элемента последовательности с применением плавающего импульса (floating pulse), метод Волпера (Wolper), использование абстрактных моделей; 4) Аспекты методологии формальной верификации, включая технологии планирования, документирования, исполнения и регрессионных последовательностей, покрытия проекта, совместного использования для формальной верификации и моделирования
Ключевые слова
	СБИС, формальная верификация, моделирование, RTL, SystemVerilog, SVA.
Ссылка на статью
	Сохацкий А.А. Практические аспекты формальной верификации проектов блоков сетевых СБИС // Проблемы разработки перспективных микро- и наноэлектронных систем. 2018. Выпуск 2. С. 16-22. doi:10.31114/2078-7707-2018-2-16-22
Адрес статьи
	http://www.mes-conference.ru/data/year2018/pdf/D123.pdf