Method for modeling and verifying timing exceptions
AssigneeAtrenta, Inc.
InventorsSolaiman Rahim, Mayank Jain
Life of this patent
Estimating the term…
Abstract
A method and system for timing exception verification in integrated circuit (IC) designs included verification of functional false paths as well as multi-cycle paths (MCPs). A false path or a MCP is modeled to a satisfiability formula and the formula is validated using a Boolean satisfiability solver. Time required for timing exception verification can be significantly reduced.
Claims23
A computer-implemented method, for modeling and verifying false paths in integrated circuit (IC) design, comprising:
- receiving a constraints file that includes at least one definition of a false path;
- for each false path in the constraints file, identifying re-convergence points in an input netlist of the IC design;
- modeling the false path together with the re-convergence points to produce a satisfiability formula;
- verifying the satisfiability formula using a Boolean satisfiability solver;
- storing a verification result of the verifying step in the memory of the computer;
- and
- providing a verification output based on the verification result.
A computer-implemented method, for modeling and verifying multi-cycle paths in integrated circuit (IC) design, comprising:
- receiving a constraints file that includes at least one definition of a multi-cycle path;
- for each multi-cycle path in the constraints file, modeling the multi-cycle to a satisfiability formula;
- verifying the satisfiability formula using a Boolean satisfiability solver;
- storing a verification result of the verifying step in the memory of the computer;
- and
- providing a verification output based on the verification result.
A system for modeling and verifying timing exceptions in integrated circuit (IC) design, comprising:
- a database for maintaining a netlist of the IC design and a constraints file, wherein the constraints file includes at least one definition of a timing exception;
- a transform module for modeling each path the timing exception into a satisfiability formula;
- and
- a solver for verifying the satisfiability formula.
Dependencies are inferred from the claim text.