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


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

Полный текст:


Аннотация

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


Об авторах

Нина Юрьевна Куцак
Московский государственный университет имени М.В. Ломоносова
Россия
студент бакалавриата, факультет ВМК


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


Список литературы

1. Baier C., Katoen, J. P., Principles of model checking, The MIT Press, Cambridge, USA, 2008.

2. Harris S., Harris D., Digital design and computer architecture, second edition, Morgan Kaufmann Publishers Inc., San Francisco, USA, 2012.

3. Meinel C., Theobald T., Algorithms and data structures in VLSI design: OBDD — foundations and applications, Springer-Verlag, Berlin, Germany, 1998.

4. Kern C., Greenstreet M. R., “Formal verification in hardware design: a survey”, ACM Transactions on Design Automation of Electronic Systems, 4:2 (1999), 123–193.

5. Kropf T., Introduction to formal hardware verification, Springer-Verlag, Berlin, Germany, 1999.

6. Bryant R. E., Seger C.J. H., “Formal verification of digital circuits using symbolic ternary system models”, Computer-Aided Verification, CAV 1990, Lecture Notes in Computer Science, 531, Springer-Verlag, Berlin, Germany, 1991, 33–43.

7. Baldor K., Niu J., “Monitoring dense-time, continuous-semantics, metric temporal logic”, Runtime Verification, RV 2012, Lecture Notes in Computer Science, 7687, Springer-Verlag, Berlin, Germany, 2013, 245–259.

8. Basin D., Klaedtke F., Z˘alinescu E., “Algorithms for monitoring real-time properties”, Acta Informatica, 55:4 (2018), 309–338.

9. Яблонский С. В., Введение в дискретную математику, Наука, Москва, 1986; [Yablonsky S. V., Vvedenie v diskretnuju matematiku, Nauka, Moscow, Russia, 1986, (in Russian).]

10. Kleene S. C., “On notation for ordinal numbers”, The Journal of Symbolic Logic, 3:4 (1938), 150–155.

11. Kleene S. C., Introduction to metamathematics, North-Holland Pub. Co., Amsterdam, Netherlands, 1952.

12. Bruns G., Godefroid P., “Model checking partial state spaces with 3-valued temporal logics”, Computer-Aided Verification, CAV 1999, Lecture Notes in Computer Science, 1633, Springer-Verlag, Berlin, Germany, 1991, 274–287.

13. Chechik M., Devereux B., Gurfinkel A., “Model-checking infinite state-space systems with fine-grained abstractions using SPIN”, Model Checking Software, SPIN 2001, Lecture Notes in Computer Science, 2057, Springer-Verlag, Berlin, Germany, 2001, 16–36.

14. Laroussinie F., Markey N., Schnoebelen P., “Temporal logic with forgettable past”, Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society, Washington, DC, USA, 2002, 383–392.


Дополнительные файлы

Для цитирования: Куцак Н.Ю., Подымов В.В. Формальная верификация диаграмм троичных цифровых сигналов. Моделирование и анализ информационных систем. 2019;26(3):332-350. https://doi.org/10.18255/1818-1015-2019-3-332-350

For citation: Kutsak N.Y., Podymov V.V. Formal Verification of Three-Valued Digital Waveforms. Modeling and Analysis of Information Systems. 2019;26(3):332-350. (In Russ.) https://doi.org/10.18255/1818-1015-2019-3-332-350

Просмотров: 92

Обратные ссылки

  • Обратные ссылки не определены.


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 1818-1015 (Print)
ISSN 2313-5417 (Online)