硬件设计形式化验证

数字电子设计中的形式化验证技术是重要的技术，相对于业界普遍采用的基于仿真的验证方法，能够覆盖较为完整的状态空间，从而在电子电路设计的早期阶段发现设计缺陷。其中：

• 等价性验证（Equivalence Checking, EC）是用于验证两个电路是否拥有等价的逻辑的技术，例如比较原始电路与经过优化的电路的等价性，或是比较逻辑综合的过程前后（例如RTL与门级网表）的等价性。

• 模型检测（Model Checking, MC）主要用于验证一个可以转化为有限状态机的时序逻辑是否满足某些属性。模型检测主要使用基于时序逻辑语言（CTL或LTL）表达的属性，并在一定的周期内检查模型中的所有状态，从而验证给定的属性是否在整个模型中成立。

• 测试向量生成（Automatic Test Pattern Generation, ATPG）,通过基于电路中特定的故障模型或启发式方法形成测试向量，相对人工撰写测试样例方法能够提供更高的测试覆盖率。

本实验室自主研发了相应的形式化验证的工具。在一些来自工业数字电路实例的数据集中，其表现优于开源工具。