Automatic generalized phase abstraction for formal verification

Abstract

A standard approach to improving circuit performance is to use an N-phase design style where combinational logic is interspersed freely between level sensitive latches controlled by separate clocks. Unfortunately, the use of an N-phase design style will increase the number of state variables by a factor of N, making formal verification many orders of magnitude harder. Previous approaches to solving this problem restrict the kind of designs that can be handled severely and construct an abstracted netlist with fewer state variables by a syntactic analysis that requires the user to identify clocks. We extend the current state of the art by introducing a phase abstraction algorithm that (1) poses no restrictions on the design style that can be used, that (2) avoids an error prone syntactic analysis, that (3) requires no input from users, and that (4) can be integrated into any model checker without requiring HDL code analysis.