Verifying Power Optimized Designs Using Sequential Analysis

All power optimization tools can perform combinational optimization, where there is an opportunity to gate a register clock input, based on the combinational logic that is feeding the register’s data input. While this method works well and does not alter the logic behavior at the register, the problem is that it leaves additional power saving opportunities on the table.

However, sequential optimization utilizes opportunities for power savings that span across the register boundaries. By performing deep sequential analysis of a design, a power optimization tool can do an exhaustive analysis, finding all possible optimizations. Some of these tools can even reject some of the possible moves based on analysis of area and timing constraints as well as the power consumption of the move’s added logic.

By analyzing across register boundaries, sequential optimizations change the functionality at internal registers — but maintain the same functionality at the outputs.

(Source: Calypto)

In a simple example, consider two registers (Figure 1, above): a sending register (connected to din) and a receiving register (connected to dout). The receiving register has a feedback multiplexer, such that when the multiplexer is selected, the register output is fed back to its input. The receiving register does not always “observe” its input, depending on the selected input of the multiplexer. So when the multiplexer is not selected, the sending register is not observed. In this case, the multiplexer is replaced with a clock gater (blue). The clock gater prevents the receiving register from being clocked when the data is not valid, saving power. This is conventional combinational clock gating.

When the sending register is not observed, the power optimization tool can gate it to save power by adding a clock gater (red). This analysis crosses the valid register boundary, so it is sequential clock gating. The sending register now has different states when gated from the original design, but the output of the receiving register is unchanged.

It is important to understand that normal LEC will not work with sequential clock gating. When we modify a design’s source code, such as when creating RTL and netlists, it is standard design practice to carefully check the resulting new source code. Many designers check their logic synthesis with a formal logic equivalency checker (LEC). When modifying a gate-level netlist for a timing ECO, LEC is used to ensure that the design has not been changed functionally. The LEC tool analyzes two logic designs and checks them for logic equivalency. It matches each register between the two representations, and it matches the combinational logic at each register data input.

As we have seen, sequential optimizations change the functionality at internal registers. This poses a problem for conventional LEC tools. The power optimization tool may add some registers, resulting in the LEC tool having a mismatch. It may also change the combinational logic functions at some registers. So a simple LEC tool cannot handle a sequentially optimized design.

As stated earlier, it is good design practice to verify the logical equivalence between the original RTL and the power optimized RTL. Although a combinational LEC tool cannot match the two designs, a sequential logical equivalence checker can. Calypto® has just such a tool, called SLEC®. SLEC is a formal equivalence checking tool that has a number of special capabilities, and checking power-optimized RTL is one of its features.

However, some design teams may have a requirement to use a specific combinational LEC tool for verification. There is a workaround to allow this when using Calypto’s PowerPro® automated power reduction tool, but there is a limitation. PowerPro can add an override signal to enable logic that disables the optimizations. The control signal becomes a top-level port in the optimized design. A combinational LEC tool can assert this signal and verify the design. Because a combinational LEC tool does not check the enabled logic, you will need to use a sequential LEC tool — i.e., SLEC — to validate that it is correct.