关于formal verification和model　checking的问题

个位大虾，问个问题：formal verification分为两类：model　checking & equivalence checking。后者很容易理解，model checking 始终不太明白。可以这样理解吗?比如说一个IIC模块，用SystemC做了建模，而且已经保证它是正确的，然后RTL写完之后不用动态仿真而是直接把RTL和SystemC的模型做对比，如果行为一致刚说明RTL功能正确。这么理解对吗?

谢谢了

2# jinzhao 谢我干嘛啊，我是在问题，请不要在这里灌水好吗?有专门的水区

model checking，模型检验
我觉得是用以一种符号模拟语言来描述被测设计，以及属性，再通过算法验证。
比如：http://www.cs.technion.ac.il/~ss ... mv/NuSMV.tools.html
NuSMV is a model checker that verifies finite state systems written in a language that is designed to allow the description of such systems, ranging from completely synchronous to completely asynchronous.
It is a reimplementation and extension of SMV, the first model checker based on BDDs.

4# whxqq 谢谢啊

你对model checking的理解不对。
model checking的工作过程是：电路的形式化模型+性质，共同作为模型检验器的输入，模型检验器会告诉你这个形式化模型是否满足上述性质，如果不满足则给出反例。
其中“电路的形式化模型”可以手工书写（如上面的NuSMV的介绍），也可以使用模型检验器直接读取RTL（它会读取RTL并转化为内部的形式化语言描述的模型）。
其中的“性质”，就是你要验证的功能点的形式化描述

很好，受教了

got lot. It's very good.