Formal VIP for PHY Protocols

Overview

PHY Protocols

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.