Concurrent Generalized Symbolic Trajectory Assignment

As digital logic designs grow larger and more complex, functional verification has become the number one bottleneck in the design process. In the past few decades, people have studied in-depth and extensively on verification of sequential behaviors of digital circuits and proposed several effective verification methods, mainly include simulation based and formal method based verification technology. However, digital circuits are typical concurrent system. How to perform the verification of concurrent behaviors is a critical factor to insure the functional correctness of digital circuits.Based on understanding of lots of previous work on formal verification, we study deeply the GSTE method which is one of the currently most important formal verification methods ,and extend it to make it can succinctly describe the concurrent properties of digital circuits in verification.On study methods, Firstly, we studied the theory about GSTE, including circuit model, circuit simulation methods, symbolic trajectory evaluation and the kernel algorithms of GSTE. Besides that, we show the shortage of GSTE when it describe the concurrent behavior by example in the three chapter.Secondly, after studying the Process Algebra, we proposed a compositional approach based on GSTE to overcome the limitation that the GSTE can't succinctly describe the concurrent properties of system. (1) We proposed a specification language that allows the concurrent behavior of a system to be specified succinctly in a compositional manner. Such a composition is logical and does not rely on a deep understanding of the implementation details of the system. The language is an extension of the GSTE specification language with a new operator"meet"and is expressed in the form of Process Algebra. (2) Against the new compositional assertion graph specification, we modified the algorithm of GSTE. The modified algorithm has the ability to walk through the syntactical structure of the specification and establish a simulation relation from the language elements of the specification to the sets of states in the circuit. Thirdly, we studied how to implement the modified algorithm using FL in Forte platform and done the experiment to test it. The experiment results show that the new approach is effective and it can reduce the complexity of the assertion graph.Finally, a comprehensive summary is given about this thesis, and point out the direction of further research and improvement, and the promising application prospect of formal verification.