Formal Verification和Functional Verification是ASIC验证的两种互补方法。Formal Verification使用数学方法来证明设计符合规格，而Functional Verification则使用仿真来测试设计，以针对各种场景。
Formal verification更加严格，可以发现Functional verification可能错过的错误，但它也可能更加复杂和耗时。Functional verification更加灵活，可用于测试更广泛的场景，但它不能提供与Formal verification相同的完备水平。
什么是Formal verification？
Formal verification是一种使用数学证明来验证设计正确性的方法。它涉及创建一个形式的设计模型，然后使用数学推理来证明模型符合其规格。formal verification可用于验证各种属性，例如
safety properties（例如，设计不能进入死锁状态）
liveness properties（例如，设计最终将达到预期状态）。
什么是functional verification？
functional verification是一种通过仿真设计并根据其规格检查其行为来验证设计正确性的方法。它涉及创建一个测试平台，为设计生成输入激励，然后检查设计的输出，以确保它们符合预期。功能验证可用于测试广泛的场景，包括正常操作、边界情况和错误场景等。
formal verification与functional verification：关键区别
下表总结formal verification和functional verification之间的关键区别：
| 特征 | formal verification | functional verification |
|---|---|---|
| 方法 | 数学证明 | 仿真 |
| 严谨的 | 更严谨的 | 不那么严谨的 |
| 理论上是完备的 | 可以探索设计的所有可能状态和切换 | 无法探索设计的所有可能状态和切换 |
| 灵活性 | 不太灵活 | 更加灵活 |
| 时间和精力 | 更耗时、更复杂 | 耗时更少，复杂性更小 |
formal verification的意义和场景
formal verification是一个强大的工具，可用于提高ASIC设计的质量和可靠性。它对于验证复杂设计特别有用，例如用于安全关键应用的设计。formal verification也可用于验证难以使用functional verification测试的设计，例如具有大量状态或切换的设计。
以下是formal verification的一些具体场景：
- 验证safety properties，例如设计不能进入死锁状态或设计不能违反安全约束。
- 验证liveness properties，例如设计最终将达到预期状态，或者设计将始终在一定时间内响应请求。
- 验证两种设计的等价性，如硬件设计及其软件实现。
- 验证设计优化的正确性。
- 验证设计ECO的正确性。
结论
formal verification和function verication是ASIC验证的两种互补方法。formal verification更加严格，可以发现function verification可能遗漏的bug，但它也可能更加复杂和耗时。functional verification更加灵活，可用于测试更广泛的场景，但它不能提供与formal verification相同的保证水平。
