June 12, 2006 -- Equivalency checking is an important and necessary step to verify the functional correctness of a design’s implementation. However, circuit retiming introduces changes that strike at the fundamental techniques used by combinational equivalency checking technology. Retiming changes can make formal verification of large designs a complex and often impossible task. Formality has developed a breakthrough approach to verify the functional correctness of large retimed designs.

The retiming verification problem

Combinational equivalence-checking (EC) tools verify whether two versions of a design at different stages of implementation are functionally equivalent. The known functionally correct design is referred to as the reference design. The design being verified against the reference is referred to as the implementation design. As an EC tool reads a design, it is segmented into smaller components called logic cones. A logic cone is simply a set of logic bounded by registers, primary inputs/outputs, or black boxes (Figure 1). Logic cone outputs are referred to as compare points.

Figure 1. Logic cone

Retiming shifts registers across combinational logic to transfer the associated delay from a path with negative slack to a neighboring path with available slack. During synthesis, retimed registers can be moved either forwards or backwards through logic. In many cases, the register moves will result in forking (duplicating) or combining registers. Figure 2 highlights examples of register retiming. Register classes, those with the same clock/set/clear functionality, are denoted by class names C1, C2, and C3. G1 and G2 represent combinational cells.

Figure 2. Examples of register retiming

Since the registers have been moved, added, and/or combined; retiming changes the number, structure, and size of logic cones as well as the logic contained within a given logic cone. Changing the number of logic cones results in compare points that cannot be matched between the two designs; moreover, those that are matched may no longer be functionally equivalent. When taken as a whole the design is functionally equivalent, but since the individual matched compare points are not, the verification will fail. This result is referred to as a “false difference.”

Consider the very simple pre- and post-retimed circuit of Figure 3.

Figure 3. Simple retimed circuit with logic cones highlighted

In this example, the EC tool will identify the logic cones as indicated. The reference design contains three logic cones that can be identified by compare points Reg_1, Reg_2, and Out_1. The implementation design contains two logic cones identified by compare points Reg_1_2 and Out_1. Compare points Out_1 will be easily matched between the two designs, but the other compare points will not, preventing a complete verification. Additionally, the matched Out_1 compare points are not functionally equivalent and the verification will fail (a false difference).

Traditional retiming verification approaches

Sequential equivalence checking is one approach that may be used to verify retimed designs. Unlike EC tools that rely on one-to-one state point matching, sequential tools do not. Here the state space of a design is transformed while the behavior of the primary outputs remains the same. Sequential equivalence checking is currently limited to relatively small circuits and state machines, and cannot be readily applied to large circuits where thousands of retiming moves have been introduced.

Another approach to verifying retimed designs is to normalize both the reference and implementation designs into a standard canonical form. Once a standard form is obtained, the designs are then compared. This approach has been successful for several classes of designs, including pipelined multipliers, but it suffers from two shortcomings. First, the normalization process can be quite time consuming. Second, and more importantly, a single canonical form for each design does not always exist. Designs that contain loops of registers, where retiming has occurred somewhere along the path of the loop, is a commonly occurring example. Registers within these loops will remain throughout the normalization process. When the reference and implementation start with different loops, they cannot be normalized to a common structure.

A third approach, a guided approach, is possible if the retiming moves can be recorded during the optimization process. The record can then be provided to the EC tool to guide it during the compare point matching process. Unfortunately, the EC tool cannot simply apply the moves to one design in an attempt to create the same state space. In RTL-togate verifications, the record defines moves made by synthesis after it elaborates the RTL into a gate-level representation. EC tools have their own independent elaboration process. The elaborated RTL netlist within the EC tool may be structurally different from that within the synthesis tool, and it is not possible to simply duplicate the retiming moves across registers from a structurally different starting point.

Comprehensive retiming verification

To verify today’s large and complex designs, the only potentially comprehensive and scalable solution is the guided approach. The recorded moves can be used to define logical transformations between the two designs, but new technology is required to understand how to apply the transformations. The Synopsys Formality Equivalence Checker has solved the problem and brought retiming verification into the domain of combinational equivalence checking.

