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

Фирюлин Д.И. (науч. рук. Антонов А.А.) РАЗРАБОТКА АРХИТЕКТУРЫ САПР ДЛЯ ДОКАЗАТЕЛЬСТВА ЭКВИВАЛЕНТНОСТИ ПОТАКТОВОЙ И RTL МОДЕЛЕЙ АППАРАТУРЫ // Сборник тезисов докладов конгресса молодых ученых. Электронное издание. – СПб: Университет ИТМО, [2024]. URL: https://kmu.itmo.ru/digests/article/13874