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