Name
Abstract | ||
|---|---|---|
FPGA-based SAT solvers have the potential to dramatically accelerate SAT solving by effectively exploiting finegrained pipeline parallelism in a manner which is not achievable with regular processors. Previous hardware-based approaches have relied on on-chip memory resources to store data which, similar to a CPU cache, are very fast, but are also very limited in size. For hardware-based SAT approaches to scale to real-world instances, it is necessary to utilise large amounts of off-chip memory. We present novel techniques for storing and retrieving SAT clauses using a custom multi-port memory interface to off-chip DRAM which is connected to a processor core implemented on a medium sized FPGA on the BEE3 system. Since DRAM is slower than on-chip memory resources, the parallelisation which can be achieved is limited by memory throughput. We present the design and implementation of a new parallel architecture that tackles this problem and estimate the performance of our approach with memory benchmarks. |
Year | Venue | Keywords |
|---|---|---|
2010 | Formal Methods in Computer-Aided Design | off-chip memory,memory benchmarks,retrieving sat clause,relieving capacity limit,on-chip memory resource,fpga-based sat-solvers,hardware-based sat,fpga-based sat solvers,present novel technique,custom multi-port memory interface,previous hardware-based approach,memory throughput,field programmable gate arrays,system on a chip,hardware,chip,memory management,sat solver,processor core,computability |
Field | DocType | ISBN |
Registered memory,Interleaved memory,Uniform memory access,CPU cache,Computer science,Parallel computing,Cache-only memory architecture,Static random-access memory,Memory management,Flat memory model | Conference | 978-0-9835678-0-6 |
Citations | PageRank | References |
4 | 0.44 | 13 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Leopold Haller | 1 | 127 | 6.93 |
| Satnam Singh | 2 | 571 | 59.08 |