论文部分内容阅读
形式化方法作为仿真方法的补充，为电路功能验证提供了新的途径。介绍了形式化验证方法之一，模型检验的理论基础和实现方法。介绍了分支时态逻辑CTL、CTL的固定点算法，二元决策图BDD，以及符号模型检验方法。最后使用SMV工具在一个CISC处理器的存储管理单元（MMU）上应用了模型检验，验证了模型检验在模块级验证中的可行性。