VIP for ARM AMBA Protocols



The Jasper Verification IP (VIP) for AMBA® supports the following:
  • AMBA 4 Coherency Extensions (ACE)
  • AXI-4 (including AXI-Lite and AXI-Stream versions)
  • AXI-3
  • AHB (including AHB-Lite version)
  • APB

The Jasper AMBA VIP can be used in a variety of verification methodologies including simulation and formal verification using Jasper solutions.  Jasper AMBA VIP solutions address complex system-level SoC issues such as cache coherency, absence of deadlocks, data consistency, etc. The collaboration between Jasper and ARM to rigorously verify the AXI4 protocol resulted in the Jasper ACE certified VIP with unparalleled performance for formal verification.

 
 
FEATURES
 
Assertions and constraints provided for use with Jasper formal solutions
VIP optimized for formal proof convergence using JasperGold®
Interface checks also designed to be used in simulation
 
BENEFITS
 
Exhaustive verification of AMBA-based SoCs
Reduction to design and verification risk
Easier protocol comprehension
High confidence in validity of VIP
 
 
Jasper AMBA 4/ACE VIP Components

Figure:1 Jasper AMBA 4/ACE VIP Components
 
Challenges of Protocol Verification:

Protocol verification entails several challenges.  Capturing the intent of the specification by transferring intent from the specification into a machine-readable format that can be processed can produce errors.  When proving all possible scenarios, using only simulation is impractical because the state space is too large and it is difficult for dynamic verification systems to generate comprehensive stimuli.  Using simulation can also result in long debug times.  During debug, a presentation of conflicts or errors in functional terms that are abstracted from the waveform and relate to the specification is required

 

Jasper AMBA VIP Solutions:

Users can leverage the Jasper ACE and AXI4 VIP to:

  • Model and verify the protocol to demonstrate that it adheres to high-level, cache coherence rules
  • Ensure correctness and completeness of protocol properties
  • Visualize and query executable spec of the protocol
  • Enable easier protocol comprehension for RTL designers and verification engineers

 

 
Visualize and Query the AMBA 4/ACE interconnect
 
Figure:2 Visualize and Query the AMBA 4/ACE interconnect

 

 
Collaboration with ARM:

Jasper worked extensively with ARM to validate the ACE protocol specification resulting in VIP that was rigorously tested and that can be used by ARM licensees in the verification of their own SoCs.  The ACE protocol met with several implications for verification.  Evolutionary interface VIP was needed to account for changes to the specification (i.e. AXI4 updated from AMBA-3, new ACE channels, and verification of interface correctness).  A Revolutionary system-level VIP was needed to monitor system-level behaviors, verify system coherency, and verify system ordering and messaging.