#48DAC reports: Jasper collaborates with ARM to verify ACE multicore SoCs

The challenge of designing and verifying a heterogeneous multicore SoC (system on a chip) has been at the top of the list of "hot topics" at DAC (Design Automation Conference) for several years running now. DAC 2011 was no different, and ARM did their part to keep it that way with the announcement of a new AMBA-4 (advanced microcontroller bus architecture) specification, ACE™ - for AMBA-4 AXI™ (advanced extensible interface) Coherency Extensions.  With this new specification, designers will be able to optimize cache coherency for heterogeneous multicore SoCs, according to ARM's press release.

ARM indicated that this new specification was been driven by a group of semiconductor, EDA and verification vendors; including Arteris, Cadence, Jasper, Marvell, Mentor, Sonics, ST Ericsson, Synopsys, Texas Instruments and Xilinx. I spoke with Oz Levia, VP of Marketing and Business Development at Jasper, about their contribution to system-level verification IP (VIP) for ARM ACE-based SoCs. Jasper's "Intelligent Proof Kits" provide verification IP for protocol certification, with configurable properties that are optimized for formal analysis.Through their collaboration with ARM, Jasper developed an executable specification and methodology for the ACE protocol.

Jasper described some of the key features of ACE that you must account for in your design:

• Data Sharing and caching are supported in hardware-based cache coherency.
• Cross component communications require memory barriers.
• Independently processing engines require distributed virtual memory.

According to Oz Levia, in order to verify ACE interface correctness, designers will need "revolutionary" system VIP that provides the ability to monitor system-level behaviors, verify system coherency, and verify system ordering and messaging.

Among the verification challenges that Jasper sees with ACE are that coherency violations are hard if not impossible to detect in simulation, which can result in a time-consuming process for verification closure. Jasper also finds that it is difficult to model all the freedoms of the protocol that are available to designers through simulation, and it can be difficult to model the non-deterministic timing of some transactions - such as simultaneous requests to the same address from multiple master processors.

Jasper's solution for verification engineers is to formalize the otherwise error-prone process of capturing specification items, by using the Jasper Gold product to auto-generate verification properties and executable models. Jasper validated their VIP for ACE with ARM, to produce what the company describes as "multi-tiered" VIP for architectural exploration and connectivity verification of of AMBA-4 based SoCs. The Jasper ACE VIP provides assertions and constraints that you can use in formal verification that are optimized for formal proof convergence. Jasper has also designed the interface checks so that you can use them in simulation. The ACE VIP is available now for Jasper Gold customers. For more information on ARM ACE, you can download the specification, view a webinar, and download a whitepaper.