Method for modeling and verifying timing exceptions
View Patent ↗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.
1. 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;
wherein a re-convergence point is a point in the false path that starts from a starting point and does not pass through at least one preceding through point.
2. The method of claim 1 , further comprising reporting on paths that are verified as false paths.
3. The method of claim 1 , wherein the false path is a functional false path.
4. The method of claim 1 , wherein the re-convergence points are points included in a path that starts from a starting point and does not pass through preceding through-points of the false path.
5. The method of claim 4 , wherein the identified re-convergence points are added to the through points of the false path.
6. The method of claim 1 , wherein verifying the satisfiability formula further comprises determining whether the output of the satisfiability formula equals to a zero logic value for any logic value set in inputs of the logic circuits.
7. The method of claim 1 , wherein the Boolean satisfiability solver comprises at least one of: Boolean satisfiability problem (SAT), automatic test pattern generation (ATPG), and binary decision diagram (BDD).
8. A computer aided design (CAD) system embodying a CAD program, said CAD program comprising a computer readable medium with instructions adapted to implement the method of claim 1 .
9. A computer program product embodied on a computer readable medium with instructions that when executed on a computer perform the method of claim 1 .
10. A computer-implemented method, for modeling and in 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,
wherein modeling the false path to satisfiability formula comprises:
duplicating a logic circuit that includes the false path;
connecting each pair of through points in the false path to a XOR gate;
connecting each pair of end points in the false path to a XOR gate;
connecting the outputs of the XOR gates to an AND gate;
setting the inputs of the through points to zero and one logic values; and
setting the pair of starting points in the false path to zero and one logic values.
11. The method of claim 10 , wherein connecting each pair of through points further comprises de-coupling the through points from the logic circuits.
12. The method of claim 10 , wherein the through points comprise re-convergence points.
13. 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,
wherein modeling the multi-cycle path to satisfiability formula comprises:
duplicating a logic circuit that includes the multi-cycle path;
connecting each pair of through points in the multi-cycle to a XOR gate;
connecting each pair of end points in the multi-cycle path to a XOR gate;
connecting the outputs of the XOR gates to an AND gate;
setting the inputs of the through points to zero and one logic values; and
setting the pair of starting points in the multi-cycle path to zero and one logic values.
14. The method of claim 13 , further comprising reporting on paths that are verified as multi-cycle paths.
15. The method of claim 13 , wherein the multi-cycle path is a path where a signal can propagate from an input to an output in at least two clock cycles.
16. The method of claim 15 , wherein verifying the satisfiability formula further comprises determining whether the satisfiability formula can be solved in less clock cycles than it requires for a signal to propagate through the multi-cycle path.
17. The method of 13 , wherein the Boolean satisfiability solver comprises at least one of: Boolean satisfiability problem (SAT), automatic test pattern generation (ATPG), and binary decision diagram (BDD).
18. A computer aided design (CAD) system embodying a CAD program, said CAD program comprising a computer readable medium with instructions adapted to implement the method of claim 13 .
19. A computer program product embodied on a computer readable medium with instructions that when executed on a computer perform the method of claim 13 .