Средства функциональной верификации микропроцессоров

А. Д. Татарников; А. С. Камкин; Чупилко М. М.; Коцыняк А. М.; Смолов С. А.; Сортов А. А.

doi:10.15514/ISPRAS-2014-26(1)-5

Публикации

?

Средства функциональной верификации микропроцессоров

Труды Института системного программирования РАН. 2014. Т. 26. № 1. С. 149–200.

Татарников А. Д., Камкин А. С., Чупилко М. М., Коцыняк А. М., Смолов С. А., Сортов А. А.

Обеспечение корректности микропроцессоров и другой микроэлектронной аппаратуры является фундаментальной проблемой, для решения которой применяют разнообразные средства функциональной верификации. В отличие от программ, ошибки в которых исправляются сравнительно просто, дефекты в интегральных схемах (конструктивные и производственные) не могут быть устранены. Несмотря на то, что постоянно совершенствуются системы автоматизированного проектирования (САПР), инструменты генерации тестов и методы анализа схем, верификация остается самым узким местом процесса разработки (на нее тратится около 70% всех ресурсов проектирования). В работе делается краткий обзор средств верификации микропроцессоров, рассматриваются проблемы, возникающие в промышленной практике, анализируются возможные пути их решения. Значительная часть статьи посвящена исследованиям по верификации аппаратуры, проводимым в ИСП РАН: подводятся итоги выполненных работ, описываются текущие разработки, формулируются направления дальнейших исследований.

Научное направление: Компьютерные науки

Приоритетные направления: компьютерно-математическое

Язык: русский

DOI

Ключевые слова: моделирование modeling верификация тестирование testing validation валидация цифровая аппаратура генерация тестов Microprocessor hardware микропроцессоры parallelization распараллеливание Test generation functional verification architecture description languages языки описания архитектуры

Рефакторинг исходного кода на основе LLM и расширения UML

Караваева Е. А., Кулигин Л. А., Резуник Л. и др., Труды Института системного программирования РАН 2026 Т. 38 № 3 С. 67–94

В статье представлен метод рефакторинга исходного кода на основе интеграции большой языковой модели (LLM) и расширенной UML-модели программного кода. Предложенный подход позволяет выявлять проблемные участки кода с использованием функций тревожности и структурных метрик классов, а затем выполнять автоматизированный рефакторинг. Ключевой особенностью метода является использование LLM для генерации формальных спецификаций на языке OCL (Object Constraint Language), ...

Добавлено: 24 мая 2026 г.

Coping with AI errors with provable guarantees

Tyukin I., Тюкина Т. А., van Helden D. P. и др., Information Sciences 2024 Vol. 678 Article 120856

Добавлено: 23 мая 2026 г.

Overcoming the Curse of Dimensionality with Synolitic AI

Zaikin A., Sviridov I., Sosedka A. и др., Technologies 2026 Vol. 14 No. 2 Article 84

Добавлено: 23 мая 2026 г.

Stable On-the-Fly Learning for Dynamic Neural Networks With Delayed Inputs

Kibkalo Vladislav, Chertopolokhov V., Mukhamedov A. и др., IEEE Access 2026 Vol. 14 P. 14369–14392

Добавлено: 22 мая 2026 г.

Опыт применения сетевого анализа (SNA) в историческом нарративе полисубъектного региона (на примере валлийской хроники Brut y Tywysogyon)

Лошкарева М. Е., Матвеева Н. Н., Вестник Томского государственного университета. История 2026 № 100 С. 112–118

Предпринята попытка применения сетевого анализа в изучении средневекового нарративного источ ника. Цель исследования – проверка гипотезы о политической фрагментарности как основной причины завоевания Уэльса Англией. Построены сети взаимодействий исторических лиц на основе данных валлийской Хроники принцев с 1193 по 1282 г. Построение сетей демонстрирует, что завоевано Англией было формально объеди ненное княжество, ослабляемое не столько ...

Добавлено: 22 мая 2026 г.

ML-based Fast Simulation of FARICH Responses

Шипилов Ф. А., Barnyakov A., Ivanov A. и др., / Series Physics "arxiv.org". 2026.

Добавлено: 19 мая 2026 г.

Proceedings of the 19th Conference of the European Chapter of the Association for Computational Linguistics (Volume 3: System Demonstrations)

Rabat: Association for Computational Linguistics, 2026.

Добавлено: 19 мая 2026 г.

Dataset of solubility values for organic compounds in binary mixtures of solvents at various temperatures

Беззубов С. И., Malikov D., Krasnov L. и др., Scientific data 2026 Vol. 13 Article 727

Добавлено: 19 мая 2026 г.

Aerokinesis: An IoT-Based Vision-Driven Gesture Control System for Quadcopter Navigation Using Deep Learning and ROS2

Pikalov V., Meshcheryakov V., Kondratev S. и др., Technologies 2026 Vol. 14 No. 1 P. 1–27

This paper presents Aerokinesis, an IoT-based software–hardware system for intuitive gesture-driven control of quadcopter unmanned aerial vehicles (UAVs), developed within the Robot Operating System 2 (ROS2) framework. The proposed system addresses the challenge of providing an accessible human–drone interaction interface for operators in scenarios where traditional remote controllers are impractical or unavailable. The architecture comprises ...

