US 2008/0178132 A1 · Computer program product for design verification using sequential and combinational transformations

Abstract

System and software for verifying that a model of an integrated circuit satisfies its specification includes performing a sequence of at least one sequential transformation on a sequential model of the integrated circuit to produce a simplified sequential model of the integrated circuit. Thereafter, the simplified sequential model is unfolded for N time steps to create a combinational representation of the design. A sequence of at least one combinational transformation algorithms is then performed on the unfolded design to produce a simplified unfolded model. Finally, an exhaustive search algorithm is performed on the simplified unfolded model. The sequence of sequential transformations may include a sequential redundancy removal (SRR) algorithm and/or another sequential algorithm such as a retiming transformation. The combinational transformations may include a combinational redundancy removal algorithm or a logic re-encoding algorithm. The exhaustive search includes performing an exhaustive satisfiability search by propagating a binary decision diagram (BDD) through the netlist.

Claims6

Dependent claims

1-20. (canceled)

A computer program product comprising computer executable instructions, stored on a computer readable medium, for a process of verifying whether a model of an integrated circuit satisfies its specification, comprising:

computer code means for performing a sequence of at least one sequential transformation on a sequential model of the integrated circuit to produce a simplified sequential model of the integrated circuit;
computer code means for unfolding the simplified sequential model for N time steps to produce a combinational model of the integrated circuit;
computer code means for performing a sequence of at least one combinational transformation on the combinational model to produce a simplified combinational model;
and
computer code means for performing an exhaustive search of states of the simplified combinational model, wherein the computer code means for performing the exhaustive search comprises computer code means for performing an exhaustive satisfiability search, and wherein the computer code means for performing an exhaustive satisfiability search includes computer code means for propagating a binary decision diagram (BDD) through a netlist;
and
computer code means for storing a result of the verifying process in response to i) performing a predetermined number of iterations of the verifying process, or else ii) the verifying process encountering a checkstop or no new states.

4 more elements

Dependencies are inferred from the claim text.

Computer program product for design verification using sequential and combinational transformations

Life of this patent

Computer program product for design verification using sequential and combinational transformations

Life of this patent

Abstract

Claims6