RUS  ENG JOURNALS   PEOPLE   ORGANISATIONS   CONFERENCES   SEMINARS   VIDEO LIBRARY   PACKAGE AMSBIB
General information
Latest issue
Archive
Impact factor

Search papers
Search references

RSS
Latest issue
Current issues
Archive issues
What is RSS



Model. Anal. Inform. Sist.:
Year:
Volume:
Issue:
Page:
Find






Personal entry:
Login:
Password:
Save password
Enter
Forgotten password?
Register


Model. Anal. Inform. Sist., 2019, Volume 26, Number 3, Pages 332–350 (Mi mais683)  

Software

Formal verification of three-valued digital waveforms

N. Yu. Kutsak, V. V. Podymov

Lomonosov Moscow State University, Faculty of Computational Mathematics and Cybernetics, 1-52, Leninskiye Gory, Moscow, GSP-1, 119991 Russia

Abstract: 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 HDL-based 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.

Keywords: formal verification, digital signal, temporal logic, three-valued logic.

Funding Agency Grant Number
Russian Foundation for Basic Research 18-01-00854_а
The reported study was funded by RFBR according to the research project № 18-01-00854.


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

Full text: PDF file (685 kB)
References: PDF file   HTML file

UDC: 519.71
Received: 28.06.2019
Revised: 02.09.2019
Accepted:04.09.2019

Citation: N. Yu. Kutsak, V. V. Podymov, “Formal verification of three-valued digital waveforms”, Model. Anal. Inform. Sist., 26:3 (2019), 332–350

Citation in format AMSBIB
\Bibitem{KutPod19}
\by N.~Yu.~Kutsak, V.~V.~Podymov
\paper Formal verification of three-valued digital waveforms
\jour Model. Anal. Inform. Sist.
\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}


Linking options:
  • http://mi.mathnet.ru/eng/mais683
  • http://mi.mathnet.ru/eng/mais/v26/i3/p332

    SHARE: 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
  • Моделирование и анализ информационных систем
    Number of views:
    This page:27
    Full text:12
    References:1

     
    Contact us:
     Terms of Use  Registration  Logotypes © Steklov Mathematical Institute RAS, 2020