?
MicroTESK: An ADL-Based Reconfigurable Test Program Generator for Microprocessors
P. 64-69.
В книге
Камкин А., Петренко А., Терехов А. Perm : -, 2012
Создание тестовых программ и анализ результатов их выполнения — основной подход к функциональной верификации микропроцессоров на системном уровне. Имеется множество методов автоматизации разработки тестовых программ, начиная от генерации случайного кода и заканчивая нацеленным построением тестов на основе моделей, однако панацеи не существует: на практике применяются комбинации различных техник, дополняющих друг друга. К сожалению, в настоящее ...
Добавлено: 5 февраля 2018 г.
Татарников А. Д., Проблемы разработки перспективных микро- и наноэлектронных систем (МЭС) 2016 Т. II С. 38-45
Генерация тестовых программ и анализ результатов их симуляции на проектной модели являются основным подходом к функциональной верификации микропроцессоров. Верификация – крайне трудоемкий процесс. По некоторым оценкам затраты на нее составляют около 70% от общих трудозатрат на разработку микропроцессора. Это связано с тем, что логика работы современных микропроцессоров содержит огромное количество состояний, и для того, чтобы ...
Добавлено: 12 декабря 2017 г.
Татарников А. Д., Proceedings of the Institute for System Programming of the RAS 2016 Vol. 28 No. 4 P. 77-98
Генерация тестовых программ на языке ассемблера и проверка корректности результатов их выполнения является наиболее широко применяемым подходом к функциональной верификации микропроцессоров. Данная задача решается при помощи специальных автоматизированных средств, называемых генераторами тестовых программ. Высокая сложность современных электронных устройств создает потребность в автоматизированных средствах, способных генерировать тестовые программы, покрывающие нетривиальные ситуации в их работе. Большинство таких ...
Добавлено: 26 ноября 2017 г.
Татарников А. Д., , in : Proceedings of IEEE East-West Design & Test Symposium (EWDTS'2016). : Yerevan : IEEE, 2016. P. 270-273.
Добавлено: 22 декабря 2017 г.
Татарников А. Д., Камкин А. С., Чупилко М. М. и др., , in : Hardware and Software: Verification and Testing. HVC 2017. Lecture Notes in Computer Science. Vol. 10629: 13th International Haifa Verification Conference, HVC 2017, Haifa, Israel, November 13-15, 2017.: Cham : Springer, 2017. P. 217-220.
Добавлено: 24 января 2018 г.
Татарников А. Д., Камкин А. С., Проценко А. С. и др., Труды Института системного программирования РАН 2016 Т. 28 № 6 С. 87-102
ARM — это семейство микропроцессорных архитектур, разработанных в одноименной компании. Новейшая архитектура этого семейства, ARMv8, содержит большое число команд разных типов и отличается сложной организацией виртуальной памяти (включающей аппаратную поддержку многоуровневой трансляции адресов и виртуализации); все это делает функциональную верификацию микропроцессоров этой архитектуры крайне трудной технической задачей. Неотъемлемой частью верификации микропроцессора является генерация тестовых программ ...
Добавлено: 24 ноября 2017 г.
Татарников А. Д., Камкин А. С., Проценко А. С., Proceedings of the Institute for System Programming of the RAS 2015 Vol. 27 No. 3 P. 125-138
Подсистема памяти является одним из ключевых компонентов микропроцессора. Она включает в себя набор запоминающих устройств различного назначения, объединенных в сложную иерархическую структуру. При этом количество возможных состояний подсистемы крайне велико. По этой причине верификация ее функциональной корректности представляет собой нетривиальную задачу. В настоящее время наиболее часто применяемым на практике подходом к функциональной верификации микропроцессоров является ...
Добавлено: 10 декабря 2017 г.
Татарников А. Д., Камкин А. С., Проценко А. С. и др., Проблемы разработки перспективных микро- и наноэлектронных систем (МЭС) 2018 № 2 С. 2-8
В работе рассматривается генератор тестовых программ, предназначенный для верификации микропроцессоров с архитектурой RISC-V. Генератор разработан на основе инструмента MicroTESK и состоит из формальных спецификаций архитектуры RISC-V и архитектурно независимого ядра. Спецификации задают синтаксис и семантику команд. Ядро реализует техники построения последовательностей команд и генерации данных. Генерация осуществляется на основе шаблонов, описывающих структурные и поведенческие свойства программ. Инструмент позволяет расширять ...
Добавлено: 30 октября 2018 г.
Татарников А. Д., Камкин А. С., , in : Perspectives of System Informatics - 11th International Andrei P. Ershov Informatics Conference, PSI 2017, Moscow, Russia, June 27-29, 2017, Revised Selected Papers, Lecture Notes in Computer Science. Vol. 10742.: Springer, 2018. P. 387-393.
Добавлено: 23 января 2018 г.
Татарников А. Д., Камкин А. С., Сергеева Т. И. и др., , in : Proceedings of the 7th Spring/Summer Young Researchers’ Colloquium on Software Engineering, SYRCoSE 2013. : Kazan : -, 2013. P. 51-57 .
Добавлено: 20 декабря 2017 г.
Камкин А. С., Татарников А. Д., Смолов С. А. и др., , in : 2015 16th International Workshop on Microprocessor and SOC Test and Verification (MTV). : IEEE, 2015. P. 1-6.
Добавлено: 18 июля 2018 г.
Татарников А. Д., Камкин А. С., Чупилко М. М. и др., Труды Института системного программирования РАН 2014 Т. 26 № 1 С. 149-200
Обеспечение корректности микропроцессоров и другой микроэлектронной аппаратуры является фундаментальной проблемой, для решения которой применяют разнообразные средства функциональной верификации. В отличие от программ, ошибки в которых исправляются сравнительно просто, дефекты в интегральных схемах (конструктивные и производственные) не могут быть устранены. Несмотря на то, что постоянно совершенствуются системы автоматизированного проектирования (САПР), инструменты генерации тестов и методы анализа ...
Добавлено: 11 декабря 2017 г.
Камкин А. С., Татарников А. Д., Проценко А. С. и др., , in : 2017 18th International Workshop on Microprocessor and SOC Test and Verification (MTV). : IEEE, 2017. P. 10-14.
Добавлено: 18 июля 2018 г.
Камкин А. С., М. : МАКС Пресс, 2018
Книга является учебным пособием по формальным методам верификации программ и основана на курсах лекций, читаемых автором на факультете ВМК МГУ имени М.В. Ломоносова, ФУПМ МФТИ и ФКН ВШЭ. В ней изложены основы таких подходов, как дедуктивный анализ и проверка моделей. Список тем включает: методы формализации семантики языков программирования (операционная и аксиоматическая семантика), методы формальной спецификации ...
Добавлено: 2 ноября 2018 г.
Татарников А. Д., Камкин А. С., Проценко А. С., Известия высших учебных заведений. Физика 2015 Т. 58 № 11-2 С. 70-74
В работе предлагается метод автоматизированного построения тестовых программ, предназначенных для функционального тестирования подсистем памяти одноядерных микропроцессоров. Предложенный метод осно ван на использовании формальных спецификаций механизмов кэширования и трансляции адресов. Различные варианты метода успешно применялись для тестирования промышленных микропроцессоров. ...
Добавлено: 25 января 2018 г.
Камкин А. С., Чупилко М. М., Смолов С. А. и др., , in : 2018 19th International Workshop on Microprocessor and SOC Test and Verification (MTV). : Austin : IEEE Computer Society, 2018. P. 6-11.
Добавлено: 3 июля 2019 г.
Татарников А. Д., Известия высших учебных заведений. Физика 2016 Т. 59 № 8-2 С. 97-100
В работе предлагается метод автоматизированного построения поведенческих моделей микропроцессоров, используемых при генерации тестовых программ для предсказания результатов их выполнения. Предложенный метод основан на использовании формальных спецификаций системы команд. Данный метод реализован в инструменте MicroTESK, разработанном в ИСП РАН. Инструмент успешно применяется для верификации промышленных микропроцессоров. ...
Добавлено: 2 февраля 2018 г.
SciTePress, 2023
This book contains the Proceedings of the 18th International Conference on Evaluation of Novel Approaches to Software Engineering (ENASE 2023). This conference is sponsored by the Institute for Systems and Technologies of Information, Control and Communication (INSTICC), held in cooperation with the ACM Special Interest Group on Management Information Systems (ACM SIGMIS) and technically co-sponsored ...
Добавлено: 19 мая 2023 г.