SoC的功能验证
随着设计的进行，越接近最后的产品，修正一个设计缺陷的成本就会越高。
不同设计阶段修正一个设计缺陷所需费用示意图
1.功能验证概述
在IC设计与制造领域，通常所说的验证（Verification）和测试（Test）是两种不同的事
验证
- 在设计过程中确认所设计的正确性
- 通过软件仿真、硬件模拟和形式验证等方法进行
- 在流片之前要做的。
测试
- 检测芯片是否存在制造或封装过程中产生的缺陷。
- 采用测试设备进行检查
功能验证
功能验证一般是指设计者通过各种方法比较设计完成的电路和设计文档规定的功能是否一致，保证逻辑设计的正确性。
通常不包括面积、功耗等硬件实现的性能检测。
SoC功能验证的挑战
- 系统复杂性提高增加验证难度
- 设计层次提高增加了验证工作量
发展趋势
2.功能验证方法与验证规划
仿真为基本出发点的功能验证方法
功能验证开发流程制订验证计划
- 功能验证需求
- 激励产生策略
- 结果检测策略
验证开发
- 提高验证的效率
功能验证开发流程
3.系统级功能验证
行为级功能验证
测试数据控制流，包括初始化和关闭I/O设备、验证软件功能、与外界的通信，等等
性能验证
通过性能验证可以使设计者清楚地知道整个系统的工作速度、功耗等性能方面的指标。
协议验证
根据总线协议对各个模块的接口部分进行验证
系统级的测试平台
- 边界条件
- 设计的不连续处
- 出错的条件
- 极限情况
系统级的测试平台标准
- 性能指标
- 覆盖率指标
4.仿真验证自动化
激励的生成
- 直接测试激励：检测到测试者所希望检测到的系统缺陷
可以快速、准确地产生大量的与实际应用一致的输入向量
- 随机测试激励：
检测到测试者没有想到的一些系统缺陷带约束的随机测试激励是指在产生随机测试向量时施加一定的约束，使所产生的随机测试向量满足一定的设计规则。
带约束的随机激励生成的例子
x1和x2为系统的两个输入，它们经过独热码编码器编码之后产生与被验证设计（DUV）直接相连的输入
输入约束：in[0] + in[1] + in[2] <= 1
这样产生的随机向量就可以保证它们的合法性。
用SystemVerilog语言写的带约束随机激励生成例子
输入data的数量限制在1～1000
program automatic test;
// define constraint
class Transaction;
rand bit [31:0] src, dst, data[]; // Dynamic array
randc bit [2:0] kind; // Cycle through all kinds
constraint c_len
{ data.size inside {[1:1000]}; } // Limit array size
Endclass
// instantiation
Transaction tr;
// start random vector generation
initial begin
tr = new();
if(!tr.randomize()) $finish;
transmit(tr);
end
endprogram
响应的检查
- 可视化的波形检查：直观，但不适用于复杂系统设计
- 自动比对检查：通过相应的检测模型或验证模型来自动完成输出结果的比对
覆盖率的检测
- 覆盖率数据通常是在多个仿真中收集的.
- 覆盖率的模型由针对结构覆盖率（Structural Coverage）和功能覆盖率（Functional Coverage）两种目标而定义的模型所组成。
可细化为：
限状态机覆盖率（FSM Coverage） 表达式覆盖率（Expression Coverage） 交叉覆盖率（Cross Coverage） 断言覆盖率（Assertion Coverage）
用SystemVerilog语言写的覆盖率检测的例子
program automatic test(busifc.TB ifc);
class Transaction;
rand bit [31:0] src, dst, data;
rand enum {MemRd, MemWr, CsrRd, CsrWr, I
oRd, IoWr, Intr, Nop} kind;
endclass
covergroup CovKind;
coverpoint tr.kind; // Measure coverage
endgroup
Transaction tr = new(); // Instantiate transaction
CovKind ck = new(); // Instantiate group
initial begin
repeat (32) begin // Run a few cycles
if(!tr.randomize()) $finish;
ifc.cb.kind <= tr.kind; // transmit transaction
ifc.cb.data <= tr.data; // into interface
ck.sample(); // Gather coverage
@ifc.cb; // Wait a cycle
end
end
endprogram
5.形式验证
形式验证（Formal Verification）
静态形式验证（Static Formal Verification）和半形式验证（Semi-Formal Verification）
- 静态形式验证不需要施加激励，也不需要通过仿真来验证。目前，SoC设计中常用的静态形式验证方法是相等性检查。
- 半形式验证是一种混合了仿真技术与形式验证技术的方法。常用的半形式验证是混合属性检查或模型检查，它将形式验证的完整性与仿真的速度、灵活性相结合。
相等性检查（Equivalent Check）
- 对设计进行覆盖率100％的快速验证
- 主要是检查组合逻辑的功能相等性
- 不需要测试平台和测试矢量，不需要进行仿真
- 可用于比较RTL与RTL、RTL与门级、门级与门级的功能相等性，被广泛应用于版图提取的网表与RTL代码比较，特别是做完ECO后要进行网表和修改后的RTL的相等性检查。
半形式验证（Semi-Formal Verification）
仿真和形式验证形结合，如混合模型检查（Model Checking）或属性检查（Property Checking）的方法。
6.基于断言的验证
仿真验证面临的问题：可观测性和可控制性
- 合适的输入矢量能够激活错误
- 错误要能够以某种预期的形式输出
采用断言描述设计的行为，在仿真时起到监控作用，当监控的属性出现错误时，立刻触发错误的产生，增加了设计在仿真时的可观测性问题。
也可以用在形式属性检查中作为要验证的属性。属性检查（Property Check）时，是对整个状态空间进行搜索，能够控制到每一个信号并能指出错误的具体位置，解决了设计验证时的可控制性和可观察性问题。
验证实现所花费的时间与验证的质量
断言的作用
断言语言及工具的使用
断言语言
C or SystemC SystemVerilog Assertion (SVA) Property Specification Language (PSL) (IBM, based on Sugar) Open Verification Library (OVL) Verilog, VHDL
SVA（SystemVerilog Assertion）例子
用Verilog实现的检查器：
always @ (posedge A)
begin repeat (1) @ (posedge clk);
fork: A_to_B
begin @ (posedge B)
$display (“SUCCESS: B arrived in time\n”, $time);
disable A_to_B;
end
begin
repeat (1) @ (posedge clk)
@ (posedge B)
display (“SUCCESS: B arrived in time\n”, $time);
disable A_to_B;
end
begin
repeat (2) @ (posedge clk)
display (“ERROR: B didn’t arrive in time\n”, $time);
disable A_to_B;
end
end
用SVA实现的检查器：
assert property
( @(posedge clk )A|->##[1:2]B);
基于断言的验证
在属性检查中使用断言
在属性检查中，最重要的就是属性描述。
在仿真中使用断言
