Reset State Shifting in FPGA Designs to Handle Inconclusive Formal Property Verification Results

Abstract

Verifying the functional correctness of register-transfer level (RTL) designs is still challenging. Thereby, functional simulation is frequently selected as the first choice to verify system behavior. A strong alternative to simulation is represented by formal approaches. In detail, formal property verification (FPV) often provides a more efficient way to ensure the functional correctness of designs. This paper shows how inconclusive formal property results can be handled for intellectual property (IP) cores embedded into a system-on-a-chip (SoC) environment. While FPV runs are usually carried out from a default reset state, it is possible to shift the formal analysis starting point to a beneficial position. This paper investigates the approach on two IP-Cores, which allows fast property checks instead of being inconclusive after hours of formal analysis.