哈工大功能验证技术

功能验证技术概述验证的基本概念验证：保证某种形式的转换是符合我们所期望的。它是一个复杂的过程。功能验证：保证设计正确的实现了规范所定义的功能。形式验证：形式验证采用数学的方法来验证一个设计的不同描述是等价的。平等性检测、模型检测。验证平台（Testbench)：一段代码用来对一个设计产生预先决定了的输入序列，然后选择性的观察响应，是一个封闭式的系统。概述验证面临的挑战验证的主导地位SOC设计的关键是IP复用，IP复用的关键是信任，信任的关键是完整正确的验证。在当今百万门级的ASIC，IP，SoC设计中，验证消耗了大约70%的设计努力。

用于验证的工程师的人数是RTL设计工程师的两倍。

当一个设计完成的时候验证代码的长度占总代码长度的80%。

验证要解决的问题如何保证验证是充分的？如何实现验证的自动化？概述验证要解决的问题这个设计的功能是否正确？测试要解决的问题一个正确的设计，在物理实现过程中是否有制造缺陷？二者的相同点施加激励---〉观看响应二者的不同点验证施加的激励要人来编写测试施加的激励是工具自动产生的，响应也是自动计算出来的。整个过程完全的自动化。功能验证与芯片测试的差别5功能验证分类从验证方法上分：目的性验证

目的是验证设计所试图完成的功能在设计中已正确实现。最典型的情况是在抽象程度最高的层次完成，其最终结果是建立一套“黄金模型”，它可以在整个设计过程中作为设计细节的参考。等价性验证

目的是验证设计过程中产生的不同层次的设计结果功能是否符合“黄金模型”。从验证对象上分：IP验证

对某个IP的功能（如：单元测试）进行验证的过程。系统验证

对包含一个或多个IP的SoC进行功能验证的过程。概述6适合目的性验证技术动态验证

动态验证是在一系列激励的作用下，对以下几个方面的测试：一个设计方案的一个或几个模块、某设计的硬件实现等。静态功能验证静态功能验证利用公式化的数学技巧来进行验证而不使用验证测试序列。其测试方法还没有统一的工业标准，说法比较含糊。

形式验证动态－形式化混合验证为了更好的发挥形式化验证技术全面性的特点，在处理大型设计、更加广泛的设计风格的设计时使用。（符号仿真、半形式化仿真）软、硬件协同验证硬件仿真物理样机虚拟样机概述7目的性验证——动态验证技术概念：对一个模块施加激励信号并由这个模块产生响应信号的过程。在确定性仿真中，激励信号被明确给出，而且模块的响应信号能够预知并被检测到。基于事件的仿真：基于事件的软件仿真器通过事件的发生（一次一个事件）和在设计中进行传播而进行操作直至获得一个稳定的状态。该设计方案的模块包含内部周期时钟的概念和功能性的概念。输入的激励信号的任何变化都将作为事件被检测到，并将被传遍设计的每个阶段。由于输入信号的到达不同时和底层被测元素的信号的反馈不同时，可以在每个时钟周期对设计的某个元素评估多次。虽然这能提供高精度的仿真环境，但执行速度有赖于设计的规模，在大型的设计中其验证速度会相应降低。基于周期的仿真：基于周期的仿真采用了不同的方法。这种仿真不再具有内部周期时钟的概念，它在单个周期中对状态及/或各端口之间进行逻辑评估。由于每个逻辑元素在每个周期中只赋值一次，因此这种方法极大地缩短了执行时间。8目的性验证——动态验证技术随机模式仿真随机地址和随机控制信号被加入总线或信号流中，而且有一个或多个总线监测器对这些信号进行监控，以确保总线协议不会因为这些操作而产生误操作。这种方法对总线验证尤其适用。验证测试序列是直接的，因为操作周期的产生并非纯粹的随机产生，而是以某种特殊的方式来强调设计。这种向量发生器可用来以特定的分配产生特定的传输周期，如：在伪随机序列中产生20％的读，30％的写和50％的变址读写。类似的，在数据和地址领域中也可产生随机序列，但是得在有限的范围内使用有限的离散数值。这些类型的仿真验证用确定性仿真很难验证的临界状态、临界序列以及依赖于数据的状态。用这种方法，任何算法错误都能在设计周期的早期就能被发现和更正。9目的性验证——动态验证技术硬件加速硬件加速是特指为加速某些仿真操作而将设计中部分或全部的模块映射到硬件平台上。最典型情况就是测试平台仍然保留在软件中运行，而被验证的设计却是在硬件加速器中运行。有些类型的加速器也能运行行为级的代码，这种情况下，具体的时钟周期的行为表现并没有给出详细的说明，因此，有可能会全部在硬件加速器中运行纯确定性或随机模式仿真。

