Using ACL2 to Verify Loop Pipelining in Behavioral Synthesis

Disha Puri, Sandip Ray, Kecheng Hao +1

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 a…