Research On High-Level Equivalence Checking For SoC Designs

As the complexity of SoC increases,designers can not start the design from RTL and shift to more abstract system level modeling.System level verification has become the most important part that affects design efficiency and quality of SoC.To solve the existed problems of high-level equivalence checking(duplicated work and low verification efficiency of SoC),this thesis researches on high-level equivalence checking techniques.The techniques of high-level equivalence checking can be classified into simulationbased method,assertion-based method and formal-based method.Simulation-based methods check the equivalence by comparing the outputs of designs under test.Assertionbased methods check whether the designs of different level satisfy the same assertion.Formal-based methods utilize formal techniques(model checking,predicate abstraction,symbolic simulation)to check the equivalence of different level designs.The three kinds of methods face some difficulties.Simulation-based methods have to simulate quantity of tests,which makes the verification efficiency low and cannot guarantee the verification completeness.The verification quality of assertion-based methods depends on the quality of assertions.Formal-based methods need mapping information of designs and have state space explosion problem.This thesis first summarizes the high-level equivalence checking techniques for SoC designs.And we classify the equivalence checking methods,introduce each methods and analyse their merit and demerit.Finally,we analyse the still existing problems in high-level equivalence checking.This thesis proposes new algorithms and techniques to solve the existing problems in high-level equivalence checking for SoC designs and the contributions are as follows:First,this thesis proposes a coverage-based directed simulation method to solve the low verification efficiency and completeness of simulation-based method.we first analyze the similarities(algorithm description,modules division and data type)and the relationship of coverage between System Level Modeling(SLM)and Transaction Level Modeling(TLM).According to the analysing results,code coverage and functional coverage are introduced to equivalence checking as the quality measure of generated tests.Our method utilize combined coverage(code coverage and functional coverage)to direct high quality tests generation,simulate SLM and TLM models using the generated tests and compare the outputs.The experimental results show that our method can efficiently check the equivalence between SLM and TLM and increase the completeness of verification.Next,this thesis proposes a deep state sequence(dss)based equivalence checking method to solve the low efficiency and lacking mapping information problem of formal methods.Our method first extracts the Finite State Machines with Data Paths(FSMD)of SLM model and extracts all the dss of generated FSMD.And then test generation technique is used to generate direct tests for all the SLM dss.The output statements are inserted into the RTL model.The generated tests are converted to RTL signals and are used to simulate RTL model.The RTL dss are output after simulation.Finally,symbolic simulation and constraint solver are used to compare the corresponding dss of SLM and RTL.Our method can check the equivalence of designs without mapping information and only compare corresponding dss avoiding blind comparisons.The experimental results show that our method can efficiently check the equivalence of designs without mapping information and increase the efficiency.Next,this thesis proposes a machine learning(ML)based equivalence checking method to solve the low efficiency and lacking mapping information problem of formal methods.Our method need not extract FSMD explicitly.The output statements are inserted in the SLM and RTL models and simulate the models using the tests that generated in the process of hardware development.The states sequences will be output after simulation.ML techniques are used to classify the state sequences of SLM and RTL.According to the classification,we construct the corresponding paths between SLM and RTL.Finally,symbolic simulation and constraint solver are used to compare the corresponding paths of SLM and RTL.Our method can check the equivalence of designs without mapping information and only check the corresponding paths avoiding blind comparisons.The experimental results show that our method can efficiently check the equivalence between SLM and RTL.Finally,this thesis proposes a Shared-Value Graph(SVG)based equivalence checking method to solve the low verification efficiency and multiply iteration of loop structure problems of scheduling in high-level synthesis.Our method utilize cutpoint technique to generate bisimulation locations and utilize SVG to check the equivalence of common variables in the bisimulation locations.Cutpoints techniques can decompose and verify the large designs.The bisimulation locations can decrease the number of comparisons and increase the verification efficiency.SVG can check the loop structure in a single time which avoids iterations to fixpoint.The experimental results show that our method can efficiently check the equivalence in high-level synthesis.