Scipediacontent: Scipediacontent moved page Draft Content 622930441 to Xie et al 2012a

2021-01-28T17:28:22Z

Scipediacontent moved page Draft Content 622930441 to Xie et al 2012a

Scipediacontent: Created page with " == Abstract == Loop pipelining is a critical transformation in behavioral synthesis. It is crucial to producing hardware designs with acceptable latency and throughput. Howe..."

2021-01-28T17:28:18Z

Created page with " == Abstract == Loop pipelining is a critical transformation in behavioral synthesis. It is crucial to producing hardware designs with acceptable latency and throughput. Howe..."

New page

== 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&ftid=1223143&dwn=1 http://dl.acm.org/ft_gateway.cfm?id=2228423&ftid=1223143&dwn=1],
: [http://dx.doi.org/10.1145/2228360.2228423 http://dx.doi.org/10.1145/2228360.2228423]

← Older revision	Revision as of 17:28, 28 January 2021
(No difference)

Xie et al 2012a - Revision history

Scipediacontent: Scipediacontent moved page Draft Content 622930441 to Xie et al 2012a

Scipediacontent: Created page with " == Abstract == Loop pipelining is a critical transformation in behavioral synthesis. It is crucial to producing hardware designs with acceptable latency and throughput. Howe..."