Automated Formal Verification of a Highly-Configurable Register Generator

TL;DR

This paper presents an automated formal verification framework for a highly-configurable register generator in SoC design, significantly reducing manual effort and ensuring complete coverage despite complex configurations.

Contribution

It introduces a formal verification approach tailored for a highly-configurable register generator, achieving full coverage and bug detection with minimal human effort.

Findings

Verification effort reduced from 20PD to 3PD per configuration

Achieved 100% code coverage across configurations

Discovered 11 new design bugs during verification

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.