硬件建模有些软件仿真模型的设计元件难以实现，或者不够精确。解决这个难题的方法就是运行硬件模型中的一个半导体元件，将它连接到软件仿真器上。这个硬件模型的输入是接收来自仿真器的信号，然后将该信号送到半导体元件中运行一个周期，最后获得输出信号并将它送回仿真器。10目的性验证——动态验证技术协议检验协议检验器指的是监测接口的数据处理以及检查任何无效操作的元件。如果在仿真器中有任何无效操作被检验到，检验器将会作标记。这种元件可以装备在测试平台中而不作为设计的部分。在这种应用中，检验器仅仅在仿真时才起作用。当然，协议检验器也可以植入设计之中，这样检验器不仅可以在仿真的时候，而且可以在实际的物理设备进行的普通操作中都能查错。不过，设计中植入的这种设备要能够在门级进行综合。预期结果检验是系统测试平台的一部分。它对仿真结果与事先的规定——期望响应文件进行比较。如果结果不符，将会报错。11目的性验证——形式验证形式验证利用数学方法对设计结果的功能进行验证。它依赖于对设计的数学分析，无需使用验证测试序列。适用于目的性验证和等价性检验。性能/模型验证

性能/模型验证是运用公式化的数学技巧来校验设计的功能特性。模型验证器搜索一个设计在所有可能条件下的状态空间，去寻找通过仿真很难发现的缺陷。模型验证不需要建立任何测试平台，其要验证的性质是用以特殊的规范语言描述的查询表形式。当模型验证工具发现错误的时候，它会产生自初始状态开始，到行为或特性出错的地方为止的完全搜索路径。包含数据通道的系统经常包含很大很广的状态空间，对这样的系统进行验证就花费昂贵的存储空间和大量的处理时间。所以模型验证通常在控制密集设计的验证中比数据通道密集设计验证更加有效。模型验证者通常能够在各种合法输入序列和合法的输入状态下，如模型验证和性能一样可以直接从仿真验证出某种特定的条件总是真，最终为真还是永远不会是真。这种性质就是对设计的断言，对仿真和模型验证都十分有用。断言表明了某些特定条件必须总是正确，就将该条件列入checker的职能范围之内，一旦在仿真中这种条件有偏离，checker就会报告错误。12目的性验证——形式验证理论证明基于理论证明技术的验证系统通常支持某种基于选定形式的逻辑的规范语言，并支持一组以该语言命令的形式机械地构造逻辑断言的证明。一个使用基于理论证明技术的验证系统的硬件设计的形式化验证，通常包含：对设计模型(M)的初步描述，将由验证系统支持的逻辑/规范语言的性能（P）的初步描述。在所有可能的输入条件下M能够正确地推出P的断言，从而验证性能P。证明标准的完备性保证了在所有可能的输入状态下，该设计的性能都是正确的。已经有很多的理论证明系统在大型的设计中得以成功地运用，如在浮点指针单元和在复杂流水控制中。同模型校验一样，理论证明验证也不需要创建任何验证测试平台，但是需要有待证明的性能公式。与模型校验不一样的是，理论证明验证不受输入规模和状态空间的限制。因此，理论证明验证更加适于基于数据通道的设计和高层应用的功能验证，如浮点指针单元和复杂流水控制中冒险的验证等。同时，理论证明验证还能用于性能检查中，就如同在一个设计的两个模型之间的等价性校验一样。但是对两个模型的等价性检验而言，在运用系统验证语言对两个模型进行描述之后，还得给两个模型写一个合适的断言并对之加以证明。通过理论证明的验证的主要缺点就是它不如模型校验那样自动化程度较高。因为在通过理论证明的验证中，用户必须使用理论证明的命令进行交互式的证明。同时，另一个缺点就是在对某事件的证明失败时，验证系统无法自动构造搜索指针。用户必须通过人为的分析来寻找错误发生的原因。13目的性验证——软、硬件协同验证在传统的系统设计的串行流程中，首先构造硬件，然后在硬件的基础上编写和调试系统软件。但是在软、硬件联合验证技术中，对系统硬件和软件的验证是同时进行的。在硬件被开发的同时，相应的软件也在硬件仿真平台中执行，这样就实现了硬件和软件的并行调试。虽然协同验证环境的建立需要大量的时间和丰富的经验，但是使用软、硬件联合验证技术的回报也是十分丰厚的。首先，使用软、硬件协同验证技术能够在SOC芯片制造之前就能发现并纠正许多系统级漏洞和问题。在实际的处理器和固件模型中进行的仿真，结果会更加精确，而且同旧的使用总线传输模型的设计流程比较起来，可以进行更广泛的验证。而且，在仿真过程中，软件也得到了调试和验证。相应的允许在芯片实际生成的同时，给系统的发展提供较高的发展速度。最终结果是，软、硬件协同验证技术通过在设计的早期就很快的解决了问题而提高了整个产品开发周期的质量，节省了时间和金钱。

