SolidPC for AMBA Interfaces

The Definitive AMBA Compliance Checkers

 

SolidPC is a tool for verifying that designs obey the ARM AMBA 2.0 AHB, APB and AMBA 3.0 AXI protocol rules. Based on formal methods for exhaustive passes, with protocol rules written and endorsed by ARM, SolidPC is the tool of choice for AMBA protocol verification. The tool is easy to use, and require no knowledge or experience of formal methods.

Product Features

  
  • Complete functional verification environment for the following AMBA protocols:
    • AHB Lite
    • AHB full (includes splits & retries)
    • APB
    • AXI
  • Rule sets developed and maintained by ARM
  • Based on formal methods - exhaustive proofs
  • No simulation vectors, test benches or properties to write
  • Easy to use
  • Quick to run
  • Checks VHDL and Verilog designs
  • Solaris, Linux and Windows support
 SolidPC rules window
 

Figure 1 ; SolidPC Main Console

Introduction

Today's complex system-on-chip designs frequently incorporate embedded processors and rely upon a bus protocol to communicate between different blocks in the system.

The ARM range of 16/32 bit microprocessors leads the embedded microprocessor market and the associated AMBA bus protocols have become the first choice of companies designing complex, state of the art system-on-chip.

One of the key verification tasks in the design of these systems is to ensure that each of the design units in the system obeys the interconnecting bus protocol. Failure to achieve this can result in poor product quality, ASIC re-spins, and delayed entry into the market with corresponding loss of revenue.

Existing protocol checking methods are typically simulation based. They require the creation of large numbers of test vectors, have difficulty in exposing corner cases, and will often take man months of effort and a large investment in EDA tools.

SolidPC Overview

Figure 2: Signal MappingTo address the issues of protocol compliance, ARM & Averant Inc. have collaborated to develop SolidPC. The tool implements a formal and exhaustive proof of correctness against a given set of properties. Each property (or rule) describes a specific aspect of the required AMBA protocol and, taken as a whole, the complete property set will fully verify a design against the required AMBA protocol.

Each protocol rule has been written by ARM, thoroughly verified by Averant and ARM, and then embedded within the SolidPC product.

The tool combines a new user interface, the AMBA protocol rule sets and Averant's formal engine to offer push-button verification of designs against the AMBA protocols.

The combination of the new GUI, the pre-written protocol rules and the power of the formal engine make SolidPC easy to use and quick to run. The property sets are used internally by ARM and are endorsed by ARM for use by their customers.

No test vectors, testbenches, coverage points or simulations are required.

Methodology Flow

SolidPC with its intuitive user interface, guides the user through the necessary steps to establish that a given design under test is compliant with the AMBA protocols. The process starts with mapping the signal names in the design to the names defined in the AMBA standard. This is a point and click process using the dialog box box above.

Next, the rules for the selected protocol are displayed and the user may select which of these are to be applied to the design under test. Many AMBA interfaces only implement a sub-set of the protocol. If a rule is deselected a contrary rule is enabled stating that the unit under test can never perform this operation.

Created with The GIMP

Verification now commences. Each protocol rule is taken in turn and submitted to the formal engine for proving against the design under test. SolidPC explores every possible legal combination of inputs the design may experience to determine if the rule holds true in all cases. If it does, the rule is passed exhaustively. For rules that pass exhaustively there are no input conditions under which the design could fail that aspect of the protocol – something very difficult to establish with simulation. The running of these rules is also fast – with properties often passing exhaustively in seconds.

 

For each rule applied to the design there are three possible outcomes:

  1. The rule passes exhaustively: The design passes for all possible legal input values.
  2. The rule fails: SolidPC will produce a VHDL or Verilog testbench that instantiates the design and creates the precise input vectors that, when applied to a simulator, will cause the design to fail that protocol rule. You can then debug the design with your chosen simulator. The stimulus is normally short, typically less than 20 cycles, so its quick to run and debug.
  3. The rule cannot be proved exhaustively, but passes for a given number of cycles after reset. SolidPC will produce a simulation monitor for further analysis of the rule within a simulation environment.

Failing rules are listed along with an explanation of exactly why they have failed, and a reference to the section in the AMBA specification where the rule is defined. At any point in the verification process a report is available showing the verification status of each rule. Proved rules are listed, along with any user given assumptions required to make them pass.

 

Summary

    

 

In order to reduce risk and meet time-to-market pressures, verification of compliance with bus protocols in a rigorous, efficient and timely manner for system-on-chip designs is essential.

SolidPC, designed for AMBA bus protocol compliance checking and verification, represents a major breakthrough in terms of the quality of the verification results achieved, ease of use, and time taken to complete the task. 

The combination of ARM developed and endorsed AMBA rule sets, the formal nature of the Solidify engine and ease of use, makes SolidPC the tool of choice for AMBA protocol verification.

 

“Formal methods offer an innovative new approach for the verification of AMBA bus protocols, as the static nature means that verification is much faster than through simulation, and corner cases are more readily exposed.

The definition of correct AMBA technology behaviour, through the development of AMBA protocol rule sets, has done much to enhance the value of AMBA technology within the industry.

By integrating our AMBA protocol rule sets into the SolidPC tool, developers will now have high-performance verification tools that can rigorously check designs against the AMBA protocol rules.”

Tim Mace
AMBA Product Manager
ARM

 

SolidPC Main Screen when verification complete

Figure 6 : SolidPC Window Upon Completion

 

Download :  

To find out how SolidPC can help you verify your Amba designs take advantage of a  FREE evaluation copy.

 

^ back to top