Record and play: a structural fixed point iteration for sequential circuit verification

This paper proposes a technique for sequential logic equivalence checking by a structural fixed point iteration. Verification is performed by expanding the circuit into an iterative circuit array and by proving equivalence of each time frame by well-known combinational verification techniques. These exploit structural similarity between designs by local circuit transformations. Starting from the initial state, for each time frame the performed circuit transformations are stored (recorded) in an instruction queue. In subsequent time frames the instruction queue is re-used (played) and updated when necessary. At some point the instruction queue does not need to be modified any more and is valid in all subsequent time frames. Thus, a fixed point is reached and machine equivalence is proved by induction. Experimental results show the great promise of this approach to verify circuits after resynthesis and retiming.