Sequential Equivalence Checking for Clock-Gated Circuits

Sequential logic synthesis often leads to substantially easier equivalence checking problems, compared to general-case sequential equivalence checking (SEC). This paper theoretically investigates when SEC can be reduced to a combinational equivalence checking (CEC) problem. It shows how the theory can be applied when sequential transforms are used, such as sequential clock gating, retiming, and redundancy removal. The legitimacy of such transforms is typically justified intuitively, by the designer or software developer believing that the two circuits reach the same state after a finite number of cycles, and no difference is observed at the outputs due to fanin non-controllability and fanout non-observability effects. A method based on these theorems was applied to 12 large industrial examples, which had been combinationally and sequentially clock-gated by a commercial clock-gating tool. These examples lead to SEC problems, which are problematic for a general, state-of-the-art SEC engine. The new approach completed verification of all examples and was about 30 times faster on the 3 cases where the conventional SEC engine was able to prove the problem within one hour.