Application of the retimed normal form to the formal equivalence verification of abstract RTL descriptions for pipelined designs
AssigneeIntel Corporation
InventorsZurab Khasidashvili, John Moondanos, Ziyad Hanna
Life of this patent
Estimating the term…
Abstract
A method for facilitating the sequential verification of loop-free circuits by reducing the sequential verification problem to combinational verification, by constructing and comparing Timed Binary Decision. Diagrams (TBDDs) and Timed Binary Expression Diagrams (TBEDs). The TBEDs can be compared by using both BDDs and SAT solvers.
Claims18
A formal equivalence verification method comprising:
- listing latches in a predetermined order;
- representing the latches in a binary format;
- computing a Timed Binary Expression Diagram (TBED) using the binary format;
- and
- verifying equivalence of a circuit using the computed TBED.
A system for performing formal equivalence verification comprising a processor that defines a state transition for one or more latches in a circuit, places the latches in a predetermined order, represents the latches in a binary format, computes a Timed Binary Expression Diagram (TBED) using the binary format, and verifying equivalence of a circuit using the computed TBED.
A computer readable media having program code embedded therein, the program code comprising:
- code that lists latches in a predetermined order;
- code that represents latch functions in a binary format;
- code that computes a Timed Binary Expression Diagram (TBED) using the binary format;
- and
- code that verifies equivalence of a circuit using the computed TBED.
Dependencies are inferred from the claim text.