In this paper, we examine the need for formal sequential equivalence checking
across pairs of RTL models. We present scenarios that call for modifying the
sequential behavior of RTL models while preserving functionality. These
primarily have to do with reliably achieving aggressive timing and power goals typical of high performance design.
The advantages of verifying such sequential modifications using formal methods at the block level are identified. Some attention to front end design methodology can vastly improve the efficiency of sequential equivalence checking tools.
1 Introduction
The ability to formally determine functional equivalence between RTL models is seen as a key enabler in physically aware front-end design methodologies that are being practiced in high performance designs. In this paper, we describe sequential equivalence checking (SEC) technology and the usage of such a tool in various a practical design flows.
Commercially available equivalence checking tools today require states in the designs are tested to have one-to-one functional maps. This implies that every flop in one design must have a functionally identical flop in the partner design. As such, these tools are combinational equivalence checkers. They find maximum utility in proving that a gate level implementation of an RTL design is correct. A secondary application is that a gate level ECO can be proven not to have compromised the original functionality of RTL or gate level design.
Pixley has described the concept of sequential hardware equivalence (SHE) in [1]. We define SEC as the process of formally proving functional equivalence of designs that may in general have sequentially different implementations. Examples of sequential differences span the space from retimed pipelines (thus breaking the maps between registers, and rendering combinational equivalence checkers ineffective), differing latencies and throughputs (allowing for checking re-pipelined designs), and even scheduling and resource allocation differences.
These sequential modifications to a design are ways to robustly meet timing, area and power goals in a reliable manner. Traditionally, such modifications are frowned upon in a simulation based verification flows because of the work involved in gaining confidence in their correctness. However, sequential equivalence checking enables designers to comprehensively verify sequential design changes with trivial effort.
In the remainder of this paper, we describe some motivations for performing sequential changes to RTL designs in Section 2. Section 3 discusses some of the methodological aspects concerned with application of sequential equivalence checking to real designs. We describe technical challenges in performing sequential equivalence checking on RTL designs in section 4.
2 Case for sequentially differing models
Achieving back-end closure and meeting timing goals is perhaps the activity that consumes the maximum time and effort in today's high performance microprocessor designs. Given the tight timing goals and area constraints, simply employing larger drivers is no longer a viable solution in tackling this problem. Designers must resort to techniques that alter the sequential nature of the circuit. From a timing perspective, there are two techniques that are used most commonly:
Figure 1 — Examples of sequential changes made for timing improvement
1. Re-timing or moving combinational logic across flop boundaries in order to meet max timing constraints. Examples 1 and 2 in Figure 1 illustrate such a change.
2. Re-pipelining or adding pipeline stages to a computation, trading
off latency in order to maintain throughput while meeting max timing constraints. Example 3 in Figure 1 illustrates such a change.
3. Pre-computation, or re-ordering a computation to have results ready earlier in a clock cycle.
Let us consider each of the transformations mentioned in turn. In flat data pipelines, retiming usually involves moving logic across flip-flops. From a combinational equivalence checking point of view, this operation effectively changes the functionality of the flip-flops in the modified circuit as compared with the original design.
This renders combinational equivalence checking tools ineffective in formally verifying the functionality of the retimed circuit, and designers must resort to other means of verification. The general case of re-timing of circuits with reconvergent paths often necessitates logic replication, and the re-timed design might even contain more flip-flops than the original circuit. This technique has also been automated by many of the synthesis tools available in the market.
