Equivalence Checking between SLM and RTL Using Machine Learning Techniques

The growing complexity of modern digital design makes designers shift toward starting design exploration using high-level languages, and generating register transfer level (RTL) design from system level modeling (SLM) using high-level synthesis or manual transformation. Unfortunately, this translation process is very complex and may introduce bugs into the generated design. In this paper, we propose a novel SLM and RTL sequential equivalence checking method. The proposed method bases on Finite state machines with datapath (FSMD) equivalence checking method. The proposed method recognizes the corresponding path-pairs of FSMDs using machine learning (ML) technique from all the paths. And then it compares the corresponding path-pairs by symbolic simulation. The advantage of our method is that it separates the corresponding path pairs from all the paths and avoids blind comparisons of path pairs. Our method can deal with greatly different SLM and RTL designs and dramatically reduce the complexity of the path -based FSMD equivalence checking problem. The promising experimental results show the efficiency and effectiveness of the proposed method.