Генерация тестовых программ для микропроцессоров, виртуальных машин и компиляторов
- Моделирование систем команд микропроцессоров и виртуальных машин.
- Автоматическое построение тестовых программ по моделям.
- Инфраструктура для online-генерации тестовых программ.
- Тестирование механизмов управления памятью многоядерных микропроцессоров.
Высокоуровневый синтез моделей цифровой аппаратуры
- Распределение ресурсов и планирование вычислений.
- Организация библиотеки элементов и генерация IP-блоков.
- Логическая оптимизация цифровых схем.
- Генерация битовых потоков для ПЛИС.
Формальная верификация HDL-описаний цифровой аппаратуры
- Проверка моделей цифровой аппаратуры.
- Проверка эквивалентности моделей цифровой аппаратуры.
Формальная верификация бинарных программ на основе спецификации системы команд
- Декодирование, внутреннее представление и трансформация бинарных программ.
- Дедуктивная верификация бинарных программ на соответствие спецификациям уровня исходного кода.
- Проверка эквивалентности бинарных программ.
К.ф.-м.н. Александр Камкин