Enhancing Sequential LEC Using a Cumulative Verification Methodology

This paper describes a methodology for verifying sequentially optimized designs using sequential equivalence checking. The problems associated with verifying large designs with complex changes using current sequential equivalence checking tools are presented. This methodology aims to solve some of these problems by simplifying either the size of the circuit or the number of changes presented to the checking tool at any one time. Key to this methodology is the use of a tool called rapport for generating wrappers for the blocks being verified. Finally, the challenges with the methodology and a case study of using the methodology to verify a RISC core are presented.