Equivalence Checking for Behaviorally Synthesized Pipelines

被引：0

作者：

Hao, Kecheng ^{[1
]}

Ray, Sandip ^{[2
]}

Xie, Fei ^{[1
]}

机构：

[1] Portland State Univ, Dept Comp Sci, Portland, OR 97207 USA

[2] Univ Texas Austin, Dept Comp Sci, Austin, TX 78712 USA

来源：

2012 49TH ACM/EDAC/IEEE DESIGN AUTOMATION CONFERENCE (DAC) | 2012年

基金：

美国国家科学基金会;

关键词：

Equivalence checking; behavioral synthesis; pipeline;

D O I：

暂无

中图分类号：

TM [电工技术]; TN [电子技术、通信技术];

学科分类号：

0808 ; 0809 ;

摘要：

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.

引用

页码：344 / 349

页数：6