逻辑综合和验证资源答案

【问题标题】：Resources for logic synthesis and verification逻辑综合和验证资源
【发布时间】：2011-06-08 13:39:45
【问题描述】：

我目前正在研究逻辑综合——给出硬件的高级描述，我希望将其转换为门电路、触发器等。我对这个理论不是很熟悉。我在网上搜了一下，大部分都是网上书店。

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

【问题讨论】：

标签： logic synthesis

【解决方案1】：

可在此处找到流式底漆：
使用 Himanshu Bhatnagar 的 Synopsys® Design Compiler® Physical Compiler® 和 PrimeTime® 进行高级 ASIC 芯片综合。

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

在Google Books 和Amazon 上可用。

如果您希望使用 PAL 或 FPGA 进行简单的原型设计，那么实施这些东西适用于大公司。请参阅 Altera、Xilinx 和类似产品。

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

【讨论】：

【解决方案2】：

我在 2010 LLVM Developers' Meeting 找到了相关的演示文稿，标题为“C-to-Verilog.com：使用 LLVM 的高级合成”，作者是海法大学的 Nadav Rotem。我认为值得在presentation (slides here) 上查看他的想法。

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

【讨论】：

【解决方案3】：

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

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

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

【讨论】：

【解决方案4】：

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

现代逻辑综合工具支持基于多数门的“特定领域”数据结构（和算法），例如多数逆变器图 (MIG)、XOR-AND 图 (XAG) 和 XOR-多数图 (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 的东西已经过时了。

【讨论】：