Register Sharing Verification During Data-Path Synthesis

The variables of the high-level specifications and the automatically generated temporary variables are mapped on to the data-path registers during data-path synthesis phase of high-level synthesis process. The registers in the datapath are usually shared by the variables and the mapping is not bijective as most of the high-level synthesis tools perform register optimization. In this paper, a formal methodology for verifying the correctness of register sharing is described. The input and the output of the data-path synthesis phase are represented as finite state machines with datapaths (FSMD). The method is based on checking equivalence of two FSMDs. Our technique is independent of the mechanism used for register optimization and works for both carrier and value based register optimization. The method also works for both data intensive and control intensive input specification. Our current implementation is integrated with an existing synthesis tool and has been tested for robustness