A case study for Formal Verification of a timing co-processor

eTPU is a state-of-the-art timing co-processor unit that aims to relief I/O processing in new advanced microcontroller units. It has characteristics of both a peripheral and a processor, which are tightly integrated, requiring a verification strategy that covers equally well both of these roles. This paper discusses the formal verification effort of some specific eTPU features. For newer versions of eTPU, some complexity increasing showed to be suitable for a formal verification approach. Formal verification was now applied to verify recently added complex features. This approach is then compared with a simulation-only approach adopted earlier.