Рост сложности современных цифровых систем и увеличение объемов кода на языках описания аппаратуры требуют эффективных инструментов для выявления ошибок на ранних этапах разработки цифровых СБИС. Для своевременного обнаружения ошибок составляются сборники правил, регламентирующие описание аппаратуры. Эти сборники содержат набор правил, описывающих неточности, ошибки и последствия их нарушения. В данной работе рассмотрен список правил, разработанный на основе опыта работы инженеров, использующих язык SystemVerilog, и представлена система статического анализа SVAN, разработанная для языка SystemVerilog и учитывающая специфику описаний аппаратуры. Предлагаемая система обеспечивает полную поддержку стандарта SystemVerilog IEEE 1800-2017 и предоставляет возможности анализа описаний на наличие структурных и семантических ошибок.

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

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

В настоящее время большой популярностью пользуются языки программирования, использующие в своей инфраструктуре языковые виртуальные машины (ВМ), что стимулирует развитие данной технологии. Разработка языковой ВМ – сложный процесс, в ходе которого могут вноситься ошибки в проектируемую систему. Для обеспечения качества реализации ВМ процесс разработки включает в себя этап тестирования. При тестировании необходимо ответить на два основных вопроса: как создавать тестовые программы и как проверять результат их исполнения. В статье представлен метод функционального тестирования языковых ВМ на основе формальных спецификаций системы команд. В работе описана реализация предложенного подхода. На основе документации ВМ специфицируется системы команд с помощью языка описания архитектуры. На основе спецификации системы команд строится исполнимая модель. Для автоматизации создания тестовых программ используются тестовые шаблоны – параметризованные описания тестовых программ. При создании тестовых шаблонов используется специальный предметно-ориентированный язык, позволяющий задавать различные техники генерации и использовать байт-код ВМ, полученный из формальных спецификаций. В представленном методе тестовые шаблоны могут быть описаны вручную, сгенерированы автоматически, в соответствии с целевым критерием, или получены от сторонних генераторов. На основе тестовых шаблонов и исполнимой модели генерируются тестовые программы на байт-коде, нацеленные на проверку определенной функциональности или свойств тестируемой системы. Байт-код является естественным языком для ВМ и позволяет воздействовать на всю ее функциональность. Тестовая программа транслируется в бинарную программу и исполняется на ВМ. Во время исполнения программы на ВМ собирается трасса исполнения. Для анализа трассы исполнения создается адаптер трасс. На основе исполнимой модели и адаптера трасс строится тестовый оракул. Оракул проверяет результаты тестирования путем сравнения трассы исполнения с результатами исполнения бинарной программы на исполнимой модели. Метод реализован в инструменте MicroTESK версии 2.6 и был использован для тестирования ВМ Ark.

Развитие матричных расширений процессорных архитектур, а также внедрение этих расширений в специализированные AI-процессоры, позволяет существенно повысить эффективность выполнения искусственных нейронных сетей. В работе выполнен обзор базовых функциональных возможностей некоторых популярных матричных расширений процессорных архитектур, в частности расширений ARM SME, RISC-V IME, RISC-V AME, а также процессорной архитектуры DaVinci. В результате проведенного анализа была предложена модель абстрактного матричного процессора, отражающая особенности современных процессорных архитектур, которые поддерживают матричное расширение. Для введенной модели матричного процессора разработано гетерогенное матричное промежуточное представление, которое может быть использовано для построения компиляторов нейронных сетей. Предложенное промежуточное представление было реализовано в инфраструктуре MLIR в виде диалекта heteroMx. В работе также описан подход к построению AI-компилятора с использованием разработанного диалекта heteroMx. Разработанное промежуточное представление может быть адаптировано или конкретизировано для других матричных процессорных архитектур.

В данной работе рассматривается класс параллельных программ над общей памятью и присущий этому классу программ тип ошибок – гонки по данным. Нами спроектирован тестовый фреймворк для разработки сценариев тестирования на гонки по данным по аналогии с широко применяемыми тестовыми фреймворками для последовательных программ. Основной проблемой при создании теста является недетерминизм, присущий выполнению многопоточных программ. С целью обеспечить повторяемость сценария тестирования в данной работе мы вводим понятие точек синхронизации в исходном коде программы, в которых тест регулирует порядок исполнения инструкций программы потоками при помощи внедрения синхронизационных действий. Разработанные тесты на гонки по данным выполняются полностью автоматически при помощи фреймворка и могут использоваться для регрессионного тестирования.

В связи с необходимостью повышения производительности труда при анализе (разметке) результатов автоматизированного поиска уязвимостей в программах, проведенного с использованием инструментального средства, возникает проблема дефицита на рынке высококвалифицированных аналитиков для проведения разметки результатов. В работе описана разработанная методика для поиска уязвимостей в программном обеспечение (Далее - ПО), написанном на нескольких языках программирования (С, С++, Java, Python, Go). В ходе ее разработки проведен анализ всех автоматически обнаруживаемых детекторов в программах на этих языках и элементов их конструкций, подлежащих анализу. Детекторы упорядочены в соответствии с классификацией регулятора. Применение методики позволяет снизить квалификационные требования к аналитикам, проводящим разметку, и подготовить таких специалистов в разрабатывающих компаниях.

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

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

