Automatic Verification and Identification of Partial Retention Register Sets for Low-Power Designs

Today's low-power designs switch between active and standby modes depending on their activity. While the design is in standby mode, its power supply can be turned off to prevent static power consumption. Retention registers are used in these low-power designs to maintain design state even when power is turned off. However, replacing all normal registers with retention registers results in significant area and power overhead. As a consequence, designers often go through the tedious and error-prone process of identifying a partial set of retention registers required to maintain correct design functionality. Further, checking for the correctness of this partial retention set is limited to simulation-based validation. In this paper, we develop model-checking based techniques to formally verify the correctness of a partial retention set for a low-power design. Further, we propose automatic algorithms to help designers identify compact partial retention sets. These algorithms can leverage designers' knowledge to reduce the overall search space and improve scalability. Experiments on open-source designs demonstrate the efficiency and effectiveness of the proposed algorithms. We also show how utilizing design knowledge can help scale our method up to handling designs with about 400K flip-flops.