14目的性验证——硬件仿真硬件仿真器是通常由某些可重构逻辑（通常为现场可编程门阵列，如FPGA）组成的专门设计的硬件和软件系统。编程这些系统以模仿设计目标的行为和功能，甚至达到将仿真过的设计同设计即将在其中操作的系统的剩余部分直接连接的程度。由于这些系统是以硬件为基础的，因此，它们能够提供与最终设计目标接近的电路仿真速度。这些几千Hz的速度同以软件为基础的仿真所提供的几十Hz的速度形成鲜明的对比。这种几个量级的行为差异使得模拟技术能够执行在软件硬件仿真时要用几个月甚至几年才能完成的大型验证任务。这种验证任务的例子包括数据集的处理如视频数据流等，或者是有成千上万行的软件如操作系统的引导程序等。在带有嵌入式处理器的SoC在转化至硅片之前，在软件在与周围逻辑协同工作时，需要硬件仿真技术或样机技术对软件在嵌入的处理器上运行时的复杂功能进行验证。正因为这样，通常认为这种硬件仿真系统在并行设计流程中是介于硬件和软件之间的。15目的性验证——硬件仿真有很多不同的体系结构都借用这种硬件仿真系统来提供灵活性、可控性、可视性和性能。这些体系结构包括FPGA的互联阵列，自定义处理器阵列，带有可编程纵横切换器的磁头系统和可编程总线接口的系统等。这些不同的体系结构能够在设计容量、行为特性和最优布局结构方面能提供一定程度的折衷方案，并且力图能够兼容并辅助包括其他验证技术如软件模拟、时序验证、形式化验证和逻辑分析的验证方法。硬件仿真器在某种程度上可以看作有限精度的样机。通常硬件仿真器支持对设计的内部节点保持高度的可观察性，使设计在更类似于模拟而非真实物理样机的方式除错。事实上，因为软件模拟器与仿真器交互工作的方式在本质上与硬件模拟加速器相同，有时仿真器也用作模拟目的。虽然硬件仿真器有时候能够接近最终设计的速度，但是，除非它们能够同与最终设计一样的系统相联，否则，它们的速度仍将受到限制。另外，硬件仿真系统的成本往往限制了一个项目中允许的系统数目，反过来，这又限制了能够同时运行硬件仿真的工程师的数目。16目的性验证——物理样机一种目标设计的硬件代替品，它的运行能够“接近”目标设计平台的性能。执行速度能够比软件仿真系统的速度快出许多。物理样机能够支持以下功能：在SOC器件可用之前，应用软件和系统软件的开发和调试系统的系统级性能测试目标设计的高性能仿真平台，该设计能支持复杂测试周期具有支持硬、软件联合仿真的硬件平台和软件环境用于测试的逻辑分析接口目标设计的市场演示典型情况下，物理样机可与目标系统速度相同的数量级范围内运行，因此，它的执行速度能够比软件仿真系统的速度快出许多。这意味着全部的测试序列都能够装载到物理样机中去，并同系统级验证测试向量一起运行。在考虑到可以样机化的设计的数目、执行速度以及性能变化时间时，通过不同的方法得到的样机就会有不同的性能。17目的性验证——虚拟样机一个虚拟样机就是一个产品、一个元件或一个系统的计算机模拟模型。同其它基于其自身特性的“模型”术语不一样的是，“虚拟样机”这个术语并不是指任何特殊的模型特性，而指在设计流程中做模型的角色。一般来说，一个虚拟模型应该支持下列任务：试探开发设计的替代品证明设计的概念测试需求的满意度和正确度虚拟样机可以在各个抽象的层次上构建也可以包含一个多层次的混合体。在一个设计系统中可以有一个和几个虚拟样机同时存在，每个虚拟样机都能完成上述所说的任务。为了能在更大的设计系统中发挥作用，一个虚拟样机应该对设计的元件或系统的接口进行定义。物理样机需要有详细的硬件和软件设计描述，而虚拟样机能够更快、更有效、更加抽象而且在设计流程中能够更早的加以构建。因此，其中的一个区别就是，虚拟样机作为一个计算机仿真器，比起物理样机的常规操作来，能提供有关内部状态的更多的，无害的可视化信息。此外，与物理样机相比较而言，虚拟样机的一个主要缺点就是，它的操作速度同软件仿真器的速度十分接近，因此就限制了在一定的时间内所能完成的验证数目。

