验证是为了确认设计是否满足spec。
ASIC芯片研发的成本很大——非常大。虽然在芯片设计的早期，第一次就有可能做对，但设计尺寸和复杂性很快就增长到工程师大概率会犯一些错误的地步。为了找到这些错误，我们必须检验设计，看看它是否以正确的方式做出反应。这个过程就是一个验证行为。
当发现问题时，我们进入调试阶段，此时我们可以了解导致问题的原因，并决定如何fix设计。然后我们回到验证，直到我们有足够的信心认为设计中不再留下错误。今天，系统复杂性如此之大，以至于不可能验证完设计的所有方面，因此我们必须在执行的验证时有选择性。
与实际设计本身相比，用于验证的时间、人员和费用花费也很大，大多数设计在制造时也还存在几个bug。如果幸运的话，这些错误不会完全阻止设计工作，并且可以找到workaround办法，以便发布产品。
在验证的早期，很多事情不是那么正式。它通常涉及迭代模型和查看产生的波形。由设计决定他们是对还是错，如果是对，则进入下一个testcase。由于测试数量和重新运行testcase以查看是否有任何变化太难了，这不再可能了。如今，验证变得更加有条理。
从根本上说，验证是两个模型的比较。如果这两个模型是相互独立衍生的，并且它们在功能上匹配，那么它们很有可能都是正确的。那么，我们所说的独立是什么意思？我们假设两个不同的人各自阅读了spec并编写了他们的模型，而没有直接相互讨论。这两个人通常来自设计团队和验证团队。
为什么要在不“直接讨论”的情况下编写模型？如果spec存在问题——定义方式的模糊性——您希望该问题在验证过程中变得明显。您不希望他们每个人编写模型的方式受到"讨论"的影响，除非它就是规范的澄清。事实上，规范的澄清，这本身就是一种验证行为。当然，不能一开始就相互讨论太多。
比较模型有两种主要方式，这些通常被称为静态和动态验证方法。
动态验证是最常见的，使用仿真器或原型。这些方法通过将激励数据发送到模型中并检查输出来结果，看看模型响应了什么。如果我们发送了足够的输入数据，那么对设计的信心就会增强。 当发现差异时，这要么意味着设计模型不正确，要么意味着验证模型不正确，要么规范存在问题。两种模型之间的比较是由checker完成的。可以构建激励，将设计带入特定场景，通常称为定向测试，也可以基于随机数据。现在，我们不只是发送完全随机数据——这不太可能完全验证到模型。相反，它是受控随机化，通常被称为约束随机或定向随机测试。
静态验证，或通常称为形式验证，是两种模型在所有条件下都是相同的数学证明。不需要激励，因为考虑了所有可能的激励。第二个模型（验证模型）通常使用所谓的属性property以不同的方式构建。属性定义了设计必须表现出的行为。或者，它可能会定义一些永远不能发生的事情。
两种验证方法都需要的附加描述是一组限制验证到一组合理状态、输入的约束。
验证是试图以最有效的方式最大限度地提高设计质量，每家公司的验证方式会有所不同，有时对每个产品来说也会有所不同。例如，与车载设备相比，廉价儿童玩具的质量水平更低。这意味着没有一种正确的验证方法，许多人称其为一门艺术，而不是一门科学。
