Verifying register implementations against an IP-XACT register map

Almost every block in an electronic design contains a series of registers. These registers are used to configure, control and monitor the operation of the block, often loaded or read from a system processor utilizing a related driver software function. A very common source of errors in a system is a mismatch between some aspect of the register hardware implementation and its specification. As some blocks may contain hundreds of registers, with a nested implementation to handle addressing, issues are hard to find using simulation, requiring long run time, while still not being exhaustive.

OneSpin’s Register Checking App automatically generates formal assertions from a given register map specification in IP-XACT, and provides an exhaustive verification of all operational aspects, while cutting down on run-time.

Register Map Validation Problem

The register addresses are defined by a memory or register map, a common document used throughout hardware, software, system/IP integration and verification engineering to ensure consistency. This map might form part of a specification in the case of the IP block coming from a third party. Carefully reading a modern memory map specification to ensure system consistency takes many hours, and is extremely error prone given the typically large number of registers.

Today, register operation is often checked using simulation. In simulation, a series of read and write interactions would require testing for each register, as well as ensuring that registers behave independently of each other, clearly requiring a potentially large stimulus file. Therefore, simulation is inadequate for this purpose as it is entirely dependent on the quality of stimulus, which leads to missed issues.

Formal Register Checking

Although missing a register implementation mismatch would seem to be a relatively trivial issue, it can cause many wasted hours spent in debug, particularly because the problem might not manifest itself until the block software driver is operating with application software, at which point multiple engineering functions are involved with disassociated knowledge of the system.

As a consequence, an exhaustive analysis of register behavior is desirable where all register interaction, operation and consistency is tested completely. An exhaustive check may only be reliably accomplished with a formal solution, which eliminates the need to create a stimulus file all together.

Formal Register Checks with OneSpin

The OneSpin Register Checking App reads in an RTL description of a block to be tested, together with an IP-XACT file, or some other format, that specifies the block’s registers. It then performs an exhaustive comparison to ensure absolute consistency, by generating automatically a set of assertions and applying those assertions to a formal verification engine. The system is set up to allow other specification formats to be also utilized easily. 

Any mismatches or other errors are documented in a comprehensive log file and a simulation trace debug example is generated and made available in the included debug environment, allowing issues to be easily identified and repaired.

The Register Verification solution is completely automated, requiring only an IP-XACT or other specification and some simple setup commands to activate. It has been proven on design projects to save a considerable amount of time and downstream engineering frustration. 

Typical Use Models

Today, a register specification is often provided for a system using a standard such as the IEEE-1685 IP-XACT format, an XML meta-data representation designed to ease the integration of IP. This standard is machine-readable and provides an easier way to check for register consistency, providing an ideal input into the formal verification process using the OneSpin Register Checks App.

Some register tools use the IP-XACT format to generate register hardware. In these cases, it has been proven to still be important to verify generated implementations for various situations, including: validating a change to the register map or underlying design, incorrect signal connection, issues with block address bus sizes, extra validation of hierarchical address mapping schemes, and even some RAM tests.

One specific engineering group using the solution reported a dramatic time saving when using 360 DV-Verify versus a simulation-based solution, with the confidence of an exhaustive test dramatically increased. Three instances of bad connections were discovered on this particular occasion.

The app is prepackaged and included in the OneSpin 360 DV-Verify™ product.

Further Reading:

• Success Story: Alcatel-Lucent's Joachim Knaeblein and Hans Sahm used both automated assertion generation and automated formal methods of OneSpin 360 to verify a complex HW/SW interface in a large SDH/SONET chip – and slashed verification time and effort by 70 percent. Read their story here!
• File Formats: More information on IP-XACT can be found at Wikipedia and through Accellera IP-XACT Working Group. Common alternatives are Register Description Language and SystemRDL , also an Accellera standard.