METHOD AND APPARATUS FOR IMPROVING BOOLEAN SATISFIBILITY SOLVER GENERATED BASED ON INPUT DESIGN WITH DATA QUALIFIER SIGNALS

• US 20190318056A1
• Filed: 04/16/2018
• Published: 10/17/2019
• Est. Priority Date: 04/16/2018
• Status: Active Grant

• Current Assignee: Mellanox Technologies Limited (NVIDIA Corporation)
• Original Assignee: Mellanox Technologies Limited (NVIDIA Corporation)
• Inventors: MELLER, Yael, DAVIDI, Or, ARMONI, Roy
• Granted Patent: US 10,635,845 B2
• Time in Patent Office: Days
• CPC Class Codes: G06F 2111/10 Numerical modelling
• CPC Class Codes: G06F 30/30 Circuit design
• CPC Class Codes: G06F 30/3323 using formal methods, e.g. equivalence checking or property checking

Abstract

Embodiments are disclosed for solving a Boolean formula generated from an input design using an iterative loop using a computer-implemented Boolean satisfiability solver. An example method includes accessing data qualifier signals indicating one or more variables in a Boolean formula. The example method further includes marking the one or more variables in the Boolean formula as data qualifier variables based on the respective data qualifier signals. The example method further includes instructing a computer implemented Boolean satisfiability solver to solve the Boolean formula using an iterative loop, where operation of the iterative loop is prioritized based on the data qualifier variables. Corresponding apparatuses and non-transitory computer readable storage media are also provided.

Claims

1. A computer implemented method for solving a Boolean formula generated from a design using an iterative loop using a Boolean satisfiability solver, comprising:

accessing data qualifier signals indicating one or more variables in a Boolean formula;

marking the one or more variables in the Boolean formula as data qualifier variables based on the respective data qualifier signals; and

instructing a computer implemented Boolean satisfiability solver to solve the Boolean formula using an iterative loop, wherein operation of the iterative loop is prioritized based on the data qualifier variables.

2. The method of claim 1, wherein the Boolean formula is translated from a gate-level model graph, and wherein the one or more variables in the Boolean formula correspond to a set of elements in the gate-level model graph.

3. The method of claim 2, wherein the one or more data qualifier signals are associated with the set of elements in the gate-level model graph.

4. The method of claim 2, wherein the gate-level model graph is translated from an input circuit design and wherein the set of elements in the gate-level model graph correspond to a set of elements in the input circuit design.

5. The method of claim 4, wherein the data qualifier signals are associated with on the set of elements in the input circuit design.

6. The method of claim 1, wherein the data qualifier signals are generated by:

receiving, via a control interface, user input identifying one or more data qualifier elements in an input design;

translating the input design to a Boolean formula, wherein one or more variables in the Boolean formula correspond to the one or more data qualifier elements in the input design;

identifying the one or more variables in the Boolean formula that correspond to the one or more data qualifier elements in the input design; and

generating data qualifier signals indicating the one or more variables in the Boolean formula that correspond to the one or more data qualifier elements in the input design.

7. An apparatus comprising at least one processor and at least one memory including computer program code, the at least one memory and the computer program code configured to, with the at least one processor, solve a Boolean formula generated from an input design by causing the apparatus to at least:

receive data qualifier signals indicating one or more variables in a Boolean formula;

mark the one or more variables in the Boolean formula as data qualifier variables based on the respective data qualifier signals; and

instruct a computer implemented Boolean satisfiability solver to solve the Boolean formula using an iterative loop, wherein operation of the iterative loop is prioritized based on the data qualifier variables.

8. The apparatus of claim 7, wherein the Boolean formula is translated from a gate-level model graph, and wherein the one or more variables in the Boolean formula correspond to a set of elements in the gate-level model graph.

9. The apparatus of claim 8, wherein the one or more data qualifier data qualifier signals are associated with the set of elements in the gate-level model graph.

10. The apparatus of claim 8, wherein the gate-level model graph is translated from an input circuit design and wherein the set of elements in the gate-level model graph correspond to a set of elements in the input circuit design.

11. The apparatus of claim 10, wherein the data qualifier signals are associated with the set of elements in the input circuit design.

12. The apparatus of claim 7, wherein the data qualifier signals are generated by:

accessing, via a control interface, user input identifying one or more data qualifier elements in an input design;

translating the input design to a Boolean formula, wherein one or more variables in the Boolean formula correspond to the one or more data qualifier elements in the input design;

identifying the one or more variables in the Boolean formula that correspond to the one or more data qualifier elements in the input design; and

generating data qualifier signals indicating the one or more variables in the Boolean formula that correspond to the one or more data qualifier elements in the input design.

13. A computer program product comprising at least one non-transitory computer readable storage medium, the non-transitory computer readable storage medium storing instructions that, when executed by a processor, cause the processor to configure an apparatus to at least:

receive data qualifier signals indicating one or more variables in a Boolean formula;

mark the one or more variables in the Boolean formula as data qualifier variables based on the respective data qualifier signals; and

instruct a computer implemented Boolean satisfiability solver to solve the Boolean formula using an iterative loop, wherein operation of the iterative loop is prioritized based on the data qualifier variables.

14. The computer program product of claim 13, wherein the Boolean formula is translated from a gate-level model graph, and wherein the one or more variables in the Boolean formula correspond to a set of elements in the gate-level model graph.

15. The computer program product of claim 14, wherein the one or more data qualifier data qualifier signals are associated with the set of elements in the gate-level model graph.

16. The computer program product of claim 14, wherein the gate-level model graph is translated from an input circuit design and wherein the set of elements in the gate-level model graph correspond to a set of elements in the input circuit design.

17. The computer program product of claim 16, wherein the data qualifier signals are determined based on the set of elements in the input circuit design.

18. The computer program product of claim 13, wherein the data qualifier signals are generated by:

receiving, via a control interface, user input identifying one or more data qualifier elements in an input design;

translating the input design to a Boolean formula, wherein one or more variables in the Boolean formula correspond to the one or more data qualifier elements in the input design;

identifying the one or more variables in the Boolean formula that correspond to the one or more data qualifier elements in the input design; and

generating data qualifier signals indicating the one or more variables in the Boolean formula that correspond to the one or more data qualifier elements in the input design.