RUS  ENG ЖУРНАЛЫ   ПЕРСОНАЛИИ   ОРГАНИЗАЦИИ   КОНФЕРЕНЦИИ   СЕМИНАРЫ   ВИДЕОТЕКА   ПАКЕТ AMSBIB
Общая информация
Последний выпуск
Архив
Импакт-фактор

Поиск публикаций
Поиск ссылок

RSS
Последний выпуск
Текущие выпуски
Архивные выпуски
Что такое RSS



Модел. и анализ информ. систем:
Год:
Том:
Выпуск:
Страница:
Найти






Персональный вход:
Логин:
Пароль:
Запомнить пароль
Войти
Забыли пароль?
Регистрация


Модел. и анализ информ. систем, 2019, том 26, номер 3, страницы 332–350 (Mi mais683)  

Software

Формальная верификация диаграмм троичных цифровых сигналов

Н. Ю. Куцак, В. В. Подымов

Московский государственный университет имени М.В. Ломоносова, факультет ВМК, Ленинские горы, 1, стр. 52, г. Москва, ГСП-1, 119991 Россия

Аннотация: В работе исследуется задача формальной верификации (математически строгой проверки правильности) диаграмм цифровых сигналов, используемых на практике на ранних стадиях разработки микроэлектронных цифровых устройств (цифровых схем). Отправной точкой разработки схемы, согласно современным методам проектирования, является её описание на каком-либо высокоабстрактном языке описания аппаратуры (hardware description language, HDL). Обязательным этапом разработки HDL-кода схемы является отладка этого кода, схожая по устройству и важности с отладкой программ. Один из популярных способов отладки HDL-кода основан на получении и проверке правильности диаграммы сигналов, то есть совокупности графиков сигналов: функций, описывающих изменение значений в выделенных местах схемы в реальном времени. В работе предлагаются математические средства автоматизации проверки правильности таких диаграмм, основанные на понятиях и методах верификации систем относительно формул темпоральных логик и учитывающие такие характерные особенности сигналов в HDL и соответствующих свойств правильности диаграмм в неформальном смысле, как реальное время, троичность и наличие точек фронтов. Троичность сигнала означает, что наряду с основными логическими значениями 0 и 1 сигнал может принимать и неопределённое значение: одно из значений 0 и 1, но неизвестно или неважно, какое именно. Точкой фронта называется момент изменения значения сигнала. В работе предлагаются понятия, утверждения и алгоритмы, предназначенные для формализации и решения задачи верификации диаграмм сигналов: определения сигналов и диаграмм, учитывающие упомянутые характерные особенности сигналов; темпоральная логика, предназначенная для описания свойств диаграмм сигналов, и соответствующая постановка задачи верификации диаграмм; метод решения предлагаемой задачи верификации, основанный на сведении к задачам преобразования и анализа сигналов; соответствующий алгоритм верификации диаграмм с обоснованием корректности и “приемлемой” оценкой сложности.

Ключевые слова: формальная верификация, цифровой сигнал, темпоральная логика, троичная логика.

Финансовая поддержка Номер гранта
Российский фонд фундаментальных исследований 18-01-00854_а
Исследование выполнено при финансовой поддержке РФФИ в рамках научного проекта № 18-01-00854.


DOI: https://doi.org/10.18255/1818-1015-332-350

Полный текст: PDF файл (685 kB)
Список литературы: PDF файл   HTML файл

Тип публикации: Статья
УДК: 519.71
Поступила в редакцию: 28.06.2019
Исправленный вариант: 02.09.2019
Принята в печать:04.09.2019

Образец цитирования: Н. Ю. Куцак, В. В. Подымов, “Формальная верификация диаграмм троичных цифровых сигналов”, Модел. и анализ информ. систем, 26:3 (2019), 332–350

Цитирование в формате AMSBIB
\RBibitem{KutPod19}
\by Н.~Ю.~Куцак, В.~В.~Подымов
\paper Формальная верификация диаграмм троичных цифровых сигналов
\jour Модел. и анализ информ. систем
\yr 2019
\vol 26
\issue 3
\pages 332--350
\mathnet{http://mi.mathnet.ru/mais683}
\crossref{https://doi.org/10.18255/1818-1015-332-350}


Образцы ссылок на эту страницу:
  • http://mi.mathnet.ru/mais683
  • http://mi.mathnet.ru/rus/mais/v26/i3/p332

    ОТПРАВИТЬ: VKontakte.ru FaceBook Twitter Mail.ru Livejournal Memori.ru


    Citing articles on Google Scholar: Russian citations, English citations
    Related articles on Google Scholar: Russian articles, English articles
  • Моделирование и анализ информационных систем
    Просмотров:
    Эта страница:26
    Полный текст:12
    Литература:1
     
    Обратная связь:
     Пользовательское соглашение  Регистрация  Логотипы © Математический институт им. В. А. Стеклова РАН, 2020