The Formal VIP for PHY protocols provide a comprehensive set of checkers and RTL that check for protocol compliance with the PHY layer for several memory and interface protocol standards. Often, the data link or network layers of an interface protocol cannot be easily modeled for formal verification, since the state space is unreasonably deep.In this case, there is significant value in validating the PHY layer with a Formal VIP. The protocol checkers of the Formal VIP consist of RTL written in SystemVerilog and checkers written in the 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.
PHY Protocol Specifications
Cadence provides a variety of Formal VIP for PHY protocols.
The DFI Formal VIP provide support for the DDR PHY Interface™ (DFI) specification, covering DFI, DFI3, and DFI5 variants.
The PIPE Formal VIP provide support for the PIPE (Phy Interface for PCI Express®) protocol specification.