功能验证

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

设计输入的合法性和偏置武库被建模了。基于模型的生成器使用这个模型为目标设计产生正确的刺激。驱动器将生成器产生的刺激转化为被验证设计的实际输入。生成器在一个高度抽象的水平上创建输入，即作为事务或汇编语言。驱动器将这种输入转换成实际的设计输入，如设计的接口规范中所定义的。仿真器根据设计的当前状态（触发器的状态）和注入的输入，产生设计的输出。仿真器有一个设计网表的描述。这个描述是通过将HDL合成为低门级的网表而产生的。监控器将设计的状态和它的输出转换为事务抽象级别，因此它可以存储在"记分牌"数据库中，以便以后检查。检查器验证"记分牌"的内容是否合法。有些情况下，除了输入之外，生成器还创建了预期的结果。在这些情况下，检查器必须验证实际结果与预期结果是否一致。仲裁管理器共同管理上述所有的组件。