logic - 逻辑综合和验证资源

Question

我目前正在研究逻辑综合——给出硬件的高级描述，我希望将其转换为门电路、触发器等。我对这个理论不太熟悉。我搜索了互联网，但大多数都是指在线书店。

有人可以请我参考网上任何好的教程吗？任何有关它的帮助将不胜感激。

Answer 1

可在此处找到流程入门：
Himanshu Bhatnagar 的使用 Synopsys® Design Compiler® Physical Compiler® 和 PrimeTime® 的高级 ASIC 芯片合成。

它是一本旧书，所以那里可能有更新的东西。

可在Google Books和Amazon上找到。

如果您想要一些简单的原型制作使用 PAL 或 FPGA，则实施这些东西适用于大公司。请参阅 Altera、Xilinx 和类似产品。

大多数大学都可以使用这些或类似的工具。

Answer 2

我在海法大学的 Nadav Rotem 的2010 LLVM Developers' Meeting上找到了相关的演示文稿，标题为“C-to-Verilog.com : High-level synthesis using LLVM”。我认为值得看看他关于演示的想法（幻灯片在这里）。

我只知道一点，但关于那些东西，但试着用谷歌搜索那个人，或者电子邮件作者，他可能是个好人问。

Answer 3

与这些东西相关的基础知识怎么样，试试 Thomas H. Cormen、Charles E. Leiserson、Ronald L. Rivest、Clifford Stein 的“算法简介”。

一些算法与电路、硬件设计有关，如排序网络、算术电路、逻辑电路的可满足性。

我没有深入研究“逻辑综合”，所以这个答案仅基于直觉，与上述主题相关的算法知识可能会有用。

Answer 4

要了解逻辑综合的最新进展，请查看最近的设计自动化会议 (DAC) 和国际计算机辅助设计会议 (ICCAD) 会议记录中的相关论文。

现代逻辑综合工具支持基于多数门的“特定领域”数据结构（和算法），例如多数逆变器图 (MIG)、异或与图 (XAG) 和异或多数图 (XMG)。见https://doi.org/10.1145/3316781.3317905。

请参阅https://github.com/lsils/lstools-showcase，了解来自瑞士洛桑的 EPFL（洛桑联邦理工学院）最先进的逻辑综合库。

一个不太现代的解决方案是来自加州大学伯克利分校的“ABC”。它基于 AND 逆变器图 (AIG)。见https://people.eecs.berkeley.edu/~alanmi/abc/。不幸的是，关于电子设计自动化的书籍只提供了一个章节，如果不是一章的话。优化 AIG 的大多数参考文献是会议（和期刊）论文，或来自研究会议（尤其是 DAC 和 ICCAD，可能还有 DATE - 欧洲设计、自动化和测试会议）和研究期刊（尤其是来自 ACM 和IEEE）。

以下是一些 BibTeX 条目，它们提供了对您有帮助的书籍信息。

对于现代逻辑综合...

@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}}

对于基于二元决策图 (BDD) 的有些陈旧的逻辑综合...

@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}

评论文章、调查论文/“论文”和文献评论：

@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}}

“用于已建立和新兴计算的逻辑综合”文献综述论文（DOI：https ://doi.org/10.1109/JPROC.2018.2869760 ）。

基于 BDD 和 ESPRESSO 的其他东西已经过时了。