Close

Presentation

Formal Property Verification on Xeon SoC owned IPs
DescriptionIntel's next-generation Xeon Server/AI Accelerator SoCs integrates over 190 intellectual properties(IPs), with 26 key IPs developed in-house by the SIFG(Server IPs and Firmware Group) SoC Integration team. These IPs, which include both baseline and major derivatives, are crucial for SoC Integration validation. With limited IP-level validation on these IPs, discovering bugs during SoC integration often leads to prolonged debugging. To address this, we deployed Formal Property Verification (FPV) using Cadence's Jasper to validate end-to-end features of these Xeon's SoC-owned IPs. This paper illustrates how FPV complemented traditional simulation methods by providing exhaustive testing and faster bug detection, thereby reducing debug cycles and preventing costly post-silicon steppings across multiple Xeon product lines. Achieving several milestones on multiple Xeon products and it's IPs, we validated features on at least 17 SoC owned IPs using FPV, uncovering 84 unique bugs. These bugs included hard-to-reach scenarios not detected by traditional simulation methods and critical path issues. FPV environments along with Clock-Gating and Formal Coverage Apps, were instrumental in identifying these issues. These efforts resulted in a significant reduction of SoC Integration level bugs, enabling the Xeon Integration team to accelerate the overall pre-silicon validation timeline.