Генерация тестовых программ для микропроцессоров, виртуальных машин и компиляторов

• Моделирование систем команд микропроцессоров и виртуальных машин.
• Автоматическое построение тестовых программ по моделям.
• Инфраструктура для online-генерации тестовых программ.
• Тестирование механизмов управления памятью многоядерных микропроцессоров.

Высокоуровневый синтез моделей цифровой аппаратуры

• Распределение ресурсов и планирование вычислений.
• Организация библиотеки элементов и генерация IP-блоков.
• Логическая оптимизация цифровых схем.
• Генерация битовых потоков для ПЛИС.

Формальная верификация HDL-описаний цифровой аппаратуры

• Проверка моделей цифровой аппаратуры.
• Проверка эквивалентности моделей цифровой аппаратуры.

Формальная верификация бинарных программ на основе спецификации системы команд

• Декодирование, внутреннее представление и трансформация бинарных программ.
• Дедуктивная верификация бинарных программ на соответствие спецификациям уровня исходного кода.
• Проверка эквивалентности бинарных программ.

К.ф.-м.н. Александр Камкин