Resources for logic synthesis and verification

I am currently working on logic synthesis- given a high level descri开发者_C百科ption of a hardware I wish to convert it into a circuit of gates,flip flops etc. I am not very much familiar with the theory. I searched the internet, but most of them refer to online book stores.

Could someone please refer me to any good tutorials on the net? Any help regarding it would be appreciated.

A flow primer can be found here:
Advanced ASIC Chip Synthesis Using Synopsys® Design Compiler® Physical Compiler® and PrimeTime® by Himanshu Bhatnagar.

Its an old book so there is probably something newer out there.

Available on Google Books and Amazon.

Implementing these things are for large companies if you want some thing simple for prototyping use a PAL or FPGA. See Altera, Xilinx and similar.

Most universities have access to these or similar tools.

I've found related presentation at 2010 LLVM Developers' Meeting , titled "C-to-Verilog.com : High-level synthesis using LLVM" by Nadav Rotem from Haifa University. I think it's worth to check out his ideas on presentation (slides here ).

I know just a little but about that stuff, but try to google that guy, or e-mail author, he might be a good person to ask.

What about basics, related to this stuff, try "Introduction to Algorithms" by Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, Clifford Stein.

Some of algorithms are related to circuits, hardware design, like sorting networks, arithmetical circuits, satisfiability of logical circuits.

I am not digged into "logic synthesis", so this answer is based only on intuition, that knowledge of algorithms related to above topic might be useful.

To learn about state-of-the-art advances in logic synthesis, check out the relevant papers from the recent proceedings of the Design Automation Conference (DAC) and International Conference on Computer-Aided Design (ICCAD).

Modern logic synthesis tools support "domain-specific" data structures (and algorithms) based on majority gates, such as majority-inverter graphs (MIGs), XOR-AND graphs (XAG), and XOR-majority graphs(XMG). See https://doi.org/10.1145/3316781.3317905.

See https://github.com/lsils/lstools-showcase for the state-of-the-art logic synthesis libraries from EPFL (Ecole Polytechnique Fédérale de Lausanne) in Lausanne, Switzerland.

A not-so-modern solution is "ABC" from the University of California, Berkeley. It is based on AND-Inverter Graphs (AIGs). See https://people.eecs.berkeley.edu/~alanmi/abc/. Unfortunately, books about electronic design automation only provide a section, if not a chapter, about this. Most references for optimizing AIGs are conference (and journal) papers, or papers/articles from proceedings of research conferences (especially DAC and ICCAD, and maybe DATE - Design, Automation, and Test in Europe conference) and research journals (especially from ACM and IEEE).

Here are some BibTeX entries that provide information about books that can be helpful for you.

For modern logic synthesis...

@book{Reis2018,
    Address = {Cham, Switzerland},
    Author = {Andr{\'{e}} In{\'{a}}cio Reis and Rolf Drechsler},
    Doi = {https://dx.doi.org/10.1007/978-3-319-67295-3},
    Publisher = {Springer International Publishing {AG}},
    Title = {Advanced Logic Synthesis},
    Year = {2018}}

@book{Amaru2017,
    Address = {Cham, Switzerland},
    Author = {Luca Gaetano Amaru},
    Doi = {https://dx.doi.org/10.1007/978-3-319-43174-1},
    Publisher = {Springer International Publishing Switzerland},
    Title = {New Data Structures and Algorithms for Logic Synthesis and Verification},
    Volume = {},
    Year = {2017}}

@phdthesis{Amaru2015,
    Address = {Lausanne, Switzerland},
    Author = {Luca Gaetano Amar{\`{u}}},
    Doi = {https://dx.doi.org/10.5075/epfl-thesis-6863},
    Howpublished = {Available online at: \url{https://dx.doi.org/10.5075/epfl-thesis-6863}; December 8, 2017 was the last accessed date},
    Month = {December 18},
    School = {Swiss Federal Institute of Technology in Lausanne},
    Title = {New Data Structures and Algorithms for Logic Synthesis and Verification},
    Url = {https://dx.doi.org/10.5075/epfl-thesis-6863},
    Year = {2015}}

For somewhat-old logic synthesis based on binary decision diagrams (BDDs)...

@book{Ebendt2005,
    Address = {Dordrecht, {The Netherlands}},
    Author = {R{\"{u}}diger Ebendt and G{\"{o}}rschwin Fey and Rolf Drechsler},
    Doi = {https://dx.doi.org/10.1007/b107399},
    Publisher = {Springer},
    Title = {Advanced {BDD} Optimization},
    Year = {2005}}

@book{Hachtel1996,
    Address = {New York, {NY}},
    Author = {Hachtel, Gary D. and Somenzi, Fabio},
    Doi = {https://dx.doi.org/10.1007/0-387-31005-3},
    Publisher = {Springer Science+Business Media, {LLC}},
    Title = {Logic Synthesis and Verification Algorithms},
    Url = {https://dx.doi.org/10.1007/0-387-31005-3},
    Year = {1996}}

@book{DeMicheli1994,
    Address = {New York, {NY}},
    Author = {{De Micheli}, Giovanni},
    Publisher = {McGraw-Hill},
    Series = {McGraw-Hill Series in Electrical and Computer Engineering},
    Title = {Synthesis and Optimization of Digital Circuits},
    Year = {1994}}

@book{Hassoun2002,
    Address = {Norwell, {MA}},
    Author = {Hassoun, Soha and Sasao, Tsutomu},
    Doi = {https://dx.doi.org/10.1007/978-1-4615-0817-5},
    Publisher = {Kluwer Academic Publishers},
    Series = {The Kluwer International Series in Engineering and Computer Science},
    Title = {Logic Synthesis and Verification},
    Url = {https://dx.doi.org/10.1007/978-1-4615-0817-5},
    Year = {2002}

Review articles, survey papers/"papers", and literature reviews:

@book{Lavagno2016a,
    Address = {Boca Raton, {FL}},
    Author = {Luciano Lavagno and Igor L. Markov and Grant Martin and Louis K. Scheffer},
    Doi = {https://dx.doi.org/10.1201/b19569},
    Edition = {Second},
    Publisher = {{CRC} Press},
    Series = {Electronic Design Automation for Integrated Circuits Handbook},
    Title = {Electronic Design Automation for {IC} System Design, Verification, and Testing},
    Volume = {1},
    Year = {2016}}

The "Logic Synthesis for Established and Emerging Computing" literature review paper (DOI:https://doi.org/10.1109/JPROC.2018.2869760).

The other stuff based on BDDs and ESPRESSO are outdated.