Sciweavers

Share
DAC
2012
ACM

Equivalence checking for behaviorally synthesized pipelines

7 years 9 months ago
Equivalence checking for behaviorally synthesized pipelines
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. Categories and Subject Descriptors B.6.3 [Logic Design]: Design Aids—automatic synthesis, optimization, verification General Terms Algorithms, Performance, Reliability, Verification Keywords Equivalence checking, behavioral ...
Kecheng Hao, Sandip Ray, Fei Xie
Added 29 Sep 2012
Updated 29 Sep 2012
Type Journal
Year 2012
Where DAC
Authors Kecheng Hao, Sandip Ray, Fei Xie
Comments (0)
books