Проект ИСП РАН: Разработка инструментов верификации САПР цифровых СБИС

Важным этапом процесса проектирования цифровой микроэлектронной аппаратуры является логический синтез — построение логической схемы в заданном технологическом базисе по RTL-модели (Register Transfer Level, уровень регистровых передач), представленной на языке описания аппаратуры (Verilog [1] или VHDL [2]). На данном этапе проводятся следующие преобразования: 

1. построение внутреннего представления схемы;
2. оптимизация внутреннего представления по заданным критериям (площадь, общая задержка, энергопотребление);
3. отображение схемы на элементы технологической библиотеки (технологическое отображение).

Обеспечение корректности этих преобразований критически важно для функционирования средств логического синтеза в целом. Основным подходом в данной области является проверка логической эквивалентности (Logic Equivalence Checking, LEC) схем до и после преобразований.
Проект выполняется в рамках работ по созданию среды логического синтеза Utopia EDA, разрабатываемой в Институте системного программирования им. В. П. Иванникова Российской академии наук (ИСП РАН).

Целью проекта является создание инструментов проверки корректности средств логического синтеза, входящих в САПР цифровой микроэлектронной аппаратуры.

Ожидаемые результаты

1. компонент проверки эквивалентности, основанный на открытой системе EQY
2. компонент проверки эквивалентности, основанный на алгоритме Кюльмана (Рис. 1)
3. набор модульных тестов для разработанных компонентов проверки эквивалентности
4. тестовый набор для сравнительной оценки производительности и корректности разработанных компонентов проверки эквивалентности (сравнение должно проводиться, в том числе, с использованием данных о времени проверки схем с помощью проприетарных САПР)
5. средства анализа и визуализации результатов тестирования компонентов проверки эквивалентности, внедренные в систему непрерывной интеграции (Continuous Integration, CI) проекта Utopia EDA.

Разрабатываемые компоненты проверки эквивалентности (1-2) должны принимать на вход две проверяемые логические схемы, представленные в примитивах внутреннего представления, используемого в проекте Utopia EDA. Компоненты проверки эквивалентности должны возвращать результат, содержащий следующие поля:

1. вердикт (схемы эквивалентны, схемы не эквивалентны, результат проверки не определен, внутренняя ошибка)
2. контрпример (в текстовом формате и в формате VCD [1])

Используемые технологии

Проект предполагает применение следующих технологий и инструментов:

• Языки описания аппаратуры:
  • Verilog (по стандарту IEEE Std 1364-2005).
  • VHDL (по стандарту IEEE Std 1076-2008).
• Алгоритмы и методы проверки эквивалентности схем:
  • Алгоритм Кюльмана и Кроха для проверки эквивалентности, основанный на методах разрезов и кучи (Cuts and Heaps).
  • Система EQY для проверки логической эквивалентности.
• Программное обеспечение:
  • Среда разработки и интеграции Utopia EDA, разрабатываемая Институтом системного программирования им. В. П. Иванникова РАН.
  • Инструменты для интеграции с инфраструктурой CI/CD: GitLab CI.
• Форматы и стандарты данных:
  • VCD (Value Change Dump) для представления контрпримеров.
  • Примитивы внутреннего представления, применяемые в среде Utopia EDA для описания схем.
• Инструменты разработки и тестирования:
  • Средства модульного тестирования (в рамках CI/CD).
  • Генераторы тестов для производительности и корректности проверки эквивалентности.
  • Средства визуализации результатов тестов.

Исходные данные проекта

На данный момент задел определяется выполнением данного проекта в прошлом учебном году, когда были разработаны, основанные на известных методах и подходах, но требующие доработки и оптимизации для использования в реальном маршруте проектирования цифровых СБИС:

• компоненты проверки эквивалентности комбинационных схем
• компонент проверки эквивалентности последовательностных схем
• компонент генерации схем-мутантов
• набор средств, обеспечивающих использование инфраструктуры CI/CD и средств контейнеризации в проекте

Заказчик проекта

Организация / Федеральное государственное бюджетное учреждение науки Институт системного программирования им. В. П. Иванникова Российской академии наук (ИСП РАН)

Команда проекта

• Ильина Екатерина Сергеевна - Программист на C++
• Круглов Артём Евгеньевич - Программист на C++
• Пащенко Ярослав Владимирович - Программист на C++
• Ржевская Мария Михайловна - Программист на C++
• Соснин Артём Олегович - Программист на C++