18等价性验证确定性仿真：给模型施加明确定义的信号，产生相应的响应，在将仿真结果与预期值比较。一旦在RTL级模型上的验证平台和验证测试向量被开发出来，那么同样地验证向量集合也能在门级网表上对原设计进行仿真，以检查结果是否相同。在有些情形下，也有可能在对同样的设计的高层或者低层仿真过程中进行同样的验证测试。预期结果检查：对仿真结果同先前指定了的预期响应文件进行比较。出现任何错误的时候，检查者就会报错。黄金模型检查：监视一个设计中两个模型的响应，将响应信号与输入激励相比较，并且对任何偏差作出标记。其中一个为“黄金模型”或可信任模型，而另外一个则是待证明的模型。一般情况下，这种比较不包括任何形式化验证技术，两个模型之间的响应信号比较仅基于信号的变化。验证测试序列的迁移：把系统级验证测试序列应用到设计的其它层次需要有可以将其迁移或转换为设计的RTL级或网表级应用序列格式的能力。包括：功能级向RTL级的迁移和RTL级向网表级迁移。119等价性验证——形式化等性检验形式化等价性检验工具要证明的是：两个设计从I/O接口和基于一个接一个的周期的角度来看功能上是等价的。形式化等价性检验通常用在设计的RTL级和门级网表级。在有些情形下，也能用于更高或者更低的模型。同软件仿真相比，形式化等价性检验具有几个优点。首先，与仿真不同，形式化等价性检验能够提供完整的等价性检验，而仿真只验证到一个验证测试组是否在设计中运行的程度。另外，形式化等价性检验能够在很短的时间内执行完需要复杂仿真才能完成的任务，这就有利于将验证和错误调试自动化。等价性检验工具通常会提供与小的独立逻辑块不匹配的详细“反例”。

包括布尔等价性检验和时序等价性检验。20等价性验证——形式化等性检验布尔等价性检验许多等价性检验工具是布尔等价性检验器，这意味着它们检验的是组合逻辑。运用这些工具，通常自动进行两个设计的存储元件（如触发器、锁存器等）间格式的比较，从而完成对名词的映射。当映射确定以后，相应的工具就开始对存储器的每对映射名词的输入的组合逻辑开始检查是否等价。这意味着对每一种可能的输入组合，组合逻辑输出（也即存储器元件的输入）是相同的。

