Complete Formal Verification of TriCore2 and Other Processors

This paper describes an innovative and powerful methodology for the complete formal verification of modules and intellectual property (IP), and its application to the verification of processor IP. Unlike other formal approaches, the methodology is a self-contained approach to hardware verification, independent of simulation. The methodology eliminates all gaps in the verification plan and in the property set. It thus ensures that the IP is free of functional errors − the highest possible verification quality. Its underlying technology has been field-proven on hundreds of modules and IP, two of which are described, including the TriCore2 processor, Infineon's next generation high-end processor for embedded and safety-critical applications.