Formal VIP provide a comprehensive set of checkers and RTL that check for compliance with various 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.
Other Protocol Specifications
Cadence provides a variety of Formal VIP for other protocols.
The I2C Formal VIP supports the I2C interface protocol as defined in the UM 10204 I2C bus specification and user manual (Rev6).
The Open Core Protocol™ (OCP) defines a high-performance, bus independent interface between IP cores that reduces design time, design risk, and manufacturing costs for SOC designs. The OCP Formal VIP supports the OCP2.2 and OCP3.0 Interface Protocol Specifications. The OCP specifications can be downloaded at https://www.accellera.org/downloads/standards/ocp.
The SPI Formal VIP supports the SPI interface protocol as defined in the SPI Block Guild V03.06 Motorola, Inc. specification.