在电子设计自动化中，功能验证是验证逻辑设计是否符合规范的任务。功能验证试图回答以下问题：所提出的设计是否达到了预期的结果？这是一项复杂的任务，占用了大多数大型电子系统设计项目的大部分时间和精力。功能验证是更全面的设计验证的一部分，除了功能验证之外，还考虑时序、布局和功耗等非功能方面。功能验证非常困难，因为即使对于简单的设计也存在大量可能的测试用例。通常需要进行超过 1080 次可能的测试才能完全验证设计 - 这个数字在一生中是不可能实现的。这项工作相当于程序验证，并且是 NP 困难的，甚至更难——尚未找到在所有情况下都能很好地工作的解决方案。然而，它可以通过多种方式受到攻击。它们都不是完美的，但每一个在某些情况下都会有所帮助。逻辑仿真在构建逻辑之前进行模拟。仿真加速将专用硬件应用于逻辑仿真问题。仿真使用可编程逻辑构建系统的一个版本。这是昂贵的，并且仍然比真实硬件慢得多，但比模拟快几个数量级。例如，它可用于启动处理器上的操作系统。形式验证试图从数学上证明满足某些要求（也可以形式化地表达），或者不会发生某些不良行为（例如死锁）。智能验证使用自动化来使测试平台适应寄存器传输级代码的变化。 HDL 特定版本的 lint 和其他启发式方法用于查找常见问题。基于仿真的验证（也称为“动态验证”）广泛用于仿真设计，因为这种方法易于扩展。提供刺激来练习 HDL 代码中的每一行。建立一个测试台来验证设计的功能，方法是提供有意义的场景来检查给定的输入，设计是否符合规范。模拟环境通常由多种类型的组件组成。生成器生成输入向量，用于搜索意图（规范）和实现（HDL 代码）之间存在的异常。这种类型的生成器使用 NP 完全类型的 SAT 求解器，计算成本较高。其他类型的生成器包括手动创建的向量、基于图形的生成器 (GBM) 专有生成器。现代生成器创建定向随机和随机刺激，这些刺激通过统计驱动来验证设计的随机部分。随机性对于在可用输入刺激的巨大空间中实现高分布非常重要。因此，这些生成器的用户故意低估了它们生成的测试的要求。生成器的作用就是随机地填补这个空白。这种机制允许生成器创建显示用户未直接搜索的错误的输入。生成器还将刺激偏向设计的极端情况，以进一步强调逻辑。偏差和随机性服务于不同的目标，并且它们之间存在权衡，因此不同的生成器具有这些属性的不同组合。由于设计的输入必须有效（合法）并且应维持许多目标（例如偏差），因此许多生成器使用约束满足问题（CSP）技术来解决复杂的测试要求。