This paper introduces a novel approach for solving the Boolean satisfiability (SAT) problem by combining software and configurable hardware. The suggested technique avoids instance-specific hardware compilation and, as a result, allows the total problem solving time to be reduced compared to other approaches that have been proposed. Moreover, the technique permits problems that exceed the resources of the available reconfigurable hardware to be solved. The paper presents the results obtained with some of the DIMACS benchmarks and a comparison of our implementation with other available SAT solvers based on reconfigurable hardware. The hardware part of the satisfier was realized on Virtex XCV812E FPGA, which has a large volume of embedded memory blocks that provide direct support for the proposed approach.

This letter analyses and compares on-chip interfaces for hardware/software communications in the Zynq-7000 all programmable systems-on-chip. Many experiments were carried out to evaluate the exchange of data between the processing system and the programmable logic through general-purpose and high-performance ports; the experiments were conducted for both standalone and Linux applications. The results enable the most effective interfaces for specific types of data to be identified and the effectiveness of Zynq-based hardware accelerators to be assessed.

The paper describes the hardware implementation and optimization of parallel recursive algorithms that sort data using binary trees. Since recursive calls are not directly supported by hardware description languages, they are implemented using the model of a hierarchical finite state machine (HFSM). Parallel processing is achieved by constructing N binary trees (N>;1) and applying concurrent sorting to N trees at the same time with the aid of N communicating HFSMs. The paper presents new results in: 1) parallel sorting algorithms, 2) FPGA-based parallel architectures, and 3) the analysis and comparison of alternative and competitive techniques for implementing parallel recursive algorithms. Experiments demonstrate that the performance of sorting operations is increased compared to previous implementations.