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

Volume

9

Issue

1

fYear

2001

Firstpage

197

Lastpage

201

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;

fLanguage

English

Journal_Title

Very Large Scale Integration (VLSI) Systems, IEEE Transactions on

Publisher

ieee

ISSN

1063-8210

Type

jour

DOI

10.1109/92.920833

Filename

920833