Verification of Datapath and Controller Generation Phase in High-Level Synthesis of Digital Circuits

A formal verification method of the datapath and controller generation phase of a high-level synthesis (HLS) process is described in this paper. The goal is achieved in two steps. In the first step, the datapath interconnection and the controller finite state machine description generated by a high-level synthesis process are analyzed to obtain the register transfer-operations executed in the datapath for a given control assertion pattern in each control step. In the second step, an equivalence checking method is deployed to establish equivalence between the input and the output behaviors of this phase. A rewriting method has been developed for the first step. Unlike many other reported techniques, our method is capable of validating pipelined and multicycle operations, if any, spanning over several states. The correctness and complexity of the presented method have been treated formally. The method is implemented and integrated with an existing HLS tool, called structured architecture synthesis tool. The experimental results on several HLS benchmarks indicate the effectiveness of the presented method.