Other

Nec Usa, Inc.

Margaret Martonosi

Pranav N Ashar

Peixin Zhong

Sharad Malik

Zhen Luo

A method and apparatus for implementing communication between literals and clauses of a Boolean SAT problem through use of a time-multiplexed pipelined bus architecture rather than hardwiring it using on-FPGA routing resources. This technique allows the circuits for different instances of the Boolean SAT problem to be identical except for small local differences. Incremental synthesis and place-and-route effort required for each instance of the Boolean SAT problem becomes negligible compared to the time to actually solve the SAT problem. The time-multiplexing feature allows dynamic addition of clauses into the SAT solver algorithm. The pipeline architecture is highly pipelined with very few long wires and no wires crossing FPGA boundaries, thereby providing high clock speeds.

Method and apparatus for SAT solver architecture with very low synthesis and layout overhead

The method and apparatus for performing design rule checking on Manhattan structures in VLSI circuit layouts. The method and apparatus provides an edge-endpoint-based technique for checking the geometry and spacing of the VLSI circuit layout. The edge-endpoint-based technique uses a scanline algorithm that detects errors between adjacent structures that do not simultaneously intersect the scanline. The method also provides efficient error compilation. The apparatus allows for the design rules to be changed as the VLSI circuit layout evolves. The apparatus can process the VLSI circuit layout with a single processor, and the apparatus provides for multiple processors to process slices of the VLSI circuit layout, thereby enhancing the speed of the design rule checking over traditional software-only techniques.

Method and apparatus for edge-endpoint-based VLSI design rule checking

Disclosed is a configurable hardware system and method for implementing instance-specific (per-formula) SAT-solver circuits. A template design is provided for producing these circuits on a per-formula basis. The typical hardware requirements for implementing the invention makes the design amenable to current or next-generation FPGA implementation. Hardware simulations indicate that for many difficult SAT problems, the system according to the invention can offer one to three orders of magnitude speedup over prior art software implementations.

Configurable hardware system implementing Boolean Satisfiability and method thereof

A Boolean SAT solver uses reconfigurable hardware to solve a specific input problem. Each of the plurality of ordered variables has a corresponding one of a plurality of state machines. Each state machine has an implication circuit for its respective variable, and operates in parallel according to an identical state machine. One state machine implements the Davis-Putnam method in hardware and provides improved performance over software by virtue of the parallel checking of direct and transitive implications. Another state machine implements a novel non-chronological backtracking method that takes advantage of the parallel implication checking and avoids the need to maintain or to traverse a GRASP type implication graph in the event of backtracking. The novel non-chronological backtracking provides for setting a blocking variable as a leaf variable and for changing only the value of the leaf variable, but possibly changing both the value and identity of a backtracking variable.

Growing community of inventors

Princeton, NJ, United States of America

Margaret Martonosi