Using ACL2 to Verify Loop Pipelining in Behavioral Synthesis
The work
| Authors | Disha Puri; Sandip Ray; Kecheng Hao; Fei Xie |
|---|---|
| Editors | Freek Verbeek; Julien Schmaltz |
| Type | inproceedings |
| Year | 2014 |
| Citekey | puri2014using |
Where it appeared
| Published in | ACL2 Theorem Prover and its Applications (ACL2 2014) |
|---|---|
| Series | EPTCS |
| Volume | 152 |
| Pages | 111--128 |
Identifiers
| arXiv | 1406.1562 from its landing_page_url |
|---|---|
| DOI | 10.4204/eptcs.152.10 |
Access
| Landing page | https://arxiv.org/abs/1406.1562 |
|---|
Related
| Distinct from | baty2024formal |
|---|---|
| Distinct from | jacobi2005automatic |
| Distinct from | kurze2026nocout |
| Distinct from | nukala2024translating |
| Distinct from | oleary2013relational |
| Distinct from | saravanan2025synfuzz |
| Distinct from | sarma2026controllerdatapath |
| Distinct from | wang2026formally |
| Distinct from | zhang2025fastlec |
From bibtex.
Abstract
Behavioral synthesis involves compiling an Electronic System-Level (ESL) design into its Register-Transfer Level (RTL) implementation. Loop pipelining is one of the most critical and complex transformations employed in behavioral synthesis. Certifying the loop pipelining algorithm is challenging because there is a huge semantic gap between the input sequential design and the output pipelined implementation making it infeasible to verify their equivalence with automated sequential equivalence checking techniques. We discuss our ongoing effort using ACL2 to certify loop pipelining transformation. The completion of the proof is work in progress. However, some of the insights developed so far may already be of value to the ACL2 community. In particular, we discuss the key invariant we formalized, which is very different from that used in most pipeline proofs. We discuss the needs for this invariant, its formalization in ACL2, and our envisioned proof using the invariant. We also discuss some trade-offs, challenges, and insights developed in course of the project.
A copy is held
pdf, 396.7 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via bibtex |
|---|---|
| Added | 2026-09-17 00:43 UTC |
| Approved by | a person 2026-09-17 17:05 UTC |
Cite it as
@inproceedings{puri2014using,
title = {Using ACL2 to Verify Loop Pipelining in Behavioral Synthesis},
author = {Disha Puri and Sandip Ray and Kecheng Hao and Fei Xie},
editor = {Freek Verbeek and Julien Schmaltz},
year = {2014},
booktitle = {ACL2 Theorem Prover and its Applications (ACL2 2014)},
series = {EPTCS},
volume = {152},
pages = {111--128},
doi = {10.4204/eptcs.152.10},
}
This record lives at https://refs.drheap.org/puri2014using/ and will keep doing so.