Equivalence checking for behaviorally synthesized pipelines


== 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.


== Original document ==

The different versions of the original document can be found in:

* [http://web.cecs.pdx.edu/~xie/pubs/ec4bsp.pdf http://web.cecs.pdx.edu/~xie/pubs/ec4bsp.pdf]

* [https://dblp.uni-trier.de/db/conf/dac/dac2012.html#HaoRX12 https://dblp.uni-trier.de/db/conf/dac/dac2012.html#HaoRX12],
: [http://web.cecs.pdx.edu/~xie/pubs/ec4bsp.pdf http://web.cecs.pdx.edu/~xie/pubs/ec4bsp.pdf],
: [http://core.ac.uk/display/23541377 http://core.ac.uk/display/23541377],
: [http://yadda.icm.edu.pl/yadda/element/bwmeta1.element.ieee-000006241531 http://yadda.icm.edu.pl/yadda/element/bwmeta1.element.ieee-000006241531],
: [https://doi.acm.org/10.1145/2228360.2228423 https://doi.acm.org/10.1145/2228360.2228423],
: [https://dl.acm.org/citation.cfm?id=2228360.2228423 https://dl.acm.org/citation.cfm?id=2228360.2228423],
: [https://academic.microsoft.com/#/detail/2108124319 https://academic.microsoft.com/#/detail/2108124319]

* [http://dl.acm.org/ft_gateway.cfm?id=2228423&amp;ftid=1223143&amp;dwn=1 http://dl.acm.org/ft_gateway.cfm?id=2228423&amp;ftid=1223143&amp;dwn=1],
: [http://dx.doi.org/10.1145/2228360.2228423 http://dx.doi.org/10.1145/2228360.2228423]