FMCAD 2009
Formal Methods in Computer Aided Design
Austin, Texas, USA
November 15 - 18

Sunday Industrial Experience Report, 15. November, 17:00 - 18:00

Complete Functional Verification

Jörg Bormann, OneSpin Solutions

Abstract

Complete Functional Verification is a practical approach to verify the entire functionality of a circuit. It has been successfully applied in many industrial hardware design projects. This overview presents the technical components of the approach, sketches its scientific foundations and elaborates on the related methodology and its integration into industrial hardware design and verification processes. The approach is based on properties verifying circuit operations like, e.g., a read request of a bus bridge or the instruction execution of a processor pipeline. Such properties are well-suited for SAT based proofs, and for so called "Completeness Checking". The latter proves that a set of properties verifies all circuit functionality. An adaptation of Assume-Guarantee-Reasoning is used to decide when the complete verification of sub-circuits is also a complete verification of the compound circuit. Application examples will illustrate the approach and present circuit sizes and verification efforts.

Bio

Jörg Bormann received a masters degree in Mathematics in 1990. He worked in the formal hardware verification groups of Siemens and Infineon. Since 2005 he has been with OneSpin Solutions GmbH, Munich, where he is now the Director of Advanced Applications and Technology. Jörg has been working on SAT, BDD and theorem prover based formal verification of hardware, both in functional and equivalence verification. He developed Complete Functional Verification including Completeness Checking. For this research Jörg received a PhD in Electrical Engineering from the University of Kaiserslautern, Germany, in 2009. Jörg developed OneSpin's GapFree Verification Process, and defined OneSpin’s flagship product 360 MV. Using Complete Functional Verification Jörg conducted several business critical first time right verification projects, e.g., on processors, processor based SOCs and telecom SOCs.