Добавлено: 19 мая 2026 г.

Aerokinesis: An IoT-Based Vision-Driven Gesture Control System for Quadcopter Navigation Using Deep Learning and ROS2

Kondratev S., Yulia Dyrchenkova, Georgiy Nikitin и др., Technologies 2026 Vol. 14 No. 1 Article 69

Добавлено: 19 мая 2026 г.

Parallel Computational Technologies. PCT 2025

Springer, 2025.

Добавлено: 18 мая 2026 г.

KMHCR: A Key-Controlled Signal-Domain Transformation for 5G IoT Security

Ronglin Z., Wei L., Jiahong C. и др., Journal of Signal Processing Systems 2026 Vol. 98 P. 1–15

Добавлено: 16 мая 2026 г.

DPN Verifier: A Toolkit for Faster Soundness Verification and Repair of Process Models with Data

Суворов Н. М., Proceedings of the Institute for System Programming of the RAS 2026 Vol. 38 No. 3(2) P. 49–66

Сети Петри с данными (DPN) являются расширением классических сетей Петри, позволяющим моделировать процессы, где данные влияют на поток управления, обеспечивая комплексное представление о поведении системы и возможность обнаружения точек отказа, которые в противном случае были бы скрыты. Одним из критериев корректности для моделей процессов является бездефектность. Модель процесса называется бездефектной, если она всегда корректно завершается ...

Добавлено: 16 мая 2026 г.

QGKM: A Quantum Fidelity-Based Graph Clustering Framework for Robust Data Pattern Recognition in Education Social Networks

Xiong N., Long W., He D. и др., Algorithms 2026 Vol. 19 No. 5 Article 386

Добавлено: 13 мая 2026 г.

Proceedings of the 9th Student Research Workshop associated with the International Conference Recent Advances in Natural Language Processing

Velichkov B., Nikolova-Koleva I., Slavcheva M., Shumen: INCOMA Ltd, 2025.

Добавлено: 12 мая 2026 г.

Parallel Computational Technologies, 19th International Conference, PCT 2025, Moscow, Russia, April 8–10, 2025, Revised Selected Papers. (CCIS, volume 2891)

Springer, 2026.

Добавлено: 12 мая 2026 г.

Интегрированная среда моделирования для верификации и валидации программ управления подключенными и высокоавтоматизированными транспортными средствами

Степанянц В. Г., Долгов И. М., Хорошилов Г. С. и др., Труды Института системного программирования РАН 2026 Т. 38 № 3 С. 95–110

На рынок постепенно выходят высокоавтоматизированные и подключенные транспортные средства (ТС). В настоящее время предлагаются решения, позволяющие использовать эти технологии для совместного управления дорожным движением, что может значительно повысить его безопасность. В статье анализируются требования к интегрированной среде моделирования подключенных и высокоавтоматизированных ТС и совместной автоматизации управления дорожным движением с высокодетализированным учетом влияния окружающих объектов. Проанализированы ...

Добавлено: 12 мая 2026 г.

Connected and Automated Vehicle Scenario Manager Graphical User Interface

Тихонов Р. А., Efendiev M. T., Fedotenkov A. A., 2026 International Russian Smart Industry Conference (SmartIndustryCon) 2026 P. 542–547

Добавлено: 11 мая 2026 г.

Proceedings 2026 IEEE 11th International Conference on Smart Cloud SmartCloud 2026 8-10 May 2026

Los Alamitos: IEEE Computer Society, 2026.

Добавлено: 10 мая 2026 г.

Digital twin framework for liquidity management: Bridging the gap between theory and operations

Zanko G., Назарова В. В., MULTIDISCIPLINARY SCIENCE JOURNAL 2026 Vol. 8 No. 10 P. e2026780

Добавлено: 10 мая 2026 г.

От неизвестности к прозрачности: обзор технологий объяснимого ИИ (XAI)

Авдошин С. М., Песоцкая Е. Ю., Информационные технологии 2026 Т. 32 № 4 С. 185–194

С развитием ИИ, и в особенности глубокого обучения, появились модели, способные давать крайне точные прогнозы. Однако их внутренняя логика остается трудной для понимания — и это серьезная проблема, особенно в сферах, где от корректности алгоритма зависят критиче ски важные решения. Одним из перспективных путей ее решения считается направление Explainable Artificial Intelligence (XAI) — разработка подходов, позволяющих прояснять ...

Добавлено: 8 мая 2026 г.

Explainable AI for Industry 5.0: Shedding light on the black box

Авдошин С. М., Песоцкая Е. Ю., Business Informatics 2026 Vol. 20 No. 1 P. 7–28

Добавлено: 8 мая 2026 г.

Natural hazard database from Internet publications: text mining with a large language model

Деркачева А. А., Сакиркина М. А., Краев Г. Н. и др., /. 2026.

Добавлено: 28 апреля 2026 г.

Algorithmic overlaps as thermodynamic variables: from local to cluster Monte Carlo dynamics in critical phenomena

Пиле Я. Э., Deng Y., Щур Л. Н., / Series arXiv "math". 2026. No. 2604.10254.

Добавлено: 20 апреля 2026 г.