Title :
A bitstream reconfigurable FPGA implementation of the WSAT algorithm
Author :
Leong, P.H.W. ; Sham, C.W. ; Wong, W.C. ; Wong, H.Y. ; Yuen, W.S. ; Leong, M.P.
Author_Institution :
Dept. of Comput. Sci. & Eng., Chinese Univ. of Hong Kong, Shatin, China
Abstract :
A field programmable gate array (FPGA) implementation of a coprocessor which uses the WSAT algorithm to solve Boolean satisfiability problems is presented. The input is a SAT problem description file from which a software program directly generates a problem-specific circuit design which can be downloaded to a Xilinx Virtex FPGA device and executed to find a solution. On an XCV300, problems of 50 variables and 170 clauses can be solved. Compared with previous approaches, it avoids the need for resynthesis, placement, and routing for different constraints. Our coprocessor is eminently suitable for embedded applications where energy, weight and real-time response are of concern.
Keywords :
constraint theory; coprocessors; field programmable gate arrays; reconfigurable architectures; Boolean satisfiability; WSAT algorithm; XCV300; Xilinx Virtex device; bitstream reconfigurable architecture; circuit design; constraint satisfaction problem; coprocessor; description file; field programmable gate array; software program; Algorithm design and analysis; Boolean functions; Circuit synthesis; Circuit testing; Computer science; Coprocessors; Field programmable gate arrays; Hardware; Real time systems; Routing;
Journal_Title :
Very Large Scale Integration (VLSI) Systems, IEEE Transactions on
