Equivalence Checking for Behaviorally Synthesized Pipelines

K. Hao, S. Ray, and F. Xie

In P. Groeneveld, D. Sciuto, and S. Hassoun, editors, 49th International ACM/EDAC/IEEE Design Automation Conference (DAC 2012), San Francisco, CA, USA, June 2012, pages 344-349. ACM.

© 2012 ACM, 2 Penn Plaza, Suite 701 New York, New York 10121. Permission to make digital or hard copies of portions of this work for personal or classroom use is granted without fee provided that the copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page in print or the first screen in digital media. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, to republish, to post on servers, or to redistribute to lists, requires prior specific permission and/or a fee. Send written requests for republication to ACM Publications, Copyright & Permissions at the address above or fax +1 (212) 869-0481 or email permissions@acm.org. For other copying of articles that carry a code at the bottom of the first or last page, copying is permitted provided that the per-copy fee indicated in the code is paid through the Copyright Clearance Center, 222 Rosewood Drive, Danvers, MA 01923.


Abstract

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.

Relevant files