METHOD AND APPARATUS FOR IMPROVING BOOLEAN SATISFIBILITY SOLVER GENERATED BASED ON INPUT DESIGN WITH DATA QUALIFIER SIGNALS
First Claim
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 Assignments
0 Petitions
Accused Products
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.
-
Citations
18 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. - View Dependent Claims (2, 3, 4, 5, 6)
-
-
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. - View Dependent Claims (8, 9, 10, 11, 12)
-
-
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. - View Dependent Claims (14, 15, 16, 17, 18)
-
Specification