A Top-Down formal Verification Approach of LIN Hardware IP based on the GapFreeVerificationTM Process

Conference: edaWorkshop 09 - Workshop 2009 - Electronic Design Automation (EDA)
05/26/2009 - 05/28/2009 at Dresden, Germany

Proceedings: edaWorkshop 09

Pages: 6Language: englishTyp: PDF

Personal VDE Members are entitled to a 10% discount on this title

Sander, Oliver; Klimm, Alexander; Hogh-Binder, Arnd; Becker, Jürgen (Universität Karlsruhe (TH) - ITIV, Germany)
Weinberger, Katharina; Bulach, Slava (Robert Bosch GmbH, Germany)

With increasing complexity of System-on-Chips (SoC) the efforts to verify whether an implementation is correct regarding a given specification is rising extremely fast. The cost of verification is one of the limiting factor for the productivity of the microelectronic industry (verification gap). Formal verification is a method of proving or disproving the correctness of the intended system behavior with respect to a given specification, using formal methods of mathematics. Therefore no signal assertions go unregarded and the verified system completely fulfills all specified criteria. One of the commonly used approaches of formal verification is model checking. However model checking of serial protocols, especially on the protocol-level (Top-Down), poses specific challenges. In this work we present an approach for a top-down formal verification based on the GapFreeVerificationTM methodology supported by OneSpin 360TM Module Verifier. The results presented within this contribution are based on experiences gathered while verifying a Local Interconnect Network (LIN) slave module.