Maximal Input Reduction of Sequential Netlists via Synergistic Reparameterization and Localization Strategies

Abstract. Automatic formal verification techniques generally require exponential resources with respect to the number of primary inputs of a netlist. In this paper, we present several fully-automated techniques to enable maximal input reductions of sequential netlists. First, we present a novel min-cut based localization refinement scheme for yielding a safely overapproximated netlist with minimal input count. Second, we present a novel form of reparameterization: as equivalence preserving structural abstraction, which provably renders a netlist with input count at most a constant factor of register count. In contrast to prior research in reparameterization to offset input growth during symbolic simulation, we are the first to explore this technique as a structural transformation for sequential netlists, enabling its benefits to general verification flows. In parwe detail the synergy between these input-reducing abstractions, and with other transformations such as retiming which ...

• Type: Conference
• Year: 2005
• Where: CHARME
• Authors: Jason Baumgartner, Hari Mony
• Keywords: CHARME 2005, Hardware, Input Count, Minimal Input Count, Register Count