优点：完备性，能够完全断定设计的正确性

  缺点：首先要对原始设计进行模型抽取，这对使用者有数学技能和经验上的要求。而且，有的工具需要人工引导(如定理证明)，有的工具存在状态空间爆炸 问题(如模型检验)   类型：   (1)等价性检验   它是用数学方法验证参考设计与修改设计之间的等价性。利用等价性验证工具可对这两种设计方案进行彻底的检验以保证它们在所有可能的条件下都有一样的性能。还可利用等价性验证来验证不同的RTL或门级实施方案的等价性。   从整个数字系统的设计流程看，等价性问题几乎存在于每个上下相邻的设计层次中。   (2)定理证明技术。   运用公理和已经证明的定理证明电路的描述是正确的。   这两种方法各有特点，其中定理证明虽然能够给出设计是否正确的一个确切的回答，但由于涉及很多数学推理方面的知识，这就要求用户有很强的数学功底，这也是这种方法不能推广的一个原因。而等价性验证是验证不同阶段的设计是否相互等价的一个很好的方法。一个SOC设计是分为多个阶段进行的，那么下一个阶段的与上一个阶段的等价是设计的正确的一个保证。   4、新型的验证方法   针对SOC验证出现的各种问题现在还没有一种完全行之有效的方法出现，解决办法之一是基于断言的验证(ABV)[6]，它是把形式化方法集成到传统模拟流程中的一种有效的方法。设计团队在RTL设计中插入设计意图(断言)并且进行模拟，然后用形式化技术检查断言，限制条件，也就是合法接口行为的断言，和其他断言同时一同参加模拟。断言检查的结果改进模拟的有效性。即使利用传统的模拟验证，断言也可以大大提高模拟的效率。基于断言的验证要由用户写出断言，断言表示要验证的性质，因此需要性质描述语言。例如逻辑和时序方面的性质。这就需要尽快找到一种能实现上述功能的语言。SystemVerilog正是在这种情况下产生的，正逐渐被业界人士接受。   5、结论   形式化方法最近几年取得了长足进展，特别是等价性检验已经集成到标准验证流程中。设计和验证方法的进步应当是渐进的，不可能发生革命性的改变。因此在可以预见的几年内，混合验证方法应当成为主流的验证方法。   基于断言的验证是结合形式化验证和传统的模拟验证可行的途径。支持这种途径的统一的设计和验证语言是SystemVerilog。该语言已经得到很多EDA厂商和用户的支持，预计将会流行起来。