Automated Formal Verification of a Highly-Configurable Register Generator

TL;DR

An automated register verification framework using formal methods following the Model Driven Architecture (MDA) is proposed, based on which the human effort in the register verification can be reduced significantly, from 20Person-Day to 3PD for each configuration, and 100% code coverage can be achieved.

Abstract

Registers in IP blocks of an SoC perform a variety of functions, most of which are essential to the SoC operation. The complexity of register implementation is relatively low when compared with other design blocks. However, the extensive number of registers, combined with the various potential functions they can perform, necessitates considerable effort during implementation, especially when using a manual approach. Therefore, an in-house register generator was proposed by the design team to reduce the manual effort in the register implementation. This in-house register generator supports not only the generation of register blocks but also bus-related blocks. Meanwhile, to support various requirements, 41 generation options are used for this generator, which is highly-configurable. From the verification perspective, it is infeasible to achieve complete verification results with a manual approach for all options combinations. Besides the complexity caused by configurability, the register verification is still time-consuming due to two widely recognized issues: the unreliability of specifications and the complexity arising from diverse access policies. To deal with the highly-configurable feature and both register verification issues, we propose an automated register verification framework using formal methods following the Model Driven Architecture (MDA). Based on our results, the human effort in the register verification can be reduced significantly, from 20Person-Day (20PD) to 3PD for each configuration, and 100\% code coverage can be achieved. During the project execution, eleven new design bugs were found with the proposed verification framework.

Figures (5)

• Figure 1: (a) Overview of the in-house register generator. (b) Simplified diagram of generated RTL blocks.
• Figure 2: Proposed property generation flow for the register generator.
• Figure 3: Simplified MoT model for specification extraction.
• Figure 4: Example properties.
• Figure 5: Verification results of the proposed framework.