Invariant-Strengthened Elimination of Dependent State Elements
Michael L. Case, Alan Mishchenko, Robert K. Brayton, Jason Baumgartner, Hari Mony · 2008
This work presents a technology-independent synthesis optimization that is effective in reducing the total number of state elements of a design. It works by identifying and eliminating dependent state elements which may be expressed as functions of other registers. For scalability, we rely exclusively on SAT- based analysis in this process. To enable optimal identification of all dependent state elements, we integrate an inductive invariant generation framework. We introduce numerous techniques to heuristically enhance the reduction potential of our method, and experiments confirm that our approach is scalable and is able to reduce state element count by 12% on average in large industrial designs, even after other aggressive optimizations such as min- register retiming have been applied. The method is effective in simplifying later verification efforts.