The solution centers on introducing the recorded transformations into Formality’s design representations without altering design functionality. To achieve this, two new functional components are created and are shown in Figure 4. The first, designated the “white box,” contains the logic transformation as recorded during retiming. The second, designated the “black box,” is an abstract representation whose function is defined to be the “inverse” of the white box. The “inverse” function is a theoretical function only. It will not need to be implemented and in actuality is typically impossible to implement. If these two boxes are connected in series, in either order, the function and its inverse cancel each other out. By introducing this function/inverse combination into the designs we can maintain design functionality and provide a solution using combinational equivalency checking.

Figure 4. A “white” and “black” box.

The introduction of the white and black box has the effect of creating additional compare points in both the reference and implementation designs so that the designs can be matched for verification. If verification succeeds, the retimed designs are sequentially equivalent despite the combinational differences due to retiming. If verification fails, Formality will identify the area in the implementation which has caused the problem.

The following series of diagrams illustrates Formality’s pioneering technique. Figure 5 shows the white box and black box that are added to the retimed reference design found in Figure 3. The white box represents the register-traversed logic that was recorded during the retiming, in this case an “or” gate. The black box represents the theoretical inverse of the traversed logic. The inclusion of these blocks has no net affect on the functionality of the design.

Figure 5. Addition of traversed logic and its inverse to the reference design.

The next step is to recognize from the recorded information that a register transformation occurred during retiming. Reg_1 and Reg_2 have combined to form a single register. This combination can be accomplished by pulling the register to the input of the black box. Figure 6 shows Formality’s resulting representation for the reference design.

Figure 6. Register is pulled through the black box.

Figure 7. Conceptual mapping between original and new RTL.

Figure 8 illustrates the resulting implementation design after applying the recorded information. Within the implementation design, no register shift is necessary since the register transformation was already accounted for in the representation of the reference design.

Figure 8. The new implementation design representation.

The new reference and implementation design representations can now be easily matched for verification as shown in Figure 9.

Figure 9. New design representations are easily matched. (The dashed triangles represent matching logic cones.)

Though this is a trivial example, it undoubtedly highlights the technical application. Consider if the OR gate had been optimized into a larger set of neighboring logic or if the retimed registers numbered in the thousands. Such cases are not trivial, but Formality will be able to verify the functional equivalence of the two designs.

Built-in safety

It is beyond the scope of this paper to provide the mathematical proof showing that no false equivalence can result by applying the recorded information. However, it should be sufficient to note that the gates contained within white boxes are always verified against original logic. It is a complete contextual check and does not allow an incorrect transformation to generate a false equivalence. Furthermore, the addition of the white box and black box components do not change the functionality of the designs. These components create compare points that allow Formality to proceed with its task of verifying the designs and presenting any functional differences. If for any reason the recorded information is incorrect, equivalence checking would fail, and an error would be detected by Formality. In such cases, Formality’s Error-ID Technology will quickly isolate the problem to the logic within the white box.

Results

With this approach, Formality has been able to extend the reach of EC technology to include retimed designs previously unsolvable. In addition, these verifications have been accomplished efficiently. Table 1 illustrates a small sampling of the results obtained using Formality’s new approach.

Conclusion

A record of retiming information generated from Design Compiler enables Formality to easily solve previously unverifiable retimed designs. This capability allows users take full advantage of Design Compiler’s timing optimizations to maximize QoR without compromising the ability to verify the design. Retiming verification is available today to Synopsys customers via Formality’s Guided Setup flow (SVF).

About Formality

Formality is a full-chip functional equivalence checker. With Formality's exhaustive static verification methodology, designers can fully verify multimillion-gate designs in relatively short times. Formality’s industry-leading capacity, performance, and completion make Formality the customer-preferred EC solution. Formality supports 32- bit and 64-bit platforms, is supported in all major vendor flows, and is part of Synopsys' industry-leading, full-flow design solution.

By Robert Vallelunga and Mike Tarsi.

Robert is Formality Product Manager and Mike is Formality Engineering Manager at Synopsys, Inc.