?
Specification-Based Test Program Generation for ARM VMSAv8-64 Memory Management Units
P. 1–6.
Shushpanov I., Suslov K., Ilyushin P. и др., Energies 2021 No. 14 Article 6193
Добавлено: 29 декабря 2021 г.
Камкин А. С., Чупилко М. М., Смолов С. А. и др., , in: 2018 19th International Workshop on Microprocessor and SOC Test and Verification (MTV).: Austin: IEEE Computer Society, 2018. P. 6–11.
Добавлено: 3 июля 2019 г.
Кудряшов Е. А., Мельник Д. М., Монаков А. В., Труды Института системного программирования РАН 2016 Т. 28 № 1 С. 63–80
В статье рассматривается подход к оптимизации вызовов внешних функций в позиционно-независимом коде, основанный на выдаче вызовов непосредственно через глобальную таблицу смещений (GOT), минуя таблицу компоновки процедур (PLT). Стандартные механизмы кодогенерации на операционной системе Linux предполагают создание PLT не только для основного модуля (который является позиционно-зависимым и полагается на механизм PLT для вызовов внешних процедур), но ...
Добавлено: 5 ноября 2018 г.
Камкин А. С., М.: МАКС Пресс, 2018.
Книга является учебным пособием по формальным методам верификации программ и основана на курсах лекций, читаемых автором на факультете ВМК МГУ имени М.В. Ломоносова, ФУПМ МФТИ и ФКН ВШЭ. В ней изложены основы таких подходов, как дедуктивный анализ и проверка моделей. Список тем включает: методы формализации семантики языков программирования (операционная и аксиоматическая семантика), методы формальной спецификации ...
Добавлено: 2 ноября 2018 г.
Татарников А. Д., Камкин А. С., Проценко А. С. и др., Проблемы разработки перспективных микро- и наноэлектронных систем (МЭС) 2018 № 2 С. 2–8
В работе рассматривается генератор тестовых программ, предназначенный для верификации микропроцессоров с архитектурой RISC-V. Генератор разработан на основе инструмента MicroTESK и состоит из формальных спецификаций архитектуры RISC-V и архитектурно независимого ядра. Спецификации задают синтаксис и семантику команд. Ядро реализует техники построения последовательностей команд и генерации данных. Генерация осуществляется на основе шаблонов, описывающих структурные и поведенческие свойства программ. Инструмент позволяет расширять ...
Добавлено: 30 октября 2018 г.
Yaroslavl: Ярославский государственный университет им. П.Г. Демидова, 2018.
Добавлено: 26 октября 2018 г.
Камкин А. С., Татарников А. Д., Проценко А. С. и др., , in: 2017 18th International Workshop on Microprocessor and SOC Test and Verification (MTV).: IEEE, 2017. P. 10–14.
Добавлено: 18 июля 2018 г.
Создание тестовых программ и анализ результатов их выполнения — основной подход к функциональной верификации микропроцессоров на системном уровне. Имеется множество методов автоматизации разработки тестовых программ, начиная от генерации случайного кода и заканчивая нацеленным построением тестов на основе моделей, однако панацеи не существует: на практике применяются комбинации различных техник, дополняющих друг друга. К сожалению, в настоящее ...
Добавлено: 5 февраля 2018 г.
Татарников А. Д., Известия высших учебных заведений. Физика 2016 Т. 59 № 8-2 С. 97–100
В работе предлагается метод автоматизированного построения поведенческих моделей микропроцессоров, используемых при генерации тестовых программ для предсказания результатов их выполнения. Предложенный метод основан на использовании формальных спецификаций системы команд. Данный метод реализован в инструменте MicroTESK, разработанном в ИСП РАН. Инструмент успешно применяется для верификации промышленных микропроцессоров. ...
Добавлено: 2 февраля 2018 г.