在数字电路验证中使用模型检验

Using Model Checking in Digital Circuit Verification

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

Formal approaches provide a new measure to the verification of circuit functions as a supplement to the conventional simulation approaches. The theoretical basis and implementation of model checking are represented which is under the category of formal verification. The computational tree logic CTL, the fix point algorithm of CTL, binary decision diagram BDD, and symbolic model checking are introduced. The model checking with SMV on a memory management unit （MMU） of a CISC processor is applied, which is proved the applicability of model checking in module level verification.