验证方法
模拟：动态验证，常用，如今最主流的验证方法。
仿真：类似模拟，但依赖于硬件。
形式化验证：静态验证，用数学方法对模型的功能、功能、规范做检验。验证的完备性高，但实施困难。
半形式化验证：形式化验证和前面结合。
形式化验证分类
按验证内容分类
性质检验（property checking）：是否满足某些规范和功能需求。
等价性验证（equivalence verification）：两个设计是否是等价的。
按验证方法分类
定理证明（Theory Proving）
模型检验（model checking）
等价性验证（equivalence proving）
接下来对这三种方法详细说明。
三类形式化验证方法
1. 定理证明
使用定理证明系统（内置了各种推理规则、推理对策、元对策等），从原始设计中抽象成形式逻辑（一阶逻辑、高阶逻辑、时态逻辑）模型，在验证者引导下对公理和已证定理施加推理，最终证明出所需的目标定理。没有完全自动的定理证明。
一些定理证明系统：PVS，LCF，ACL2，HOL，isabelle，coq 。其中HOL和PVS系统是高阶逻辑证明系统。
2. 等价性检验
如给定两个电路，等价性检验就是考察在有影响的输入下其输出是否一致。如此，输入可以分为：
使输出为1的输入。
使输出为0的输入。
不管项：与输出无关的输入。
等价条件：使它们输出不同的每个输入向量，至少是其中一个电路的不管项。
一些等价性检验工具：
Candence的Affirma
Verplex的Logic Equivalence Checker
Synopsys的 Formality
Mentor Graphics的FormalPro
等价性检验途径：
符号方法：将问题形式化成为符号表示，然后用特定的问题求解方法，如BDD，SAT。适用于系统缺乏结构相似性，不能得到 系统设计的内部情况时。
增量方法：利用被检验的系统在结构上存在的相似性，逐步检验内部局部子系统的等价性，进而最终得到系统在整体上的等价性。适用于相似性比较大的系统。
3. 模型检验
针对并发系统的一种自动验证技术，系统用有限状态结构表示，被验证的性质使用时态逻辑公式表示，对状态空间进行搜索以确定被验证的性质是否是可达的。
模型检验速度比较快，且对于不满足的性质能给出反例，但缺点是存在状态爆炸问题。
模型检验分为离散系统和混成系统，对于离散系统，有：
基于Kripke结构：SMV，nuSMV，SPIN，VIS
基于时间自动机：UPPAAL
基于概率（统计）：UPPAAL，Prism