Новости ИСП РАН

Выпущена новая версия MicroTESK (Microprocessor TEsting and Specification Kit) 2.3.

Выпущена новая версия MicroTESK (Microprocessor TEsting and Specification Kit) 2.3. Она включает в себя поддержку генерации тестов для функциональной верификации подсистемы управления памятью микропроцессора. Применяемый подход основан на формальных спецификациях инструкций доступа к памяти (записи и чтения) и модулей памяти, таких как кэш-память и буферы трансляции адресов. Использование формальных спецификаций помогает автоматизировать разработку генераторов тестовых программ и обеспечивает систематичность верификации, позволяя четко задавать цели тестирования. Генератор тестов создает тестовые программы, используя комбинаторные методы. То есть тестовые воздействия в виде последовательностей операций записи и чтения получаются путем перечисления всех допустимых комбинаций инструкций, тестовых ситуаций (путей выполнения инструкций) и зависимостей (наборов конфликтов между инструкциями). Важный момент состоит в том, что информация о тестовых ситуациях и зависимостях автоматически извлекается из спецификаций. Данный подход применим для промышленных проектов и позволяет выявить критические ошибки в механизмах управления памятью.

Более подробная информация доступна здесь.