Close

Presentation

Weeding Out Timing Gaps and Improving Performance of DDR Controllers Using Formal Verification
DescriptionLPDDR6 delivers substantial gains in bandwidth, power efficiency, and scalability through phase‑aware command scheduling, multi‑sub‑channel architectures, and data rates reaching 12.8 GT/s. These architectural innovations significantly complicate the verification of minimum timing constraints and performance‑critical behaviours in memory controllers, where simulation‑based approaches fail to expose phase‑dependent corner cases and sub‑optimal scheduling interactions.
This paper presents a scalable Formal Property Verification (FPV) framework to exhaustively validate LPDDR6 timing correctness and systematically analyze controller‑level performance limitations. The approach employs a generic timing reference model augmented with frequency‑mode‑aware phase counters, constrained timing registers, and state‑driven SystemVerilog Assertions (SVA) to precisely track command scheduling across 1:2:4 and 1:4:8 clocking modes. The formal methodology detects minimum‑timing constraint violations and LPDDR6 performance degradation, ensuring strict minimum‑timing compliance while improving memory‑controller scheduling efficiency.
Applied across all 16 LPDDR6 supported data rates, the framework uncovered multiple timing and performance defects, improved scheduling robustness, and enabled early detection of corner‑case issues. These results demonstrate that FPV is an effective and scalable solution for ensuring LPDDR6 timing compliance while maximizing memory‑controller performance.