Open Access. Powered by Scholars. Published by Universities.®
Physical Sciences and Mathematics Commons™
Open Access. Powered by Scholars. Published by Universities.®
Articles 1 - 1 of 1
Full-Text Articles in Physical Sciences and Mathematics
Using Acl2 To Verify Loop Pipelining In Behavioral Synthesis, Disha Puri, Sandip Ray, Kecheng Hao, Fei Xie
Using Acl2 To Verify Loop Pipelining In Behavioral Synthesis, Disha Puri, Sandip Ray, Kecheng Hao, Fei Xie
Civil and Environmental Engineering Faculty Publications and Presentations
Behavioral synthesis involves compiling an Electronic System-Level (ESL) design into its RegisterTransfer 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 …