Overview

Arm AMBA Protocols

The Cadence® Formal VIP for Arm® AMBA® protocols provide a comprehensive set of checkers and RTL that check for protocol compliance of Arm AMBA-based systems and designs. 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.

Protocols

Arm AMBA Protocol Specifications

Cadence provides a variety of Formal VIP for Arm AMBA protocols.

AHB and APB Protocols

The Cadence Formal VIP for AHB provides support for the Arm AMBA 2, AMBA 3, and AMBA 5 AHB Interface Protocol Specifications, including the AHB-Lite subset, as well as the AMBA 2, AMBA 3, and AMBA 4 APB Interface Protocol Specifications.

AXI Protocols

The Cadence Formal VIP for AXI provides support for the Arm AMBA 3 AXI, AMBA 4 AXI and ACE, and AMBA 5 AXI and ACE specifications. The Formal VIP supports the AMBA AXI protocol v1.0 and v2.0 and AMBA 5 AXI and ACE protocols as defined in the AMBA AXI protocol specifications. The ACE protocols are supported for interface-level capabilities (see ACE-SYS for system-level capabilities). A dedicated Formal VIP is also available for the AMBA 4 AXI-Stream protocol.

ACE-SYS Protocols

The Cadence Formal VIP for ACE-SYS is a comprehensive set of checkers that check for protocol compliance of Arm AMBA ACE-based systems and designs. The Formal VIP supports issue IHI0022D and IHI0022E of AMBA AXI and ACE Protocol Specification. The ACE protocols are supported for system-level capabilities, which means that the coherence protocols can be checked in a system consisting of multiple bus managers and caches.

ATB Protocols

The Cadence Formal VIP for ATB supports the Arm AMBA ATB protocol v1.0 and v1.1 as defined in the AMBA ATB protocol specification, Arm IHI 0032B.

CHI Protocols

The Cadence Formal VIP for CHI support the Arm AMBA CHI protocol as defined in the AMBA 5 CHI architecture specification, Issue A, B, and C, and the AMBA CHI architecture as defined in the AMBA CHI architecture specification, Arm IH0050B and IH0050C. The CHI protocols are supported for interconnect- and coherence-level protocols. The Formal VIP for CHI-D additionally supports the AMBA CHI protocol as defined in the AMBA 5 CHI architecture specification IHI0050D.The Formal VIP for CHI-E additionally supports the AMBA CHI-E protocol as defined in the AMBA 5 CHI architecture specification IHI0050E.