Formal Verification of Three-Valued Digital Waveforms
Nina Yu. Kutsak, V. V. Podymov · Automatic Control and Computer Sciences · 2020
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 the 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 method for an HDL code debug is based on extraction and analysis of a waveform that is a collection of plots for digital signals: functional descriptions of value changes related to the selected circuit places in real time. We propose mathematical means for automation of correctness checking for such waveforms based on concepts and methods of formal verification against temporal logic formulas and focus on such typical features of HDL-related digital signals and corresponding (informal) properties such as real time, three-valuedness, and presence of signal edges. The three-valuedness 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 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 intended to formalize and solve the formal verification problem for considered waveforms including (i) the definitions for signals and waveforms that capture the mentioned typical digital signal features, (ii) the temporal logic suitable for formalization of waveform correctness properties and a related verification problem statement, (iii) a solution technique for the verification problem that is based on reduction to signal transformation and analysis, and (iv) a corresponding verification algorithm together with its correctness proof and “reasonable” complexity bounds.