Formal Description And Verification Of SoC Based On Projection Temporal Logic

With the rapid development of VLSI and EDA over the last few years, SoC has become the development tendency of Embedded Systems. SoC has brought about some technical problems, which puts up higher requirement for the correctness of design. How to reduce the errors and increase the reliability in system designs becomes the main problem to be solved. The traditional methods lack accuracy, and the validation cannot promise an overall overlay, which may easily result in errors. In order to solve the problems, formal methods have been applied to the design of hardware and software. Formal methods are mathematic ways to deduce and verify systems based on the specification of system designs.PTL(projection temporal logic) is a kind of temporal logic interpreted over discrete state sequences (intervals). It can deal with the complex sequential and parallel computations. It offers powerful and extensible capabilities and proof techniques to reason about properties such as safety and liveness. Extended Tempura is an executable subset of PTL, which can be used to develop the system prototype and to simulate the system.This thesis briefly introduces the main content and application of formal methods, coupled with the main content of PTL and its executed subset. Also the thesis discusses different descriptions of SoC using PTL. In addition, how to convert statecharts to PTL is explored. Thus, a PTL-based SoC design validation method is proposed. With this method, the formal description and verification of system designs in the high level can be done. This increases the reliability of system designs through different stages in the process of designs.