随着一些新科技的出现，例如受约束型随机数据生成法（Constrained-random Data Generation）、以断言为基础的验证（Assertion-based Verification）、支配导向覆盖率（Coverage-driven Verification）以及正式模型检验（Formal Model Checking）等，衡量功能验证(Functional Verification)工作效率的方式已经大大不同。虽然仿真(Simulation)仍将继续扮演实际上验证工作中不可或缺的部分，但当我们在评估整个验证过程的时候，仿真的速度已经不再是最主要的考虑基准。使用者可以通过上述多项新科技的帮助，搭配原先所单独倚仗的仿真，完成更先进的验证工作。
定义一个新的验证策略
通常来说，功能验证是为了回答以下问题：究竟我有没有构建出正确的东西来？相对来说，执行验证（Implementation Verification）可以解答这个问题。一直到今天为止，大部分的验证工程师们还是维持长久以来同样的工作模式：找寻工作速度更快的仿真器(Simulator)。也因此，典型评估设计工具的方式是把一个HDL Model和一个HDL Test-Bench(通常是一个直接简单的测试)置于各个不同的仿真器中运行，哪一个仿真器运行得出正确无误的结果、而且是最快完成的，就会得到使用者的青睐。
然而，单纯让工作“跑得更快”已经不够了，眼前可以看到的设计已经变得太大且太复杂，无法成功预测所有的个别案例(Corner cases)。因此，验证策略必须修正，而为了要明确定义出如何改变才能正确且足够地达成目标，必须先定义清楚几件事情，也就是一个成功的验证程序所必须达到的基本目标如下:
◆必须成功验证某个设计是否完成所有期望中必须达到的事项
◆必须成功验证某个设计是否没有做出任何期望中不该达到的事项
◆必须告诉使用者上述两项目标何时已经被达成了
但Verilog和VHDL语言以及常规的仿真器并无法支持完成这三个目标。于是，受约束型随机数据生成法（Constrained-Bandom Data Generation）、Assertion-based Verification、覆盖率导向验证法（Coverage-Driven Verification）以及Formal Model Checking等方法论应运而生。
当设计随着摩尔定律所预言的速度持续扩张，很显然地有越来越多的功能需要被验证；但是另外一方面，迅速进入市场的压力也在同时间直线增长。在某些状况下，验证有可能会吃掉整个设计流程七成以上的时间，我们唯一能够做的事情便是在最短的时间之内，完成所有必须的验证工作。分析一下，要尽快测试完所有的功能，并能在预定时间内完成所有必备工作的可能途径如下：
◆删掉设计里部分的功能，进而让需要测试的部分减少，这种方法显然不可行，所有设计中的功能都是为满足市场需求而设定出来的，删掉部分的功能将会使产品变成“四不像”，因此，这不是一个好答案。
◆添加更多的人力来进行验证工作，这样可以写出更多的测试。这也不会是一个好途径，因为大部分的机构都已朝着缩减预算的方向走，更何况令人沮丧的事实是，增加人力并不会使得验证的成果呈现线性的增长。
◆事实上，唯一可行的方式是将上述两点的要旨做些许的修正，也就是如何让验证团队有能力生产出更多的测试，并同时把时间与资源花费在真正应该测试的部分上面，然后让整个验证程序更快被完成。
理想中的解决方案可以帮助工程师们依照上面第三点途径搭配应用新一代的验证技术和方法，发挥更大的生产力。以下将介绍每一种新科技的优点与缺点，如何巧妙地运用使其发挥互补性，才可达到事半功倍的效果。
受约束型随机数据生成法
长久以来，仿真就是验证(Verification)的核心技术。验证工程师针对需要验证的设计，发展出测试文档来生成所需要的测试激励(Stimuli)注入在设计里面，在完成仿真之后查看结果是不是得到正确的反应。所有的测试都需要花时间来编写、纠错还有运行。当我们确定某一个测试可以成功地被运行并且覆盖某特定功能之后，我们会将它添加回归测试套件(Regression Suite)当中，然后着手撰写下一个测试文档，当然又得经过编写、纠错以及运行等步骤。这样的方式使得负责测试的工程师为了能够覆盖设计里面所有不同的特性而撰写出不同的测试文档，这是为了完成验证工作的第一个目标。当添加越多功能在设计里时，就得花更多时间并添加更多的测试文档来达成目标。
在以仿真为主的流程里，验证工程师首先须把设计里面的基础架构(Infrastructure)先串好，再想办法编写测试文档，然后安装到设计里面，记录并查看结果。这种创建测试平台(Test-Bench)的方法可能会占去绝大部分的验证时间，甚至变成整个企划的关键步骤。一般所谓的测试平台自动化指的是通过EDA工具的帮助，应用某些方法论来创建上述的验证环境，目的是让验证者在最短的时间内检测完最多的特性。因此，测试平台自动化的质量好坏就决定了可以在多短的时间内创建起所需要的环境，并发展出所有的测试文档。
若将测试平台比喻作一台大机器，上面有许多的开关和旋钮，而测试文档就是一连串运行“控制开关”和“扭转旋钮”按特定顺序指令工作。可想而知，如果机器上面有越多的开关和旋钮，而它们上面又各自有越多的刻度，那测试文档撰写者就必须得花更多的时间来描述所有可能的情况。每种情况会通过不同的路径进入设计里面不同的状态，也同时测完特定的一些功能。在如此的状况下，如果想要得到更高的生产力，似乎就得想办法让验证工具能够自动地控制旋钮和开关，以创建更多种的环境来完成测试。
上述的测试平台自动化可以利用受约束型随机(Constrained-Random, CR)搭配仿真来完成，其要旨是每一个测试文档确实描述一堆可能的情况，而仿真器本身在每次被启动(Invocation)时会自动选定其中的一种来运行。而为了帮助我们能够有效控制开关及旋钮，市面上所看到如SystemVerilog和SystemC这样的验证语言提供可利用约束条件(Constraints)的方式来描述测试激励的情况，用来控制驱动设计信号和交易的数值在一定的合法(Valid)范围。因此，仿真器便能随机生成激励所需要的数值，而且在此同时约束条件(Constraints)确保发生的情况都是正确的。要进入下一个情况时，我们可以很轻松地在仿真器中搭配另一个不同的随机种子，产生不同但合法的激励，然后检验另一个新的特性。
想像一个Bus-Based的设计，其协议(Protocol)允许单字组(Single-Word)和脉冲(Burst)两种类型的访问。可以利用描述发生在总线上面的处理(Transaction)来构建一个测试，然后让处理读写方式和总线模式(Bus mode)可以被随机决定。利用“CR”，使用者可以仅用一个测试就验证完所有的总线模式，更有机会发掘出一些个别案例，例如在一个Single Write之后马上来了一个Burst-Read的状况。而如果在总线上面的多个装置都对应到不同的地址范围(Address Range)，或是某些装置并不支持所有的总线模式，我们所要做的只是更改原本的约束条件来随机生成地址信息，并且约束总线的模式，让测试只会在合理地址范围内成为提供的模式之一。这样一来，便能够测试总线上每一个装置是在所有被支持模式之下的行为，并且可以保证不包括任何所没有被支持的状况会生成。
覆盖率导向验证法
由上述例子可知，在真正开始进行测试之前并无法得知会被采用的地址和模式，因为它们是被随机产生出来的，所以在进行仿真的时候记录下某些信息是必要的，目的是弄清楚哪些情况是真正被运行过的，这样记录的动作通常被称作功能覆盖率(Functional Coverage)分析，所得出的数据对于验证过程的效率性一目了然。倘若我们可以利用覆盖率分析的数据来理清某一个特定的测试是否测到某个想测的功能，或是到底测得好不好，接下来再将此数据回报给处理程序来决定验证的下一步该怎样进行，这样的方式称为覆盖率导向验证(Coverage-Driven Verification，CDV)。在本文所谓“高阶的验证方式”里，CDV的要旨在于能自动化记录并分析某些测试情况是否已经被运行，然后运用这些信息帮助剩下来的验证工作可以更有效率地被完成。
CDV是利用单一测试随机生成出测试激励，进而自动生产出多样的情况，因为其与生俱来的“随机”特性可以让原本简单的一些测试有能力找出个别案例的错误(Corner Case Bugs)，也就是一些设计者压根儿也不会想到的状况。当覆盖率的信息被收集完毕后，新的测试可以被自动化或是用人工创建出来，其创建的原则是更改约束条件，把未被覆盖的功能或情况当作验证目标。一个良好的CDV应用会需要使用者利用断言(Assertions)或是其他机制来具体指定其所必要运行到的覆盖点(Coverage Points)或是特定行为(Behavior)。
功能覆盖率这个用语，在不同的文章与引用处会有不同的含义。在最基本的状况之下，覆盖率分析就是记录一些数据，以确定是否所有情况都被测试完毕。其实，利用一些简单的Checkbox加上EXCEL程序就可以完成一个覆盖率分析的表格。而一个缺乏经验的工程师可能就会利用这个表格搭配波形图的方式来观察一个Bus-Based设计，辛苦地分析某些地址和模式是否被运行过。
正如所谓程序码覆盖率(Code Coverage)存在许多不同的类型，如Line、Toggle、Path、Expression等，功能覆盖率也有很多的细分类，其决定于所要测试的对象，像测试覆盖率(Test Coverage)以及规格覆盖率(Specification Coverage)分别是根据验证计划(Verification Plan)或是功能规格(Functional Specification)来测量某些特性是否已被测试。值得注意的是，这种类型的覆盖率分析其实很容易用上述的粗浅表格法来完成，而其重点是将所谓“记录数据”及“就数据提出报告的能力”构建到验证程序当中。
结构覆盖率(Structural Coverage)是一种比较先进的次分类，它是由0-IN与Mentor Graphics所提出。在设计内有一些较为困难验证的部分，例如Arbiters、FIFOs、还有跨时脉范围(Clock-Domain Crossings)的设计及一些类似的问题。但是有趣的是，此类器件的行为相对来说比较广为大家所了解，事实上，可以轻易定义出确认其已被覆盖完毕所需要的规则。而所谓的结构覆盖率就是在设计里辨别出这些器件，然后自动地根据功能覆盖率的数据提出报告。
除了“分析”功能覆盖率数据的工作之外，我们可以先就如何收集这些信息来讨论。这必须先认清一点，收集数据的工作本身也是功能覆盖率的一种，所以要小心理清讨论的目标究竟是什么。在上面所提到的收集包括记录两种基本型的功能覆盖率：即数据导向覆盖率(Data-Oriented Coverage)以及支配导向覆盖率(Control-Oriented Coverage)。
数据导向覆盖率指的是在仿真中某一特定时间点，记录下一连串变量的值。举例来说，在一个网络应用上，它可能应用来记录某些打包在进入某设计之前和之后的内容。上述曾提到的总线架构设计里，也许可代表在每一个总线周期(Bus Cycle)的起始点扫描出地址和总线模式(Bus Mode)的信息。如此记录的工作通常在创建激励的过程中完成，以确保使用者已确实把所有的处理类型(Transaction Types)都规范正确。除此之外，也可能会在检查结果的时候做完记录，其好处是每个器件的回应都是正确的。无论如何数据导向覆盖率的记录都是在测试平台里面完成，而不是待测器件(Device Under Test, DUT)。结果通常会以矩阵的方式呈现，其内涵是当每一个变量在其他变量固定于特定数值时，有多少次机会可以达到某一特定数字，得出来的每一种特殊组合会被记录其出现的次数，最后工具再帮你把这些组合出现的总和数据汇报出来。
支配导向覆盖率指的是记录bu上或是DUT里面某些特定短暂行为(Temporal Behaviors)发生的次数。基本上支配导向覆盖率大都是使用者在利用断言(Assertions)的时候，工具会记录下某些被运行的特定协议，或是某特定情况(Scenarios)发生的状况。举例来说，一个retry发生在某传输框(Frame Transfer)的第n个打包，或是当CPU正在运行jump的时候却来了一个干扰(Interrupt)等状况。典型的支配导向覆盖率的成果是一连串的数据代表每一种序列(Sequence)发生的次数为何。
Assertions所定义出来的序列可以是有弹性的，也就是例如“某b在某a的1~3个时钟之后发生”。如果我们可以知道某b在a之后一个时钟出现的次数和三个时钟之后出现的次数各是多少，这样的信息就相当有参考价值了。上例中的覆盖率次分类通常被称作断言覆盖率(Assertion Coverage)。
正式模型检验
正式模型检验(Formal Model Checking, FMC)又可以称作属性检验(Property Checking)，其含义和同属正式验证(formal verification)的等效检验(Equivalence Checking)完全不同，虽然都是依靠详细的数值分析来完成。所谓的等效检验是比较两种不同的导入方式是否功能性等效(Functional Equivalence)。然而，FMC是彻彻底底地检查过设计中所有可能的状态，看看是否有任何可能违反某特定属性的状况发生。
通常会利用Assertions来表达所谓的Properties，而内涵则是表示在一个设计里面一些精确的序列型(Sequential)行为或是不变动(Invariant)行为，前者例如“某甲发生在某乙之后”，而后者则例如某甲“永不发生”或是某乙“一定发生”。因此，可以把每一个Property当成规格(Specification)的一个小片断。可以将Property描述为设计的某些行为，或是把property描述成对于输入设计的input其行为上的限制，也就是所谓的约束条件。在此Constraints其实跟我们讨论“CR Simulation”时提及的Constraints是相同的，虽然引出这个词汇在使用流程上的来龙去脉有点不同。
就理论上来说，可以利用FMC成功验证任何一个极端复杂的设计。但是当我们实际来看，因为FMC牵扯到的数学分析可能复杂到难以想像，有些时候可能会影响FMC应用到设计里面的一些小区块。不过，由于FMC有能力分析出所有设计里面能够达成的状况，因此即使省去使用者自己撰写测试文档的步骤，应用它来彻底验证一些特定的功能是完全没有问题的。在此情况下，Properties反而扮演了验证目标的角色，搭配Constraints来定义某设计的环境条件。以下将会讨论FMC在Block Level中所提供的更多好处。
正式模型检验以及仿真
正式模型检验可以被视为仿真技术的互补，同时也扮演CDV方法论中不可或缺的一环。FMC能够彻底验证完设计中的所有可能状况，也就是可确保符合所有使用者定义Assertions的规范，同时也确保顺利达到所有的覆盖点。把FMC技术与仿真技术搭配使用的时候，可看到一个崭新的验证方法－动态正式验证(Dynamic Formal Verification ,DFV)，这概念是由0-IN所提出，其出现大大地提升了CDV内涵与价值。
首先把一些FMC与仿真的基本概念重新思考，大部分的仿真器包括Mentor的ModelSim，新思科技的VCS还有益华计算机的NCSim都是利用“Event-Based”的语义运行设计行为，而正式工具(Formal Tools)是运用Cycle-Based的方式来工作。将这两种模式分开使用来验证设计时，可能会使得结果产生一些意想不到的差别，使用者得要非常小心，否则常常会使得Formal Tool跟仿真器针对特定的Property运行出不同的结果。也就是因为这种潜在的危险，0-IN的正式验证功能会自动重新运行所有仿真器表现出的FMC反例以确保两种诠释方式的结果最后是殊途同归。
为了能够确保仿真器与FMC的结果一致，将SystemVerilog与PSL两种验证语言标准化就显得很重要了。因为如此一来才可以确保不同语言的Properties之间拥有相同的语义。如此的一致性促成可以运用通过block level正式验证的Properties来当作仿真过程中的监督者(Monitor)，尤其是在仿真大型的系统时更有效果。例如当给予某个区块指定的一些Constraints，如果它能成功通过正式验证，确认其会有某些特定的行为之后，接下来需要做的便是确认系统中与此区块有相关性的其他部分也符合同样的Constraints。由于Assertion Monitor会在系统仿真时自动检查block的输入，我们可以借此验证所有的输入Constraints是正确的，同时FMC分析也毫无瑕庛。
如果FMC能够正式证明某个区块在给予的一串输入行为之下可运转正确，而且整个系统也只会让这个区块在上述输入行为的规范内工作，那我们就可以百分之百确定此区块在这个系统里面永远不会出错。因此不需要在Full-Chip仿真的时候，绞尽脑汁想产生一堆复杂Stimulus，就为了使得区块可以跑到某些特殊的状态。而我们就可把仿真工作专注于整个芯片End-to-End的正常行为，因为单一区块的行为已经能够确保我们高枕无忧。
以断言为基础的验证
比较常看到的状况是我们都把所谓的Assertion-Based Verification(ABV)视为利用Assertions来当仿真时的监督器，虽然这没有太大的谬误，不过更正确的解释应该是将Assertions分别利用在仿真以及正式验证中。因为Assertions在仿真和正式模型检验内都可以扮演极重要的角色。所谓的Assertions让我们可以利用简单的数学概念来精确描述某区块需要遵守的行为，或是约束其运作环境。除此之外，Assertions还可以被利用来描述覆盖点，所谓覆盖点指的是不管使用任何的技术，在验证过程里面都必须要运行到的某些特定情况。
Assertion常常会被分类成“White-Box Assertions”和“Black-Box Assertions”。White-Box Assertions让我们可以对于设计的内部状态一目了然，而且通常可以反映出设计者所决定的特定履行(Implement)方式，例如某特定状态机被设置为“one-hot”。而Black-Box Assertions则是拿来描述“End-to-End”的行为，也因此它与设计者怎样做内部设计没有关联。Assertions的最大好处是可以让设计者在验证过程当中，轻松地检查设计或是环境有没有照着原先想像的方式。有趣的是，我们常听到的问题是“我怎么知道这样就够了呢？”。
如果Assertions被赋予的使命是验证设计的行为是否合乎规格的规范，有两种方式来评断“是不是真的够了”。首先是要确定有足够的Assertions来验证我们想要验证的所有关键行为，通常这也就是验证计划的一个部分。第二点是要确定设计里面的“每一个部分”都充分地与“至少一个Assertion”有相关，有关这部分就可以视为所谓的“Assertion密度”，其估算的方式是计算需要多少Clock Cycles才能让寄存器数值传送到一个Assertion。如果所需要的Clock Cycle越少，就代表我们能够更容易对于某些Assertions是否有被违反来做正式分析。倘若整个设计里面的每一个部分都可以在两个到三个Clock Cycles里面被Assertions测过(这是经验法则里面比较成功的案例数字)，也许就能回答你：“是的，这样已经够了。”
技术价值的说明
覆盖率导向验证法的价值说明
所谓CDV的价值，可从往两个方向考虑，第一是所提出来的解决方案究竟能够缩短多少创建测试平台的时间﹔第二是相关的测试到底能多有效地被运行并验证设计里的待测特性。
当我们将测试平台组合起来的时候,所谓的价值就可以用以下的条件综合考虑:
◆能否提供足够且具水平的IP缩短编写程序码的时间
◆有没有优良的方针指引我们创建一个可重复使用而且支持多样抽象(Abstraction)层级的验证环境？
当我们建好测试平台而且确认其可以正常工作后，接下来就是要运用CR技术的优点来帮助搭配仿真。而为了能够顺利完成使命，在CR仿真需要注意三个基本方针。首先，既然某些语言可以描述随机数值的约束条件，就得选择一个能支持这些语言的仿真器。第二，仿真器本身得要具备所谓约束条件解决器(Constraint Solver)的附加功能。所谓的Constraint Solver功能指的是能够忠于原味地将我们下在Constraints里面指定的随机数值表现出来。毋庸置疑的，如果一个Constraint Solver能够把这些随机数值组成功地尽量扩张，就能够协助我们生成出更多不同且具有意义的情况出来。接下来第三点，需要搭配Functional Coverage的功能来监督确保我们所想要的情况真的都已被有效运行。而就整个方法论的观点来看，CDV也同时需要测试本身能够做自我检测(Self-Checking)。
一个好的CDV方法论当然要能够支持验证的第一个目标，也就是成功验证某个设计是否完成所有期望中必须达到的所有事项。而其重点是要能够更容易创建整个验证环境并且生成某些测试，这些测试可以确保我们测完设计本身被期望达到的某些特性。在此很重要的概念是或许设计里有些特性可直接用手写测试反而较易测，也就是写测试的工程师直接提供一些Scenarios来测试就可以。但是对于大多数的特性而言，运用CDV概念使用Constrained-Random Tests来生成出各种不同却合理的情况并完成测试，才是一种有效率的验证法。
CDV也能顾及到验证的第二个目标，成功验证某个设计是否没有做出任何期望中不该达到的任何事项。试想，设计者可能没有办法将设计与子系统交互的所有状况都考虑进去，但是由于随机数值的不可预测性，促使更有机会可以发掘出一些个别案例。
正式模型检验法的价值说明
关于CDV也许能够协助找出一些在仿真工作的时候，设计者忽略考虑到的一些情况。而就定义上来说，正式分析的基本宗旨就是能够保证所有的情况都可以被测到。因此，我们可以利用FMC的方法给予一些输入Constraints来正式验证一个block，然后观察它是否正确地工作。这样我们就可以省去在block level做仿真的时间，因此，不管是用Constrained-Random或是直接做测试都可以省略。所以，当所有的区块都在一起做验证，看看工作是否正常的时候再来利用仿真即可。
另一种看法表示，可以利用FMC把整个芯片层给完全验证完毕而省略掉仿真的步骤。这样的说法必须在下列的条件下才能保证不会出错：如果你给某区块A一些输入行为，然后确认它可以工作无误，接下来你也得确认与区块A有相互作用的区块B并不会有任何“违反”上述输入行为的状况出现。这样的正式验证被称作为“Assume-Guarantee示范”，而且理论上这种方法是可行的。接下来要证明那些“区块B的输入”也符合上面的假设内容，然后依序往前推。回到现实面来看，想要有效地管理properties与区块之间的相互关系并非如理想中那么容易，理论里的大同世界在实际上可能是困难重重。
但也不用因此而太悲观，有一个人数不少且持续增长中的使用者联盟十分认可FMC的潜在益处，尤其是针对设计里面占有重要关键位置的一些组器件，例如Arbiters、Clock-Domain Crossings还有FIFOs等等。FMC的真正价值在于彻底分析的能力，对于找出不管是设计中或是规格中的错误相当有用。
当正式分析找出了问题之后，纠错机能会开始判这个问题究竟是“设计出了错”或是“Assertion的瑕疵”。别忽略一种可能性，写Assertion的人很可能把规格的要旨诠释错误。这种状况发生候，出错Assertion就必须要被更改。但是通常问题大部分会出在设计里面的错误。由于FMC彻底分析的特性，上述的任何状况都难逃法眼，并且会一一被修复，因为当所谓的“被验证过的Assertions”被使用在仿真上的时候，我们对于这样买了双保险的验证程序才更加的有信心。
覆盖率导向验证搭配正式模型验证的价值说明
CDV是通过随机生成Stimulus的方式来使得一个单一的测试可以自动创造出多种不同的情况。测试正因随机与生俱来的好处，我们有机会可以查找一些设计者原先没有想到的个别案例错误。FMC则是彻底鉴定完所有设计里面可能的状况来确保设计与规格里的描述具有一致性。FMC利用Properties或是Assertions来做实际上的检测，担保可以把所有的个别案例错误给抓出来。事实上我们可以把Constrained Random Simulation就当作FMC的近似类型，只是它利用仿真来代替正式分析。
想想上面提过的一个问题，是不是FMC只能拿来做小区块的静止分析呢(Static Analysis)？其实所谓的限制大部分是来自内存和运算资源的不足。还好，“动态正式验证(Dynamic Formal Verification, DFV)”可以增强追踪仿真工作，提高CDV方法论的价值。
给定一些目标行为(也许是利用Assertions或是Coverage Points来表现)，DFV运用了正式分析的方式来追踪仿真工作里发现的一些“令人关注的状态(Interesting States)”，然后判断它们会不会违反任何一个Assertions或者是能不能触及到某一个Coverage Point。对于功能验证的过程来说，所谓的“令人关注的状态(Interesting States)”是指发现某个“新的”或是“稀有的”设计行为发生的状况。
让我们解释一下这个概念，想像一个错误在仿真开始很久以后才出现，而这个错误只有在某一特定FIFO满了，并且某特定FSM处于“FOO”状态时候才会发生。若只通过仿真，我们需要想办法让安装的测试去喂饱那个FIFO，然后再用同一个或是另外一个测试去驱动目标FSM进入FOO状态。如果仅应用随机激励去期待两个事件会一起发生，这样的机率恐怕不高。也就是说Constrained-Random Stimulus也许需要测试平台拥有一大堆的“旋钮”和“开关”，来达成这样细密的控制，才能找出所有类似的个别案例。
倘若此时导入DFV的概念，当仿真工作走到FIFO是充满的状态时，正式分析会开始检查所有此时间点所推算出来的所有状况，所以可以顺利发现并且揭露出生成此状况而且导致错误的特殊程序究竟为何。因此，利用DFV搭配CR运用比起只单纯利用CR来做测试的好处在于可以省去很多创建额外测试平台程序码的功夫。
如果没有DFV，一个CDV的使用者得要考虑可能会有潜在的错误存在，然后想办法更动Stimulus Constraints以设法引导测试达到特定的一些状况。显而易见的这并不大容易。就现实情况而言，DFV通常能够将单一的情况扩张成相当大量且有效的测试(也许超过一万个)。这样一来，真正的测试平台约束条件就可以变得简单的多，因为我们无需为了上述的“细密控制状况”绞尽脑汁以建出理想中的Constraint环境。
方法论探讨
前面的讨论主要都是着重在验证流程中所谓创建测试平台自动化，以及正式属性检验技术的概念。为了能够真正在实际上发挥效用，接下来就要讨论如何应用这些技术，并且看看到底在实际上可以或是可能可以做些什么事情。其实所谓“如何应用”完全决定于设计者本身，验证的工作其实就是确保如何应用，以吻合规格所指定要做的什么事情。
须注意的是，在从制定的规格移动到真正逻辑闸的过程里，通常都会运用到多个不同程度的抽象层级(Levels of Abstraction)。然而，想要成为一个成功的验证方法论，其中之一的条件便是能够轻易地在抽象层之间转移，并且维持功能上的一致性。
施行验证(Implementation Verification)指的是确保RTL到闸门层之间的一致性。一般来说，大家对于合成(Synthesis)过程的精神了解颇丰，想要检查RTL到闸门的一致性相对来说比较直观。在此状况当中，所谓的“RTL”就可以被看作是与“闸门层设计”相比较时的“规格”。另外一方面，对于所有功能验证的过程来说，所有意图都是为了可以确保RTL设计能够精确反映出我们期望中的功能，因此也可以成为要比较闸门层功能时的正确目标。所以本段落所提到的功能验证里，RTL的角色就被视为拿来跟规格相比较的导入过程。
不管是讨论到施行验证或是功能验证，验证的基本工作都是去比较两种行为各自的表现。有很多方式描述期望中的行为，其中之一是利用Properties或是Assertions，然后利用它们来做FMC，拿来跟RTL做比较，彻底验证设计里面的次区块的功能是否正确；另一方面，Assertions也可以拿来运用在仿真当中监控已经被运行过的行为。当然众所周知仿真本身也需要另外一种表现期望中行为的对象，就是测试平台。
交易层原型的塑造
能够经常考虑验证流程如何比较有效率是一件好事，而确信最有效的方式就是让测试平台永远聚焦在设计被期望达成的目标上。想要达到这个目标，最合理的方法也许就是让测试平台在“交易层(Transaction level)”里被完成。所谓“Transaction”指的是设计里面某个任意活动的表现。而且可以被表现在各种不同的抽象层级之中，例如un-timed、cycle-accurate、pin-accurate等等。因此一个交易层级的测试必须能够描述目标交易所应该运行的工作。而验证环境这时所扮演的角色是负责转换这些transactions成为明确的行为，使这些行为能够合乎将进行仿真模式的抽象层级。我们常常会利用所谓的“Transactors”或是“Bus-functional models, BFM”等器件，它们都是运用来做上述转换的工作。在此可以定义一个好的验证环境：允许我们创建交易层级的测试，并且提供完善的机能，即使设计里面有不同抽象层级的运用，这些测试仍然能够被成功地使用。
首先，让我们讨论一下仿真，不管交易是被应用在哪一种抽象层级之内，总是会有一些信息是与这些层级相关的，例如地址或是数据等。可以说测试是用来描述交易，而Transactors则是用来执行这些交易。CDV的好处都可以在交易描述符号(Transaction Descriptor)的身上查找，这些符号可以告诉Transactors该做些什么，还有该指定哪些的随机约束条件。倘若我们可以创建标准界面组，用来管理测试、Transactors还有设计之间的通讯，就可以轻易地通过交换架构中比较低端的部分，而无需想办法改变较高的阶层。如此一来，一个相同的测试可以通过一组Transactors来驱动设计中的一个交易层模式，也可以通过另外一组不同但是却兼容的Transactors来驱动一个RTL模式。
当我们进入一个交易层模式的仿真时，“黑匣子(Black Box)”的Assertions可以用来指定在此层的某些特定行为，而当我们更改设计下到RTL层的时候，黑匣子的Assertions也可以同时做类似程度的更改。因此，当设计和Assertions都已经成功下到RTL层时，这些相同的Assertions就可以拿来当作动态正式分析的目标物，其目的是为了能够帮助交易层测试的自动化。
达成完善修复的终极验证
如果可以同时使用Dynamic Formal Verification以及Constrained-Random的测试平台，将可以大幅提升CDV的价值，因为可以利用相同的激励来衍生出大量的情况。除此之外，运用DFV来分析某仿真工作里多重的情况，代表可以减少附加在测试平台上面的旋钮以及开关的数量，也因此DFV帮使用者省去了极可观自行生出程序码的时间，如此一来让写测试平台的工作简化了许多。
另一方面，利用Constrained Random Simulation搭配Dynamic Formal Analysis更可以让每一个测试本身能够达成更高的功能性覆盖率。综上所述，都是为了完成验证的终极目的，不论在多么复杂的设计里面，个别案例错误都能够更轻易地被发现并且被修复。
