SP3: Correct Industrial Hardware/Software-System — Reliable Chips by Mathematical Proofs

In the research project Verisoft, funded by the German Federal Ministry of Education and Research, the completion of the correctness proof for a large-scale industrial processor, previously considered infeasible, is now just around the corner.

Circuit designs are normally checked before fabrication through extensive simulations in order to prevent logical design errors—the bulk of all design errors—on time. As this approach has reached its limits because of today's design complexity of millions of transistors, industrial and academic researchers are working on formal verification methods. These methods do not simulate individual runs of the design but establish the correspondence between a circuit's logic and its specification in the mathematical sense.

Infineon places its know-how in processor design at Verisoft's disposal, as it does with its formal verification technique CVE (Circuit Verification Environment), which was awarded the German EDA-Achievement-Award in 2003.

With the collaboration of Infineon's academic partners in Verisoft—the Saarland University as well as the Technical University of Munich—this method is extended with newly developed computerised proof techniques for the early stages of design.

It was first proved in January 2005 on the basis of the Infineon processor Tricore 2, the future 'flagship' of 32-bit microcontroller family from Infineon, that this innovative technique is applicable on highly complex designs, and these will stay manageable in the future.

Formal methods, because of the certainty of their assertations, are predestined to be the vital new components, complementing established methods such as simulation, for the successful breakthrough in the creation of more stable, in fact, errorfree designs and the simultaneous significant reduction of the iterative verification process.

For the proof the TriCore 2 processor core with its pipeline of up to six stages and almost its complete rich instruction set were fully formally specified. Around 70% of the complete functionality of the TriCore 2 core have already been verified five months before the end of the first phase of Verisoft (June 2005).

Even though this work is not yet completed, the improvements achieved so far have been directly incorporated in the design. This will enable Infineon to offer the TriCore 2, which is, e.g., targeted at high end vehicle electronics, with unprecedented quality.

The intended further development of the method should simplify its application even more, so that it becomes accessible to a wider group of circuit developers and verification engineers. That will result in the extension of the enterprise's extreme quality standards with regards to the production to the level of design.

Revision 14 Dec 2006