逻辑综合和验证资源

Question

我目前正在从事逻辑综合工作-给定一个硬件的高级描述，我希望将其转换为门电路、触发器等。

我对这个理论不是很熟悉。我搜索了互联网，但大部分都是在线书店的参考资料。

请问有没有人能够向我推荐一些好的网络教程？任何关于此方面的帮助都将不胜感激。

- Adwaitvedant

Answer 1

这里有一份流程入门资料：
《Advanced ASIC Chip Synthesis Using Synopsys® Design Compiler® Physical Compiler® and PrimeTime®》作者：Himanshu Bhatnagar。

这是一本旧书，可能有更新的版本。

在Google Books和Amazon上都可以找到。

如果你想要实现这些内容，需要大公司来完成。如果你只是为了原型设计而需要简单的东西，请使用PAL或FPGA。请参见Altera、Xilinx等类似公司。

大多数大学都有这些或类似工具的访问权限。

- oldman

Answer 2

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

现代逻辑综合工具支持基于大多数门的“领域特定”数据结构(和算法)，如大多数反相图(MIGs)，XOR-AND图(XAG)和XOR-大多数图(XMG)。详见https://doi.org/10.1145/3316781.3317905。

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

一个不太现代的解决方案是来自加州大学伯克利分校的“ABC”。它基于AND-Inverter图（AIGs）。请参见https://people.eecs.berkeley.edu/~alanmi/abc/。不幸的是，关于电子设计自动化的书籍只提供了一节，如果不是一章，关于这个问题。优化AIGs的大多数参考资料都是会议（和期刊）论文，或者来自研究会议（特别是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的其他内容已经过时。

- Giovanni

Answer 3

我在2010 LLVM开发者会议上找到了相关的演示文稿，题为“使用LLVM进行高级综合的C-to-Verilog.com”由Haifa大学的Nadav Rotem所作。我认为值得查看他在演示（幻灯片在此）中的想法。

我对这方面知之甚少，但可以尝试谷歌一下这个人，或给作者发电子邮件，他可能是一个很好的咨询对象。

- Grzegorz Wierzowiecki

Answer 4

关于基础知识，可以尝试阅读Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, Clifford Stein所著的《算法导论》。

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

我没有深入研究“逻辑综合”，因此这个答案仅基于直觉，认为了解与上述主题相关的算法可能会有用。

- Grzegorz Wierzowiecki