Practical Aspects of Formal Verification of Networking Chips

 
Sokhatski A.A. (Cisco Systems Inc.)
 
Abstract - Formal Verification (FV) is becoming now important part of Design Verification (DV) especially for areas which has higher requirements for quality of chips such as networking chips which should work 24x7 without failures while re-spin cost for huge chips is high. It is difficult to cover all possible scenarios by simulation having a lot of corner cases for packet alignments, sizes, combinations of values of configuration ports and registers. Formal Verification should be able to help to improve quality and reduce Time to Market but it requires: - Selection of right scope, candidate and method for Formal Verification; - Addressing Formal challenges main of such is fighting with complexity and exponential grow of proof time with each proof cycle; - Consistent Methodology to ensure verification coverage and to reduce effort. The paper goes through those aspects basing on experience at Cisco Systems Inc. with help from OSKI Technology [1], Formal Verification service provider and Formal sign-off company [2]. The paper covers: 1) Brief review of Formal Applications while concentrating on End-to-End Formal sign-off for Design Modules along with criteria for selection of good candidates for Formal; 2) Structure of simple Formal Environment; 3) Methods helping to fight with complexity which author found especially useful for data transport modules of networking chips, such as floating pulse method, Wolper method, use of abstraction models; 4) Formal methodology aspects including: - Document and test plan flow; - Run Flow, Regression & Scripting; - Coverage Flow; - Reuse for Formal & Simulation.

Keywords - Design Verification, Formal Verification, SystemVerilog, SVA.

Практические аспекты формальной верификации проектов блоков сетевых СБИС

 
Сохацкий А.А. (Сиско Системс Инк., г. Сан Хосе)
 
Аннотация - Формальная верификация в наши дни становится важной составляющей верификации проектов цифровых блоков в особенности в областях, предъявляющих повышенные требования к качеству проверки. Так сетевые СБИС должны фунционировать безошибочно без перерывов в течении длительного времени, при том, что перепроектирование и повторное изготовление этих коплексных микросхем требует существенных затрат. Довольно сложно проверить функционирование на всех возможных входных последовательностях путем моделирования при наличии множества граничных условий связанных с различной длиной и выравниванием пакетов, комбинациями значений входных настроечных портов и регистров. Формальные методы должны помочь достичь полноту проверки и сократить время разработки , но это требует: - правильной стратегии выбора блоков и модулей проекта для формальной верификации, а также метода формальной верификации; - применения решений для ответа на проблему экспотенциального роста времени формального доказательства в зависимости от глубины доказательства; - последовательной методологии для обеспечения верификационного покрытия и сокращения затрат. В статье рассматриваются аспекты формальной верификации на основе опыта работы автора в компании Сиско Системс Инк. и консультаций поставщика услуг формальной верификации компании OSKI Technology. Излагаются следующие аспекты: 1) Краткий обзор применений формальной верификации. При этом статья фокусируется на задаче полной (sign-off) сквозной проверки (end-to-end check) отдельных модулей проекта. Рассатриваются вопросы выбора модулей для формальной веривикации; 2) Структура простого окружения для формальной верификации; 3) Методы, позволяющие увеличить глубину доказательства, в частности, использование символических переменных, символического выбора элемента последовательности с применением плавающего импульса (floating pulse), метод Волпера (Wolper), использование абстрактных моделей; 4) Аспекты методологии формальной верификации, включая технологии планирования, документирования, исполнения и регрессионных последовательностей, покрытия проекта, совместного использования для формальной верификации и моделирования

Ключевые слова - СБИС, формальная верификация, моделирование, RTL, SystemVerilog, SVA.