时序等价性检验有这样一种情况：两个设计的存储元件的数目不同或排列不同，但是就输入－输出数据流的生成以及在两个状态机之间给定的某些初始状态方面两者是等价的，这就是时序等价。这样的例子如有限状态机的两种实现方式：一个采用全译码方式，即用3个锁存器编码8个状态；另一种采用one-hot编码，用8个锁存器为8个状态编码。然而这两个状态机都有同样的输出/入数据信号，都开始于相同的初始状态，有相同的输入数据流。时序等价性检验比布尔等价性检验存在更大的困难。因此能够执行这种任务的工具更加稀少。有很多的布尔等价性检验确实支持时序等价性检验，允许检验很小的有限状态机（通常用户必须手动地支持一些等价状态赋值的映射，因而限制了这种检验只能适合于小规模的状态机），或者允许检验某些组合逻辑器件跨越存储器元件边界的简单操作。121等价性验证——物理验证物理验证就是通过检验图形设计的数据库以确信物理实现确实是原始逻辑设计的正确表述。物理验证包括以下三个部分：电学规则检验（以下简称ERC）、设计规则检验（以下简称DRC）及布线和电路图检验（以下简称LVS）。标准的图形数据库形式是GDSII－数据流。一个设计的GDSII－数据流数据库包括电路的多边形表述，并对目标设计划分成不同的设计层次。ERC指的是检验图形数据库是否有与电学设计规则相违背之处。这些电学规则就是流程说明，并包含检验是否有无用输入，浮点输入和装载冲突等。还检验连接是否合法，如短路和短接。DRC指的是检验图形数据库是否有与设计流程规则相违背之处。这些规则收集在DRC规则文件中，并包含层与层之间的空间检验、布线宽度、层与层的相互重叠等。LVS就是检验提取的图形数据库是否有与“黄金”网表相违背之处。LVS工具从多边形数据中构建网表以及从物理布局中提取器件模型。提取出的网表需和“黄金”模型保持一致。所有的器件和互连都必须严格地相匹配。其他的影响时序的物理验证如信号的完整性、串扰、金属迁移、噪音等不在功能验证论述的范围内。22验证衡量方法

硬件代码覆盖率：可以在仿真过程中通过硬件代码覆盖率分析工具来评定验证测试序列的覆盖率指标。把特定的测试验证序列输入到特定设计中，通过代码覆盖率分析就有可能得出功能覆盖率的某些方面的信息。分析工具可以提供以下信息：·每个被评估属性的百分比的覆盖率值·设计中没有执行或者只是部分执行的区域的列表代码覆盖率分析通常是在设计流程的RTL级上进行的，评估的是以下类型的覆盖率：

·语句覆盖率：表明每条语句被执行的次数；·信号触发覆盖率：表明设计信号中的哪一位被触发；·有限状态机覆盖率：表明进行了多少个有限状态机的转变过程，可以视为路径覆盖率的一部分；·被访问状态覆盖率：表明有限状态机有多少个的状态参与了仿真；·触发覆盖率：表明每个进程是否被敏感度列表中的每个信号唯一触发到；·分支覆盖率：表明哪一条“case”或者“if…else”语句被执行；·表达式覆盖率：表明“if”条件布尔表达式或赋值布尔表达式的执行的好坏程度；·路径覆盖率：表明通过“if…else”和“case”顺序结构的哪条路径被执行；·信号覆盖率：表明状态信号或ROM寻址的执行的好坏程度。23验证衡量方法功能覆盖率功能覆盖率是一种由用户定义的、反映在验证过程中被运行到的功能点的范围的衡量方法。功能点可以是对VC用户而言可视的体系结构特点，也可以是主要的微结构特征。通常情况下，这些特征不能从实现中自动生成，因此需要在验证testbench中的一些规范。功能覆盖率数据一般是一些时序行为（如总线的交易）和一些数据（如交易源、目的和优先级等）的交叉组合。附加覆盖率信息可以从功能覆盖率点的交叉引用中得到。比如，在一个器件的两个引脚之间进行的数据处理的相互关系，或者在一个处理器中指令和中断的关系等。与代码覆盖率不一样的是功能覆盖率的指标需要开发者自行定义。一个好的定义不仅与验证平台紧密相关，而且应覆盖VC中的所有主要特征。因此，功能覆盖率比代码覆盖率的要求更加严格。经验表明，功能覆盖率与bugs/每周衡量法之间有紧密联系。虽然有些方面可以在更低或者更高的层次上评估，功能覆盖率分析通常还是在设计的RTL级上进行。验证什么？---功能验证textspecificationdesignspecificationdesign??理解RTL实现功能验证验证过程示意图功能验证yesno验证什么？--形式验证形式验证等价性检测：两种不同的结构或者行为描述

在功能上是等价的。模型检测：证明特定结构符合预期的行为门级网表1门级网表2等价性检测：扫描链的插入功能相等？模型检测：文本规范设计应该具有的行为形式化的编程语言设计模型检测形式验证示意图验证的方法方法黑盒子模型白盒子模型灰盒子模型验证的级别单元级的验证：基本模块的验证。

宏单元验证：可复用单元（模块）的验证。IP级别。系统级验证：验证的前提是各个单元模块是已经经过验证