片上系统的模型检验

片上系统(SoC)的验证是一个比较复杂的问题，仅靠模拟仿真无法保证SoC设计的正确。形式化方法是利用数学推理的方法来证明其正确．是对SoC设计进行验证的一条重要途径。模型检验技术是一种完全自动化的形式化方法，针对模型检验技术，讨论了在SoC验证中的应用，指出在SoC设计中，只有把模拟仿真与形式化、半形式化的方法结合起来，才能更好的对SoC进行验证。

Model Checking of System on Chip

The verification of System on Chip(SoC) is a complicated problem. It not only depends on simulation, but also on other methods, such as formal verification, which is a mathematic method to reason about correction of the system. Model checking technique is a complete automatic formal methodology. How to apply model checking to the System on Chip is studied in the paper. Conclusion is given that the main trends in defining new verification methodologies are considering a hybrid combination of formal, semi-formal and simulation techniques.