SE3: Sequential Equivalence Checking for Non-Cycle-Accurate Design Transformations †
SE3: Sequential Equivalence Checking for Non-Cycle-Accurate Design Transformations †
复制标题
SE3：非周期精确设计转换的顺序等价检查 †
DOI：
10.1109/dac56929.2023.10247912
复制
发表时间：
2023
期刊：
影响因子：
--
通讯作者：
H. Zhou
中科院分区：
文献类型：
--
作者：
You Li;Guannan Zhao;Yunqi He;H. Zhou
在高级设计探索中，许多有用的优化将电路转换为具有不同操作周期的另一个电路，以便在性能和资源使用之间进行更好的权衡。如何有效地检查它们的等价性是关键和具有挑战性的，因为大多数现有的等价检查器是为周期精确电路设计的。本文介绍了SE 3，一个有效的顺序等价检查没有假设的周期精度，锁存器映射，或I/O接口的检查电路。它通过计算两个电路的状态之间的等价关系来证明两个电路的等价性，并利用语法抽象来加速这个过程。实验结果表明，SE 3是显着快于国家的最先进的顺序等价性检查算法。
In high-level design explorations, many useful optimizations transform a circuit into another with different operating cycles for a better trade-off between performance and resource usage. How to efficiently check their equivalence is critical and challenging since most existing equivalence checkers are designed for cycle-accurate circuits. This paper presents SE3, an efficient sequential equivalence checker without assumption on cycle-accuracy, latch mapping, or I/O interface of the checked circuits. It proves the equivalence of two circuits by computing an equivalence relation between the states of the two circuits and utilizes syntax abstraction to accelerate this process. Experimental results show that SE3 is significantly faster than state-of-the-art sequential equivalence checking algorithms.
DOI：
10.1145/3489517.3530585
发表时间：
2022-07
期刊：
Proceedings of the 59th ACM/IEEE Design Automation Conference
影响因子：
--
作者：
Hongwu Peng;Shaoyi Huang;Shiyang Chen;Bingbing Li;Tong Geng;Ang Li;Weiwen Jiang;Wujie Wen;J. Bi;Hang Liu;Caiwen Ding
通讯作者：
Hongwu Peng;Shaoyi Huang;Shiyang Chen;Bingbing Li;Tong Geng;Ang Li;Weiwen Jiang;Wujie Wen;J. Bi;Hang Liu;Caiwen Ding
DOI：
10.23919/fmcad.2019.8894295
发表时间：
2019-10
期刊：
2019 Formal Methods in Computer Aided Design (FMCAD)
影响因子：
--
作者：
Luca Piccolboni;G. D. Guglielmo;L. Carloni
通讯作者：
Luca Piccolboni;G. D. Guglielmo;L. Carloni