Study. Based On Gste Theory Of Counter-examples

In the past several decades, with the great demand for information technology, and the high-speed development of microelectronics, the size and complexity of integrated circuits are increasingly high. So the integrated circuits design and manufacture need higher quality than past. It is very difficult without an error in the millions of transistor-level circuits, such as the float error in the 1994, so verification is very important. Symbolic trajectory evaluation (STE) is a model checking technique based on a four value symbolic simulation. It has shown great promise in the design of large scale hardware. Although the STE verification is very efficient, the disadvantage of the STE is the limited attribute types of verification and helpless for the unlimited time attribute. In addition, the STE only can simulate forward, but not backward. So it does't need find the adverse example. In the recent years, GSTE (Generalized symbolic trajectory evaluation) has improved on STE, not only can verify the unlimited time attribute, but also can simulate backward. Because of the feature of GSTE supporting backward simulation, we may research counter-examples generated of GSTEBecause GSTE is generally carried out the verification related to the nature, once the nature fail, we need to generate a counter-example provided to the designer to debug the error, and thus to determine the reason for the failure. Through debugging the counter-examples, the designer can determine this error is caused by an invalid input, or due to design error. In the former case, it needs to add constraints to eliminate the invalidity; the latter will need to redesign the system. As the relatively new theory of GSTE, there is no scholar to research the GSTE counter-example systematically. Therefore, this topic about the study of counter-example technology is crucial for the improvement of the GSTE theory.In this paper, we studied the verification, including development of verification, STE theory, and GSTE theory, development of counter-example and activity of counter-examples. Then, we designed two algorithms to find counter-examples through the analysis of the GSTE theory. Then, this paper implemented the algorithm by programming, designed and implemented the module of compile, the module of GSTE authentication and the module of finding counter-examples. In the process of programming implementation, we introduce the Hash function and BDD (Binary Decision Diagram). The programming greatly improved the efficiency of the system through the use of Hash function and BDD; Finally, We analyzed the efficiency and feasibility of the system through an example.