Sequential Equivalence Checking for Clock-Gated Circuits
Autor: | Hamid Savoj, Robert K. Brayton, Alan Mishchenko |
---|---|
Rok vydání: | 2014 |
Předmět: | |
Zdroj: | IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems. 33:305-317 |
ISSN: | 1937-4151 0278-0070 |
Popis: | 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. |
Databáze: | OpenAIRE |
Externí odkaz: |