Formal Verification Study In SOC Design

Formal verification in SOC design is studied and designed in this dissertation,which comes from the project of a Baseband SOC chip of mobile phone in Infineon company as a internship. The author has a deeply research on the application of Formal Verification in a SOC design and formal verification flow and detail implementation method research in SOC based on formal verification tool ONESPIN which is developed by Infineon. Through this research, the author proposed a good way to predigest the verification flow. It is proved that the strategies proposed in this paper are effective, intuitionistic and reliable. The research work of this dissertation mainly includes:This thesis shows some examples to describe the idiographic methods on the consistency check and equivalence check and explains how the designs are represented within the Onespin tools, and how the commands in the setup mode are used to create this representation. The thesis introduces the module verification which also is named property checking. It expatiates on the exactly process of module verification. And the author combined a small design module to show how to write your own properties and how to debug the fault. It also narrates some about property language ITL(internal language).As PCL(port control ligic)for an example to do a further research on how to create property and how to predigest the property checking flow. It gives a available predigestion method of property check flow aiming at the problem of how to improve the efficiency of verification. At last, it shows a detail useful information of the GUI interface.The results studied in this dissertation are successfully applied for the verification of SOC. And the flow predigestion strategies proposed in this paper are used for the real project successfully in Infineon. It is indicated that the method can predigest the property checking flow efficaciously. And it exactly satisfies the specification.