Integrated circuit design model splitting for formal verification

Abstract

An apparatus for model splitting includes an extraction module that extracts netlist parameters from a static netlist. The netlist parameters include node parameters of each node of the static netlist. The node parameters include node connection information and execution cycle information. The nodes of the static netlist include nodes of an integrated circuit design from an input to an output. A split node module analyzes, using the netlist parameters, each node in a cycle and determines if each node is a potential split node, which is a node with a projected sub-proof execution time less than a time limit. A split chain module determines if a split chain exists. The split chain includes a connection between potential split nodes from the input to the output at each execution cycle. A reporting module reports nodes of a split chain in response to determining that a split chain exists.