Ivanov

Improving the verification of hardware and software systems is associated with the usage of formal methods among which the authors consider the model checking method which provides an automated consideration of all possible "paths of functioning" of the system. The problem of “explosion of the number of states” inherent in the method of verification of model checking is analyzed in the article; various methods of dealing with this problem are discussed. Particular attention is paid to verification of coherence memory protocols; possible approaches to solving this problem are outlined.

 This paper considers the causes of metastability during the interaction of devices controlled with asynchronous clock signals. The article suggests different ways of eliminating metastability and proposes using a FIFO buffer with asynchronous FIFO pointer comparison.