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

Abstract:
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.