Incremental routing for circuit designs using a SAT router

• US 10,445,456 B1
• Filed: 06/14/2017
• Issued: 10/15/2019
• Est. Priority Date: 06/14/2017
• Status: Active Grant

• Current Assignee: Xilinx, Inc. (Advanced Micro Devices, Inc.)
• Original Assignee: Xilinx, Inc. (Advanced Micro Devices, Inc.)
• Inventors: Fraisse, Henri
• Primary Examiner(s): Garbowski, Leigh M
• Application Number:
  US15/623,302
• Time in Patent Office: 853 Days
• Field of Search: None
• CPC Class Codes: G06F 2111/04 Constraint-based CAD
• CPC Class Codes: G06F 2119/12 Timing analysis or timing optimisation
• CPC Class Codes: G06F 30/3312 Timing analysis
• CPC Class Codes: G06F 30/3323 using formal methods, e.g. equivalence checking or property checking
• CPC Class Codes: G06F 30/34 for reconfigurable circuits, e.g. field programmable gate arrays [FPGA] or programmable logic devices [PLD]
• CPC Class Codes: G06F 30/39 Circuit design at the physical level physical level design for reconfigurable circuits G06F30/347
• CPC Class Codes: G06F 30/394 Routing G06F30/396 takes precedence
• CPC Class Codes: G06F 30/398 Design verification or optimisation, e.g. using design rule check [DRC], layout versus schematics [LVS] or finite element methods [FEM] optical proximity correction [OPC] design processes G03F1/36

Abstract

Routing a circuit design for implementation within an integrated circuit can include determining a set of candidate paths from available paths of the integrated circuit for connecting source-sink pairs of the circuit design, wherein the set of candidate paths is initially a subset of the available paths, and generating, using a processor, an expression having a plurality of variables expressed as a conjunction of routing constraints representing legal routes of the source-sink pairs using only the candidate paths. A routing result for the circuit design can be determined by initiating execution of a SAT solver on the expression using the processor.

Claims

1. A method of routing a circuit design for implementation within an integrated circuit, the method comprising:

determining a set of candidate paths from available paths of the integrated circuit for connecting source-sink pairs of the circuit design, wherein the set of candidate paths is initially a subset of the available paths;

generating, using a processor, an expression having a plurality of variables expressed as a conjunction of routing constraints representing legal routes of the source-sink pairs using only the candidate paths;

determining, using the processor, a routing result for the circuit design by initiating execution of a SAT solver on the expression; and

in response to the routing result indicating that the expression is not satisfiable, expanding the set of candidate paths, extending the expression using the expanded set of candidate paths, and initiating further execution of the SAT solver on the extended expression.

2. The method of claim 1, wherein the expanding the set of candidate paths includes adding selected ones of the available paths having a next incrementally longer length to the set of candidate paths.

3. The method of claim 1, wherein the set of candidate paths is expanded, the expression is extended using the expanded set of candidate paths, and the SAT solver is executed on the extended expression in response to each unsatisfiable result until a stopping condition is met.

4. The method of claim 1, wherein, for each execution of the SAT solver, only candidate paths for sinks of the source-sink pairs determined to be critical are expanded.

5. The method of claim 1, wherein the expression is generated using a path-driven encoding process.

6. The method of claim 1, wherein the expression is generated using a timing-driven encoding process.

7. The method of claim 6, wherein the set of candidate paths includes nodes, wherein the variables encode delay values, and wherein each source of a source-sink pair and each node of the set of candidate paths in a routing solution has a unique delay.

8. A system for routing a circuit design for implementation within an integrated circuit, the system comprising:

a processor configured to initiate executable operations including;

determining a set of candidate paths from available paths of the integrated circuit for connecting source-sink pairs of the circuit design, wherein the set of candidate paths is initially a subset of the available paths;

generating a expression having a plurality of variables expressed as a conjunction of routing constraints representing legal routes of the source-sink pairs using only the candidate paths;

determining a routing result for the circuit design by initiating execution of a SAT solver on the expression; and

in response to the routing result indicating that the expression is not satisfiable, expanding the set of candidate paths, extending the expression using the expanded set of candidate paths, and initiating further execution of the SAT solver on the extended expression.

9. The system of claim 8, wherein the expanding the set of candidate paths includes adding selected ones of the available paths having a next incrementally longer length to the set of candidate paths.

10. The system of claim 8, wherein the set of candidate paths is expanded, the expression is extended using the expanded set of candidate paths, and the SAT solver is executed on the extended expression in response to each unsatisfiable result until a stopping condition is met.

11. The system of claim 8, wherein, for each execution of the SAT solver, only candidate paths for sinks of the source-sink pairs determined to be critical are expanded.

12. The system of claim 8, wherein the processor is configured to generate the expression using a path-driven encoding process.

13. The system of claim 8, wherein the processor is configured to generate the expression using a timing-driven encoding process.

14. The system of claim 13, wherein the set of candidate paths includes nodes, wherein the variables encode delay values, and wherein each source of a source-sink pair and each node of the set of candidate paths in a routing solution has a unique delay.

15. A computer program product comprising a computer readable storage medium having program code stored thereon for routing a circuit design for implementation within an integrated circuit, the program code executable by a processor to perform operations comprising:

determining a set of candidate paths from available paths of the integrated circuit for connecting source-sink pairs of the circuit design, wherein the set of candidate paths is initially a subset of the available paths;

generating an expression having a plurality of variables expressed as a conjunction of routing constraints representing legal routes of the source-sink pairs using only the candidate paths;

determining a routing result for the circuit design by initiating execution of a SAT solver on the expression; and

in response to the routing result indicating that the expression is not satisfiable, expanding the set of candidate paths, extending the expression using the expanded set of candidate paths, and initiating further execution of the SAT solver on the extended expression.

16. The computer program product of claim 15, wherein the expanding the set of candidate paths includes adding selected ones of the available paths having a next incrementally longer length to the set of candidate paths.

17. The computer program product of claim 15, wherein the set of candidate paths is expanded, the expression is extended using the expanded set of candidate paths, and the SAT solver is executed on the extended expression in response to each unsatisfiable result until a stopping condition is met.

18. The computer program product of claim 15, wherein, for each execution of the SAT solver, only candidate paths for sinks of the source-sink pairs determined to be critical are expanded.

19. The computer program product of claim 15, wherein the expression is generated using a path-driven encoding process.

20. The computer program product of claim 15, wherein the expression is generated using a timing-driven encoding process.