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.
Reset State Shifting in FPGA Designs to Handle Inconclusive Formal Property Verification Results
02.03.2024
1057725 byte
Aufsatz (Konferenz)
Elektronische Ressource
Englisch