Equivalence checking for behaviorally synthesized pipelines
Equivalence checking for behaviorally synthesized pipelines
复制标题
行为综合管道的等效性检查
DOI：
10.1145/2228360.2228423
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
Fei Xie
中科院分区：
文献类型：
--
作者：
K. Hao;S. Ray;Fei Xie
循环流水线是行为综合中的一个关键转换。这对于生产具有可接受的延迟和吞吐量的硬件设计至关重要。然而，这是一个复杂的转换，涉及积极的调度策略，高吞吐量和仔细的控制生成，以消除危险。我们提出了一个等价性检查的方法来验证合成的硬件设计中存在的流水线变换。我们的方法的工作原理是（1）构造一个可证明正确的流水线参考模型从顺序规格说明，（2）应用顺序等价性检查之间的参考模型和合成RTL。我们证明了我们的方法的可扩展性，从商业合成工具的几个合成设计。
Loop pipelining is a critical transformation in behavioral synthesis. It is crucial to producing hardware designs with acceptable latency and throughput. However, it is a complex transformation involving aggressive scheduling strategies for high throughput and careful control generation to eliminate hazards. We present an equivalence checking approach for certifying synthesized hardware designs in the presence of pipelining transformations. Our approach works by (1) constructing a provably correct pipeline reference model from sequential specification, and (2) applying sequential equivalence checking between this reference model and synthesized RTL. We demonstrate the scalability of our approach on several synthesized designs from a commercial synthesis tool.