Patent ID: 7237208

Claim:
A computer-implemented method for performing formal verification of a circuit design that includes a plurality of datapath elements, the method comprising: detecting a first datapath element in a circuit design, wherein detecting the first datapath element comprises matching a portion of the circuit design including one or more datapath elements with a datapath element in a component library; replacing the first datapath element in the circuit design with a first abstraction the first abstraction applying a constraint relating an incoming signal of the first datapath element to an output of the first data path element; locating a second datapath element in the circuit design by tracing a data signal of the detected first datapath element through the circuit design to the second datapath element; replacing the second datapath element in the circuit design with a second abstraction the second abstraction applying a constraint relating an incoming signal of the second datapath element to an output of the second data path element; and passing the abstracted circuit design to a formal verification system, the abstracted circuit design including the first and second abstractions.