В нашей статье описан опыт организации второго соревнования по формальной верификации программ среди молодых специалистов и студентов российских вузов. Соревнования проводились в связке с семинаром по семантике, спецификации и верификации программ (PSSV) в Иннополисе в октябре 2024 года. Формат соревнования был близок к формату так называемых хакатонов. Участникам было предложено решить на выбор 5 задач по верификации с использованием заранее определенных инструментов проверки моделей и дедуктивной верификации (Frama-C, Coq, C-lightVer, SPIN, TLC). Мы обсуждаем вопросы организации такого мероприятия, предложенные задачи, результаты решений и обратную связь от участников.

Данная исследовательская работа посвящена использованию технологий искусственного интеллекта для проведения теста Роршаха. Рассматриваются методы машинного обучения. Оба этих метода используется для многоклассовой классификации категорий ответов. В статье описаны алгоритмы методов машинного обучения для интерпретации результатов, алгоритм выставления результатов по одной из категорий и конечного результата тестирования в веб-интерфейсе для пользователя. Применение искусственного интеллекта для проведения проективных методик тестирования, на примере теста Роршаха, открывает новые возможности для самодиагностики и терапии.

В настоящее время задача построения цифровых двойников различных природных и технических объектов является актуальной задачей. В работе рассматриваются возможности открытого ПО для разработки цифровых двойников почвенных процессов. Облачная платформа для проведения научных исследований может быть спроектирована и создана на базе аппаратно-программного комплекса, куда входят такие компоненты как сервера, система хранения данных, сетевое оборудование, стек системного программного обеспечения, виртуальные машины, микросервисы и другие элементы. Облачная платформа может быть выступать основной для проектов разработки цифровых двойников. В качестве исходных данных для построения цифрового двойника почвенных полей могут выступать метеорологические данные, данные по цифровому рельефу местности, данные по физико-химическому составу почвы, данные по сельскохозяйственным культурам, синтетические данных. В статье рассматриваются возможности открытых программных комплексов ParFlow, OpenFOAM, Paraview для моделирования почвенных процессов с использованием уравнения Ричардса для однофазной среды. Физическое моделирование проведено для случаев задания модельных почвенных полей с заданной проницаемостью и пористостью среды. В результате расчета получены поля влагонасыщенности, гидростатического напора, скорости движения влаги. В одной из модельных задач также исследовалось влияние наличия скважины на поле давления. Базовая расчетная сетка включала в себя 288 000 расчетных ячеек. Типовые расчеты проведены на вычислительном кластере ИСП РАН. Один типовой расчет запускался на 12 ядер и выполнялся по времени около 20 минут. Визуализация результатов расчета выполнена в пакете Paraview с использованием технологии фильтров и программных скриптов на языке программирования Python.

Разработана модификация метода погруженных границ LS-STAG с функциями уровня для моделирования течений неньютоновских вязких жидкостей – жидкостей, для которых вязкость в каждой точке в любой момент времени полностью определяется интенсивностью тензора скоростей деформации. Ранее была разработана модификация данного метода для другого класса неньютоновских жидкостей (вязкоупругих жидкостей), показавшая высокую точность даже для течений, которые характеризуются высокими значениями числа Вайсенберга. Поэтому представляет интерес обобщить метод LS-STAG и для неньютоновских вязких жидкостей. Отметим, что несмотря на то, что метод LS-STAG может успешно применяться для моделирования течений с подвижными погруженными границами, в данной работе внимание сфокусировано только на течениях с неподвижными границами. Построенный численный метод может использоваться как для вязкопластичных жидкостей, так и для обобщенных ньютоновских жидкостей, не обладающих пределом текучести. Для вязкопластичных жидкостей рассмотрены модели Офоли-Моргана-Штеффе, Мизрахи-Берка, Кассо и Гершеля-Балкли, используемые с моделями регуляризации Берковьера-Энгельмана и Папанастасио, а для жидкостей, не обладающих пределом текучести, модели Эллиса, Кросса, Карро, Язуды (Карро-Язуды), а также степенная модель Оствальда-де Веле. Для верификации разработанного и реализованного в авторском программном комплексе численного метода использовалась хорошо исследованная задача об обтекании неподвижного кругового профиля потоком степенной жидкости при различных значениях числа Рейнольдса и индекса течения. Полученные результаты хорошо согласуются с известными в литературе расчетными данными других исследователей. В дальнейшем планируется обобщить разработанную модификацию метода для расчета неньютоновских вязких жидкостей на случай подвижных погруженных границ.