Zaychenko S. Models and methods for the functional verification of digital systems, based on the temporal assertions

The object of research is the process of design and verification of digital systems-on-chips using high-level hardware description languages and HDL-simulator. Thesis goal is development of models and methods for the functional verification of digital system-on-a-chip, based on the use of temporal assertions, when diagnosing errors in process of software-hardware simulation for increasing the quality of digital product and decreasing the time-to-market and cost of designing. Main results: an analytical model for verification of digital system-on-a-chip, based on the use of dynamic register queues, focused on the analysis of linear temporal logic assertions, which provides high speed simulation and specified diagnosis depth of code errors; model for interpreting linear temporal logic, using the global time and designed for verification of formulae during simulation; methods for analyzing the assertion engine, which allow considerable increasing the speed of simulation and decreasing the time of verification by 15%; interacting data model of register level and process models for processing the events and queue functions, which provide improvement of event transportation parameters during the simulation; verification and diagnosis infrastructure, characterized by the software redundancy in the form of assertions and hardware support of simulation, which makes it possible to decrease the total time of SoC designing by 30%; software components of the verification system Riviera (Aldec Inc.), where the temporal assertion based models and methods for the functional verification are implemented. This makes it possible to decrease the time of functionality and assertions simulation by 20%-80% during the testing digital designs.