形式验证 动态－形式化混合验证
为了更好的发挥形式化验证技术全面 性的特点，在处理大型设计、更加广 泛的设计风格的设计时使用。 （符号 仿真、半形式化仿真 ）
软、硬件协同验证 硬目的性验证——动态验证技术 ——
概念：对一个模块施加激励信号并由这个模块产生响应信号的过程。在确 定性仿真中，激励信号被明确给出，而且模块的响应信号能够预知并被检 测到。 基于事件的仿真：基于事件的软件仿真器通过事件的发生（一次一个事件） 和在设计中进行传播而进行操作直至获得一个稳定的状态。该设计方案的 模块包含内部周期时钟的概念和功能性的概念。输入的激励信号的任何变 化都将作为事件被检测到，并将被传遍设计的每个阶段。由于输入信号的 到达不同时和底层被测元素的信号的反馈不同时，可以在每个时钟周期对 设计的某个元素评估多次。虽然这能提供高精度的仿真环境，但执行速度 有赖于设计的规模，在大型的设计中其验证速度会相应降低。 基于周期的仿真：基于周期的仿真采用了不同的方法。这种仿真不再具有 内部周期时钟的概念，它在单个周期中对状态及/或各端口之间进行逻辑评 估。由于每个逻辑元素在每个周期中只赋值一次，因此这种方法极大地缩 短了执行时间。
8
目的性验证——动态验证技术 目的性验证——动态验证技术 ——
硬件加速 硬件加速是特指为加速某些仿真操作而将设计中部分或全部的模块映射 到硬件平台上。最典型情况就是测试平台仍然保留在软件中运行，而被 验证的设计却是在硬件加速器中运行。有些类型的加速器也能运行行为 级的代码，这种情况下，具体的时钟周期的行为表现并没有给出详细的 说明，因此，有可能会全部在硬件加速器中运行纯确定性或随机模式仿 真。 硬件建模 有些软件仿真模型的设计元件难以实现，或者不够精确。解决这个难题 的方法就是运行硬件模型中的一个半导体元件，将它连接到软件仿真器 上。这个硬件模型的输入是接收来自仿真器的信号，然后将该信号送到 半导体元件中运行一个周期，最后获得输出信号并将它送回仿真器。
13
目的性验证——硬件仿真 硬件仿真 目的性验证
硬件仿真器是通常由某些可重构逻辑（通常为现场可编程门阵列， 如FPGA）组成的专门设计的硬件和软件系统。编程这些系统以模 仿设计目标的行为和功能，甚至达到将仿真过的设计同设计即将在 其中操作的系统的剩余部分直接连接的程度。 由于这些系统是以硬件为基础的，因此，它们能够提供与最终设计 目标接近的电路仿真速度。这些几千Hz的速度同以软件为基础的仿 真所提供的几十Hz的速度形成鲜明的对比。这种几个量级的行为差 异使得模拟技术能够执行在软件硬件仿真时要用几个月甚至几年才 能完成的大型验证任务。这种验证任务的例子包括数据集的处理如 视频数据流等，或者是有成千上万行的软件如操作系统的引导程序 等。在带有嵌入式处理器的SoC在转化至硅片之前，在软件在与周 围逻辑协同工作时，需要硬件仿真技术或样机技术对软件在嵌入的 处理器上运行时的复杂功能进行验证。正因为这样，通常认为这种 硬件仿真系统在并行设计流程中是介于硬件和软件之间的。
功能验证技术
概述
验证的基本概念 验证：保证某种形式的转换是符合我们所期望的。它是一 个复杂的过程。 功能验证：保证设计正确的实现了规范所定义的功能。 形式验证：形式验证采用数学的方法来验证一个设计的不 同描述是等价的。平等性检测、模型检测。 验证平台（Testbench)：一段代码用来对一个设计产生预 先决定了的输入序列，然后选择性的观察响应，是一个封 闭式的系统。
概述
功能验证与芯片测试的差别
1. 2. 3. 4. 验证要解决的问题
这个设计的功能是否正确？
测试要解决的问题
一个正确的设计，在物理实 现过程中是否有制造缺陷？
HW Design
Manufacturing
二者的相同点
施加激励---〉观看响应
二者的不同点
验证施加的激励要人来编写 测试施加的激励是工具自动 产生的，响应也是自动计算 出来的。整个过程完全的自 动化。
14
目的性验证——硬件仿真 硬件仿真 目的性验证
有很多不同的体系结构都借用这种硬件仿真系统来提供灵活性、可控性、 可视性和性能。这些体系结构包括FPGA的互联阵列，自定义处理器阵列， 带有可编程纵横切换器的磁头系统和可编程总线接口的系统等。这些不同 的体系结构能够在设计容量、行为特性和最优布局结构方面能提供一定程 度的折衷方案，并且力图能够兼容并辅助包括其他验证技术如软件模拟、 时序验证、形式化验证和逻辑分析的验证方法。 硬件仿真器在某种程度上可以看作有限精度的样机。通常硬件仿真器支持 对设计的内部节点保持高度的可观察性，使设计在更类似于模拟而非真实 物理样机的方式除错。事实上，因为软件模拟器与仿真器交互工作的方式 在本质上与硬件模拟加速器相同，有时仿真器也用作模拟目的。 虽然硬件仿真器有时候能够接近最终设计的速度，但是，除非它们能够同 与最终设计一样的系统相联，否则，它们的速度仍将受到限制。另外，硬 件仿真系统的成本往往限制了一个项目中允许的系统数目，反过来，这又 限制了能够同时运行硬件仿真的工程师的数目。
10
目的性验证——形式验证 目的性验证——形式验证 ——
形式验证利用数学方法对设计结果的功能进行验证。它依赖于对设 计的数学分析，无需使用验证测试序列。适用于目的性验证和等价 性检验。 性能/模型验证
性能/模型验证是运用公式化的数学技巧来校验设计的功能特性。模型验证器搜索 一个设计在所有可能条件下的状态空间，去寻找通过仿真很难发现的缺陷。 模型验证不需要建立任何测试平台，其要验证的性质是用以特殊的规范语言描述 的查询表形式。当模型验证工具发现错误的时候，它会产生自初始状态开始，到 行为或特性出错的地方为止的完全搜索路径。 包含数据通道的系统经常包含很大很广的状态空间，对这样的系统进行验证就花 费昂贵的存储空间和大量的处理时间。所以模型验证通常在控制密集设计的验证 中比数据通道密集设计验证更加有效。 模型验证者通常能够在各种合法输入序列和合法的输入状态下，如模型验证和性 能一样可以直接从仿真验证出某种特定的条件总是真，最终为真还是永远不会是 真。这种性质就是对设计的断言，对仿真和模型验证都十分有用。 断言表明了某些特定条件必须总是正确，就将该条件列入checker的职能范围之内， 一旦在仿真中这种条件有偏离，checker就会报告错误。
Specificati on
Verification
Netlist Testing
Silicon
图 3 验 验 验 验验 验 验 验 验 验
概述
功能验证分类 从验证方法上分：
目的性验证 目的是验证设计所试图完成的功能在设计中已正确实现。最典型的 情况是在抽象程度最高的层次完成，其最终结果是建立一套“黄金 模型”，它可以在整个设计过程中作为设计细节的参考。 等价性验证 目的是验证设计过程中产生的不同层次的设计结果功能是否符合 “黄金模型”。
11
目的性验证——形式验证 目的性验证——形式验证 ——
理论证明
基于理论证明技术的验证系统通常支持某种基于选定形式的逻辑的规范语言，并支持 一组以该语言命令的形式机械地构造逻辑断言的证明。 一个使用基于理论证明技术的验证系统的硬件设计的形式化验证，通常包含：对设计 模型(M)的初步描述，将由验证系统支持的逻辑/规范语言的性能（P）的初步描述。在 所有可能的输入条件下M能够正确地推出P的断言，从而验证性能P。证明标准的完备 性保证了在所有可能的输入状态下，该设计的性能都是正确的。 已经有很多的理论证明系统在大型的设计中得以成功地运用，如在浮点指针单元和在 复杂流水控制中。 同模型校验一样，理论证明验证也不需要创建任何验证测试平台，但是需要有待证明 的性能公式。与模型校验不一样的是，理论证明验证不受输入规模和状态空间的限制。 因此，理论证明验证更加适于基于数据通道的设计和高层应用的功能验证，如浮点指 针单元和复杂流水控制中冒险的验证等。同时，理论证明验证还能用于性能检查中， 就如同在一个设计的两个模型之间的等价性校验一样。但是对两个模型的等价性检验 而言，在运用系统验证语言对两个模型进行描述之后，还得给两个模型写一个合适的 断言并对之加以证明。 通过理论证明的验证的主要缺点就是它不如模型校验那样自动化程度较高。因为在通 过理论证明的验证中，用户必须使用理论证明的命令进行交互式的证明。同时，另一 个缺点就是在对某事件的证明失败时，验证系统无法自动构造搜索指针。用户必须通 过人为的分析来寻找错误发生的原因。 12
概述
验证面临的挑战
1. 验证的主导地位 SOC设计的关键是IP复用，IP复用的关键是信任，信任的关键 是完整正确的验证。 在当今百万门级的ASIC，IP，SoC设计中，验证消耗了大约70% 的设计努力。 用于验证的工程师的人数是RTL设计工程师的两倍。 当一个设计完成的时候验证代码的长度占总代码长度的80%。 2. 验证要解决的问题 如何保证验证是充分的？ 如何实现验证的自动化？
7
目的性验证——动态验证技术 目的性验证——动态验证技术 ——
随机模式仿真
随机地址和随机控制信号被加入总线或信号流中，而且有一个或多个总 线监测器对这些信号进行监控，以确保总线协议不会因为这些操作而产 生误操作。这种方法对总线验证尤其适用。 验证测试序列是直接的，因为操作周期的产生并非纯粹的随机产生，而 是以某种特殊的方式来强调设计。这种向量发生器可用来以特定的分配 产生特定的传输周期，如：在伪随机序列中产生20％的读，30％的写和 50％的变址读写。 类似的，在数据和地址领域中也可产生随机序列，但 是得在有限的范围内使用有限的离散数值。 这些类型的仿真验证用确定性仿真很难验证的临界状态、临界序列以及 依赖于数据的状态。用这种方法，任何算法错误都能在设计周期的早期 就能被发现和更正。
从验证对象上分：
IP验证 对某个IP的功能（如：单元测试）进行验证的过程。 系统验证 对包含一个或多个IP的SoC进行功能验证的过程。
5
概述
适合目的性验证技术 动态验证 动态验证是在一系列激励的作用下，对以下几个方