NDLI: A fast SAT solver algorithm best suited to reconfigurable hardware

Please wait, while we are loading the content...

Exploiting dynamic and partial reconfiguration for FPGAs: toolflow, architecture and system integration

REDEFIS: a system with a redefinable instruction set processor

Dynamic task binding for hardware/software reconfigurable networks

Ant colony based routing architecture for minimizing hot spots in NOCs

An ultra low-power class-AB sinh integrator

Bias circuit design for low-voltage cascode transistors

Energy aware multiple clock domain scheduling for a bit-serial, self-timed architecture

MDA-based approach for embedded software generation from a UML/MOF repository

Exploiting general coefficient representation for the optimal sharing of partial products in MCMs

Single event transients in dynamic logic

Quadratic placement for 3d circuits using z-cell shifting, 3d iterative refinement and simulated annealing

The re-definition of low power design for HPC: a paradigm shift

Formal verification for real-world designs

Asynchronous circuit design on reconfigurable devices

Infrastructure for dynamic reconfigurable systems: choices and trade-offs

Application driven traffic modeling for NoCs

Ultra low-voltage ultra low-power CMOS threshold voltage reference

A differential switched-capacitor amplifier with programmable gain and output offset voltage

Aspect-oriented design in systemC: implementation and applications

Hardware support in a middleware for distributed and real-time embedded applications

A cell library for low power high performance CMOS voltage-mode quaternary logic

A cryptography core tolerant to DFA fault attacks

Effects of digital switching noise on analog voltage references in mixed-signal CMOS ICs

High performance silicon MEMS for niche market applications

Robust low power computing in the nanoscale era

FPGA architecture for static background subtraction in real time

Mapping of image processing systems to FPGA computer based on temporal partitioning and design space exploration

Area and performance optimization of a generic network-on-chip architecture

A test chip for automatic MOSFET mismatch characterization

4GHz continuous-time bandpass delta-sigma modulator for directly high IF A/D conversion

SAEPTUM: verification of ELAN hardware specifications using the proof assistant PVS

Cache performance impacts for stack machines in embedded systems

On-line optimization of FPGA power-dissipation by exploiting run-time adaption of communication primitives

Design at high level of a robust 8-bit microprocessor to soft errors by using only standard gates

A band-pass Gm-C Filter design based on gm/ID methodology and characterization

Run-time reconfigurabilility and other future trends

Implementation of dispatching algorithms for elevator systems using reconfigurable architectures

Power constrained design optimization of analog circuits based on physical gm/ID characteristics

A general domain CMOS companding integrator

A fast SAT solver algorithm best suited to reconfigurable hardware

ByZFAD: a low switching activity architecture for shift-and-add multipliers

Evaluation of SEU and crosstalk effects in network-on-chip switches

Low maintenance verification

Fast disjoint transistor networks from BDDs

Using a software testing technique to identify registers for partial scan implementation

Razor: a low-power pipeline based on circuit-level timing speculation

Using NEXUS compliant debuggers for real time fault injection on microprocessors

A fast SAT solver algorithm best suited to reconfigurable hardware

Content Provider	ACM Digital Library
Author	Coelho, Claudionor N. Zuim, Romanelli de Sousa, José T.
Abstract	The majority of the existing reconfigurable hardware SAT solvers employ some variation of the Davis-Putnam algorithm; we propose a new algorithm for organizing the search in SAT Solvers best suited to reconfigurable architectures due to its vector-like operations. Its essence is to view each negated clause as a cube in the n-dimensional Boolean search space, and realizing that each of these clause-cubes denotes a sub-region of the search space where no satisfying assignments can be found. Starting from the universal cube, which represents the whole space, we systematically subtract all clause-cubes until we end up with a satisfying cube or an empty cube if the SAT formula is unsatisfiable. The algorithm for cube subtraction is the D-Sharp algorithm. We implemented this strategy in the well-known zChaff SAT solver. Improvements in execution time and number of aborted instances have been observed for the new algorithm. The test suite includes several instances from IBM-CNF BMC and Microprocessor's Formal Verification benchmarks. Given the breadth of the experimental software evaluation, we claim that D-Sharp subtraction search is an effective algorithm for improving the performance of SAT solvers and due to its data structure and bit-to-bit operations it is very well suited to reconfigurable hardware implementations. Design Automation (EDA).
Starting Page	131
Ending Page	136
Page Count	6
File Format	PDF
ISBN	1595934790
DOI	10.1145/1150343.1150380
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2006-08-28
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	Sat Cnf Dpll Formal verification
Content Type	Text
Resource Type	Article

Central Library (ISO-9001:2015 Certified)
Indian Institute of Technology Kharagpur
Kharagpur, West Bengal, India | PIN - 721302

See location in the Map
03222 282435
Mail: support@ndl.gov.in

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in