maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2019-3-332-350mais-1227Research ArticleSoftwareФормальная верификация диаграмм троичных цифровых сигналовFormal Verification of Three-Valued Digital Waveformshttps://orcid.org/0000-0002-0832-3635КуцакНина ЮрьевнаKutsakNina Yu.

студент бакалавриата, факультет ВМК

bachelor student, Faculty of Computational Mathematics and Cybernetics

nina_svetik@mail.ruhttps://orcid.org/0000-0002-2041-7634ПодымовВладислав ВасильевичPodymovVladislav V.

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

PhD in Mathematics, researcher, Faculty of Computational Mathematics and Cybernetics

valdus@yandex.ruМосковский государственный университет имени М.В. ЛомоносоваРоссияLomonosov Moscow State UniversityRussian Federation201928092019263332350Copyright © Куцак Н.Ю., Подымов В.В., 20192019Куцак Н.Ю., Подымов В.В.Kutsak N.Y., Podymov V.V.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/1227

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

We investigate a formal verification problem (mathematically rigorous correctness checking) for digital waveforms used in practical development of digital microelectronic devices (digital circuits) at early design stages. According to modern methodologies, a digital circuit design starts at high abstraction levels provided by hardware description languages (HDLs). One of essential steps of an HDLbased circuit design is an HDL code debug, similar to the same step of program development in means and importance. A popular way of an HDL code debug is based on extraction and analysis of a waveform, which is a collection of plots for digital signals: functional descriptions of value changes related to selected circuit places in real time. We propose mathematical means for automation of correctness checking for such waveforms based on notions and methods of formal verification against temporal logic formulae, and focus on such typical featues of HDL-related digital signals and corresponding (informal) properties, such as real time, three-valuededness, and presence of signal edges. The three-valuededness means that at any given time, besides basic logical values 0 and 1, a signal may have a special undefined value: one of the values 0 and 1, but which one of them is either not known, or not important. An edge point of a signal is a time point at which the signal changes its value. The main results are mathematical notions, propositions, and algorithms which allow to formalize and solve a formal verification problem for considered waveforms, including: definitions for signals and waveforms which the mentioned typical digital signal features; a temporal logic suitable for formalization of waveform correctness properties, and a related verification problem statement; a solution technique for the verification problem, which is based on reduction to signal transfromation and analysis; a corresponding verification algorithm together with its correctness proof and “reasonable” complexity bounds.

формальная верификацияцифровой сигналтемпоральная логикатроичная логикаformal verificationdigital signaltemporal logicthree-valued logicИсследование выполнено при финансовой поддержке РФФИ в рамках научного проекта № 18-01-00854The reported study was funded by RFBR according to the research project № 18-01-00854.ReferencesBaier C., Katoen, J. P., Principles of model checking, The MIT Press, Cambridge, USA, 2008.Baier C., Katoen, J. P., Principles of model checking, The MIT Press, Cambridge, USA, 2008.Harris S., Harris D., Digital design and computer architecture, second edition, Morgan Kaufmann Publishers Inc., San Francisco, USA, 2012.Harris S., Harris D., Digital design and computer architecture, second edition, Morgan Kaufmann Publishers Inc., San Francisco, USA, 2012.Meinel C., Theobald T., Algorithms and data structures in VLSI design: OBDD — foundations and applications, Springer-Verlag, Berlin, Germany, 1998.Meinel C., Theobald T., Algorithms and data structures in VLSI design: OBDD — foundations and applications, Springer-Verlag, Berlin, Germany, 1998.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.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.Kropf T., Introduction to formal hardware verification, Springer-Verlag, Berlin, Germany, 1999.Kropf T., Introduction to formal hardware verification, Springer-Verlag, Berlin, Germany, 1999.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.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.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.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.Basin D., Klaedtke F., Z˘alinescu E., “Algorithms for monitoring real-time properties”, Acta Informatica, 55:4 (2018), 309–338.Basin D., Klaedtke F., Z˘alinescu E., “Algorithms for monitoring real-time properties”, Acta Informatica, 55:4 (2018), 309–338.Яблонский С. В., Введение в дискретную математику, Наука, Москва, 1986; [Yablonsky S. V., Vvedenie v diskretnuju matematiku, Nauka, Moscow, Russia, 1986, (in Russian).]Яблонский С. В., Введение в дискретную математику, Наука, Москва, 1986; [Yablonsky S. V., Vvedenie v diskretnuju matematiku, Nauka, Moscow, Russia, 1986, (in Russian).]Kleene S. C., “On notation for ordinal numbers”, The Journal of Symbolic Logic, 3:4 (1938), 150–155.Kleene S. C., “On notation for ordinal numbers”, The Journal of Symbolic Logic, 3:4 (1938), 150–155.Kleene S. C., Introduction to metamathematics, North-Holland Pub. Co., Amsterdam, Netherlands, 1952.Kleene S. C., Introduction to metamathematics, North-Holland Pub. Co., Amsterdam, Netherlands, 1952.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.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.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.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.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.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.

The authors declare that there are no conflicts of interest present.