Compositional verification of retiming and sequential optimizations

Once a design is both retimed and sequentially optimized, sequential equivalence verification becomes very hard since retiming breaks the equivalence of the retimed sub-blocks although the design equivalence is preserved. This paper presents a novel compositional algorithm to verify sequential equivalence of large designs that are not only retimed but also optimized sequentially and combinationally. With a new notion of conditional equivalence in the presence of retiming, the proposed compositional algorithm performs hierarchical verification by checking whether each sub-block is conditionally equivalent, then checking whether the conditions are justified on their parent block by temporal equivalence. This is the first compositional algorithm handling both retiming and sequential optimizations hierarchically. The proposed approach is completely automatic and orthogonal to any existing sequential equivalence checker. The experimental results show that the proposed algorithm can handle large industrial designs that cannot be verified by the existing methods on sequential equivalence checking.