The Formal VIP for memory protocols provide a comprehensive set of checkers and RTL that check for protocol compliance with various JEDEC memory protocol standards. The protocol checkers consist of RTL written in SystemVerilog and checkers written in SystemVerilog Assertion (SVA) property language. The Formal VIP also have a comprehensive set of covers for measuring functional coverage of verification. These Formal VIP can be used in both Jasper™ formal verification and simulation environments. In the Jasper formal environment, they generate stimulus using SVA constraints and verify protocol behavior using SVA property language, and in simulation, they are used as checkers.
Memory Protocol Specifications
Cadence provides a variety of Formal VIP for memory protocols.
The DDR Formal VIP provide support for versions of the JEDEC DDR SDRAM standard (JESD79), covering DDR, DDR2, DDR3, and DDR5 variants.
The LPDDR Formal VIP provide support for versions of the JEDEC LPDDR SDRAM standard (JESD209), covering LPDDR, LPDDR2, LPDDR3, and LPDDR5 variants.
The SDRAM Formal VIP provides support for the JEDEC SDR SDRAM STANDARD (JEDEC No.21-C) protocol specification.