Invariant-Strengthened Elimination of Dependent State Elements

Abstract-- 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 SATbased 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 25% on average in large industrial designs, even after other aggressive optimizations such as minregister retiming have been applied.

• Type: Conference
• Year: 2008
• Where: FMCAD
• Authors: Michael L. Case, Alan Mishchenko, Robert K. Brayton, Jason Baumgartner, Hari Mony
• Keywords: Dependent State Elements, FMCAD 2008, Formal Methods, State Element, Technology-independent Synthesis Optimization