Formal Verification of Three-Valued Digital Waveforms
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 abs...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Yaroslavl State University
2019-09-01
|
| Series: | Моделирование и анализ информационных систем |
| Subjects: | |
| Online Access: | https://www.mais-journal.ru/jour/article/view/1227 |
| _version_ | 1797877919770476544 |
|---|---|
| author | Nina Yu. Kutsak Vladislav V. Podymov |
| author_facet | Nina Yu. Kutsak Vladislav V. Podymov |
| author_sort | Nina Yu. Kutsak |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-10T02:25:35Z |
| format | Article |
| id | doaj.art-02d76f42071b4b4dbf41f397e5ed5787 |
| institution | Directory Open Access Journal |
| issn | 1818-1015 2313-5417 |
| language | English |
| last_indexed | 2024-04-10T02:25:35Z |
| publishDate | 2019-09-01 |
| publisher | Yaroslavl State University |
| record_format | Article |
| series | Моделирование и анализ информационных систем |
| spelling | doaj.art-02d76f42071b4b4dbf41f397e5ed57872023-03-13T08:07:30ZengYaroslavl State UniversityМоделирование и анализ информационных систем1818-10152313-54172019-09-0126333235010.18255/1818-1015-2019-3-332-350913Formal Verification of Three-Valued Digital WaveformsNina Yu. Kutsak0Vladislav V. Podymov1Московский государственный университет имени М.В. ЛомоносоваМосковский государственный университет имени М.В. Ломоносова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.https://www.mais-journal.ru/jour/article/view/1227формальная верификацияцифровой сигналтемпоральная логикатроичная логика |
| spellingShingle | Nina Yu. Kutsak Vladislav V. Podymov Formal Verification of Three-Valued Digital Waveforms Моделирование и анализ информационных систем формальная верификация цифровой сигнал темпоральная логика троичная логика |
| title | Formal Verification of Three-Valued Digital Waveforms |
| title_full | Formal Verification of Three-Valued Digital Waveforms |
| title_fullStr | Formal Verification of Three-Valued Digital Waveforms |
| title_full_unstemmed | Formal Verification of Three-Valued Digital Waveforms |
| title_short | Formal Verification of Three-Valued Digital Waveforms |
| title_sort | formal verification of three valued digital waveforms |
| topic | формальная верификация цифровой сигнал темпоральная логика троичная логика |
| url | https://www.mais-journal.ru/jour/article/view/1227 |
| work_keys_str_mv | AT ninayukutsak formalverificationofthreevalueddigitalwaveforms AT vladislavvpodymov formalverificationofthreevalueddigitalwaveforms |