数据通路设计中流水线化嵌套循环的自动形式等价验证
硬件体系结构
2017-12-29 v1
摘要
在本文中，我们提出一种高效的形式化方法，用于在存在流水线变换的情况下检查综合后RTL与高层规约之间的等价性。为提高所提方法的可扩展性，我们通过引入割点将设计动态划分为若干称为段的小部分。随后我们采用模Horner展开图（M-HED）来检查规约与实现是否等价。我们以迭代方式对每一段执行等价性检查。在每一步中，移除等价节点以及对其有影响的那些节点，直至覆盖整个设计。我们所提方法使我们能够处理行为综合设计（即便存在嵌套循环的流水线）的等价检查问题。实证结果表明，对于由商用行为综合工具综合的若干大型设计，所提方法在运行时间与内存占用方面具有效率与可扩展性。与基于SMT和SAT的等价检查相比，内存占用与运行时间的平均改进分别为16.7倍和111.9倍。
引用
@article{arxiv.1712.09818,
title = {Automated Formal Equivalence Verification of Pipelined Nested Loops in Datapath Designs},
author = {Payman Behnam and Bijan Alizadeh and Sajjad Taheri},
journal= {arXiv preprint arXiv:1712.09818},
year = {2017}
}
备注
14 pages, 20 figures