Publication detail

A Synthesis of Reversible Digital Circuits to Solve the Boolean Satisfiability

ŠŤÁVA, M.

Original Title

A Synthesis of Reversible Digital Circuits to Solve the Boolean Satisfiability

Type

conference paper

Language

English

Original Abstract

The paper presents a methodology of synthesising the reversible digital circuits that solve the Boolean satisfiability (SAT). There is a full range of applications of such circuits; for example, accelerating SAT solvers, generating compacted tests for the sequential circuits designed for testability (with a scan chain), producing a set of results for the relation inverse to combinational functions, generating input vectors of a circuit from output ones, etc. Further, compacted representation of functions, and the straightforward and reverse approaches to obtain responses are discussed. The methodology comprises a few rules to synthesise a combinational function (circuit) into a reversible circuit in a way to implement them into FPGAs. A method of shortening the truth table for implementation in an FPGA is presented and the architecture of reversible circuits is described. The experimental data and features of the physical implementation of the circuits reverse to the ISCAS’85 benchmarks are presented for Xilinx FPGA Spartan 2E – the area overhead and computing complexity of generating the first valid input vector. The experiments show that both the features have asymptotically polynomial complexity.

Keywords

Boolean satisfiability; reversible circuits; VLSI; FPGA; combinational circuit

Authors

ŠŤÁVA, M.

Released

24. 9. 2020

Publisher

Springer Science

ISBN

978-981-15-5545-9

Book

Lecture Notes in Electrical Engineering

ISBN

1876-1100

Periodical

Lecture notes in Electrical Engineering

Year of study

673

State

United Kingdom of Great Britain and Northern Ireland

Pages from

233

Pages to

246

Pages count

14

URL

https://www.scopus.com/record/display.uri?eid=2-s2.0-85092094569&origin=resultslist&sort=plf-f&src=s&st1=boolean+satisfiability&st2=&sid=e25bcdaf87ef4bc2eced1790a94cd2ed&sot=b&sdt=b&sl=29&s=TITLE%28boolean+satisfiability%29&relpos=0&citeCnt=0&searchTerm=

BibTex

@inproceedings{BUT156422,
  author="Martin {Šťáva}",
  title="A Synthesis of Reversible Digital Circuits to Solve the Boolean Satisfiability",
  booktitle="Lecture Notes in Electrical Engineering",
  year="2020",
  journal="Lecture notes in Electrical Engineering",
  volume="673",
  pages="233--246",
  publisher="Springer Science",
  doi="10.1007/978-981-15-5546-6\{_}19",
  isbn="978-981-15-5545-9",
  issn="1876-1100",
  url="https://www.scopus.com/record/display.uri?eid=2-s2.0-85092094569&origin=resultslist&sort=plf-f&src=s&st1=boolean+satisfiability&st2=&sid=e25bcdaf87ef4bc2eced1790a94cd2ed&sot=b&sdt=b&sl=29&s=TITLE%28boolean+satisfiability%29&relpos=0&citeCnt=0&searchTerm="
}