Research And Implementation Of Model Checking Method Based On Semi-tensor Product

Integrated circuit industry has developed over 50 years. The new industry represented by Mobile Internet, Triple Play and the Internet of Things have become the new impetus to the IC industry. The functional validation of chip is always the main bottleneck of IC industry. The traditional way of functional verification is simulation, which is difficult to meet demand for functional validation. Formal verification with its rigorous and high test coverage has been getting more and more attention, which uses mathematical reasoning to show validity of a circuit or system.Semi-tensor product of matrices theory is a new mathematical theory. A major feature of semi-tensor product is to extend the conventional matrix product, which extends the conventional matrix product to any two matrices. By this theory, logic operations convert into the matrix multiplication, and can be used to describe the states transition in a logic system.In this thesis, the theory of design verification of integrated circuits and semi-tensor product is introduced firstly, and then shows the special utility of semi-tensor product in the study of logic system. After studying and researching some application case studies which involve semi-tensor product, there is always a problem of computational complexity, which means matrix computation often encounter with big scale and complex calculation process. In order to make this mathematical tool more effectively, this paper presents some simple and practical improvement methods with corresponding proof and demonstration, including the calculation of structure matrix in Boolean network, structure matrix power calculation and structure matrix reverse deduction.In model checking, the description of the system actually reflects the states transition, by this circumstance, semi-tensor product theory may be applied here.Then modeling method is proposed based on the semi tensor product refers to the general circuit model. The analysis of model structure is given according to the Boolean network. We point out the function of control variables which selecting the matrix blocks and the thought of divide the model into sub system. The specification based on semi-tensor product is proposed, and then the testing method is given which use the idea of the decomposition, and a case study is used to describe it.