Formal Deadlock and Lifelock Detection of FPGA-based SoC Designs

Selecting proper verification methods for present Field Programmable Gate Array (FPGA) designs can significantly impact design reliability. Functional simulation, still a primary verification method, can detect most problems, at least from a theoretical point of view. However, specific problems cannot be detected because every functional simulation is finite. This paper shows the problems that come alongside deadlocks and lifelocks regarding simulation and how formal property verification (FPV) can solve these issues. For this, multiple liveness properties are applied to particular IP-Cores that are located inside a system-on-a-chip (SoC). The results are diverse, containing inconclusive and proven properties, as well as a discovered bug in a critical unit.