Register Verification: Do We Have Reliable Specification?

IP designs contain many externally accessible registers, referred to as memory-mapped registers, that are used to control behavior, check status, and transmit and receive data. The implementation complexity of memory-mapped registers is relatively low compared with other design elements. Hence, register verification, the verification of memory-mapped registers, is mostly done by directed or lightly randomized simulation test benches and is viewed as a tedious job.

Accessing memory-mapped registers is often no different from accessing general-purpose memory. Techniques used to verify general-purpose memory are a good starting point for register verification. However, to improve efficiency, memory-mapped registers can have complex access policies. For example, a read-to-clear policy automatically clears the content of a register after reading it. The contents of a memory-mapped register may also be modified by internal operations. These complicate the task of register verification.

Another practical difficulty is the lack of a reliable specification. The specification documents not uncommonly omit details, such as precisely when a memory-mapped register can be modified by internal operations. Developing a quality verification environment from an insufficient specification is a painful task: designers and verification engineers will be frustrated by many test failures resulting from undocumented behavior. To complete the verification task, they may mask or ignore failures. In the best scenario, the verification environment will be tediously updated until no more failures are observed.

In this paper, we use formal verification to overcome the practical challenges of producing a reliable specification. We start register verification assuming no specification is available. Instead of verifying a target design based on a given specification, we use formal verification to explore all possible behaviors for each memory-mapped register. To embrace the wide range of register behaviors, we developed a register model based on four aspects of register behavior.

A small program post-processes the formal verification results and determines how each register behaves. Then, it identifies the access policies consistent with that behavior. If the identification matches the designer's intention, the verification is already done, since formal verification has thoroughly verified all possible behaviors. If it doesn't match, then there is either a design bug or an overlooked aspect of the registers' behavior.

In Section 2, we give an overview and describe the benefits of our proposed register verification method. The implementation is introduced at a high-level in Section 3. In Section 4, we show a few different approaches to developing properties for formal verification and discuss the implementation and the instantiation of the properties. The post-processing required after formal verification is described in Section 5. We present results in Section 6 and conclude in Section 7.

Overview

Figure 1 shows the steps in our verification flow. A target design is all that is needed to start the register verification; no specification of the memory-mapped registers in the design is required. The Register Verification Package (RVP) binds a set of properties that explores the register behavior of the target design. We call this type of property an exploration property. Formal verification exhaustively explores the design and determines which exploration properties are satisfied.

^{Figure 1: The flow of proposed register verification method}

^{(Green ovals denote either input or output of a process. Blue rectangles denote processing steps.)}

For the post-processing step, we developed a small program to interpret the formal verification results and produce comprehensive information on register behavior in a form of high-level specification. Because formal verification is exhaustive, the information produced in this step reflects the implementation of the individual memory-mapped registers in the design. We call this the implemented specification. If the designer sees that the implemented specification is exactly aligned with his design intent, register verification is complete. The implemented specification can be treated as the concrete intended specification.

If designer sees a mismatch, it is either a design bug or an overlooked aspect of the register behavior. The ability to detect overlooked register behavior is a key benefit of our method. It is difficult to manually maintain a good quality specification because of frequent design changes and complicated register behaviors. When verification is performed using an incomplete or unreliable specification, bugs are much more likely to escape to silicon. Our method leverages the exhaustive analysis of formal verification to avoid this common pitfall.