On verifying the correctness of retimed circuits

We address the problem of verifying a retimed circuit. After retiming, some latches in a sequential circuit are repositioned to reduce the clock cycle time and thus the behavior of the combinational portion is changed. Here, we present a novel approach to check the correctness of a retimed circuit according to the definition of 3-valued equivalence. This approach is based on our verification framework using sequential ATPG techniques. We further incorporate an algorithm to pre-process the circuits and make the verification process even more efficient. We will present the experimental results of verifying the retimed circuits with hundreds of flip-flops on ISCAS89 benchmark circuits to show its capability