【数字IC验证学习------- SOC 验证 和 IP验证和形式验证的区别】

formal 验证

Formal验证是芯片设计流程中不可或缺的数学验证手段，以穷尽性证明弥补仿真的覆盖盲区
、— 形式验证 主要有两个检查方向 一个是 逻辑等价性 另一个是功能等价性
​类型​​应用场景​​代表工具​​等价性检查​验证RTL综合后网表功能不变（如时钟门控修改）Synopsys Formality, Cadence LEC​属性检查​验证设计是否满足功能属性（如仲裁公平性、FIFO无溢出）Jasper Gold, VC Formal

等价检查 本质上是数学函数的比对
Synopsys 工具将RTL或者网表解析成逻辑堆 工具会通过SAT求解器，穷举出所有的的输入组合，确定两个fref(x) = fimpl(x）

属性检查 主要是对功能的验证
主要是依据设计提供的SVA 断言来判断，设计的关键性功能是否正确，更加聚焦在比如说仲裁器是否可以公平分配，AXI总线是否会遵守握手协议，状态机死锁

• ​等价检查是“保险丝”，守护设计流程中的功能一致性；
• ​属性检查是“探照灯”，用数学穷举确保设计符合意图规范。二者构成芯片可靠性的双支柱。

IP验证

IP验证又可以分为算法类验证和协议类验证，采用的验证方法大同小异。目前来讲还是以覆盖率(coverage)收敛为导向。IP验证工程师主要做得事情有：
a. 读spec，列测试计划(testplan);
b. 设计验证环境架构，搭建验证环境；
c. 根据测试计划，设计测试用例；
d. 收集code coverage 和function coverage；
e. 测试IP性能。

SOC验证

用户列出的项目（a-k）全面覆盖SoC验证关键任务，具体技术细节如下：

• ​a. 测试计划​：定义功能覆盖率目标（如PCIe协议覆盖点）和测试策略。

• ​b. BootROM测试​：验证复位向量跳转、初始化代码（如时钟/PLL配置）。

• ​c. IP集成测试​：检查IP间协同（如CPU通过AXI总线访问DDR控制器）。

• ​d. 总线互连测试​：使用VIP（Verification IP）模拟总线协议（AHB/APB）的仲裁与死锁场景。

• ​e. 时钟/复位测试​：

• 时钟切换：验证PLL动态调频时的时序收敛性。

• 复位类型：硬复位（Power-on Reset）与软复位（寄存器触发）的恢复时序。

• ​f. 电源管理测试​：基于UPF/CPF验证低功耗状态转换（如Sleep→Active）的电压域控制。

• ​g. 性能测试​：量化总线吞吐量（如DDR带宽）、中断延迟。

• ​h. 功耗测试​：通过PTPX等工具反标门级网表活动率，估算动态功耗。

• ​i. 电源连接性​：形式化验证UPF定义的电源网络开关逻辑。

• ​j. 网表功能测试（Post-sim）​​：带时序反标的门级仿真，检查关键路径时序违例。

• ​k. 覆盖率收集​：合并代码覆盖率（Line/Branch）与功能覆盖率（如AHB传输类型组合）

一、IP验证的核心逻辑：模块级功能完备性​
1.​验证目标​

• ​功能正确性​：确保单个IP（如AXI总线、DDR控制器）在所有设计场景下行为符合Spec，包括正常操作、边界条件（Corner Case）和异常处理（如FIFO溢出）。
• ​覆盖率驱动​：以代码覆盖率（Code Coverage）​​ 和功能覆盖率（Function Coverage）​​ 作为验证完备性的核心指标（例：是否覆盖所有状态机跳转、数据路径组合）。
  2.​方法学与工具​
• ​UVM主导​：通过标准化验证组件（Driver/Monitor/Scoreboard）构建测试平台，生成随机激励并自动检查响应。
• ​形式验证补充​：对控制密集型逻辑（如仲裁器公平性）进行数学穷举证明。
• ​验证结束标志​：覆盖率达标（通常要求>95%）且无未解决Bug。
  3.​​“Golden IP”的假设前提​
• IP交付SoC时被视为“Golden”，隐含条件：
• 覆盖率已收敛，且所有测试用例通过；
• 接口时序和协议合规性已充分验证。

---

✅ ​二、SoC验证的本质：系统级协同与真实场景模拟​
1.​验证焦点转移​

• ​IP集成正确性​：验证IP间互连（如AXI总线仲裁）、时钟域穿越（CDC）、全局复位序列。
• ​系统行为​：关注CPU启动流程（BootROM加载）、外设驱动、中断调度、电源状态切换（如Sleep→Active）。
• ​真实场景模拟​：通过C/ASM程序模拟实际应用（如操作系统启动、数据传输），而非模块级功能。
  2.​技术手段​
• ​软件主导验证​：编译C代码为二进制，加载至Flash/RAM模型，由CPU执行驱动外设。
• ​硬件加速与仿真​：超大规模设计（>2000万门）采用Palladium/Zebu等硬件仿真器，提升测试速度1000倍以上。
• ​形式验证的有限应用​：仅针对系统级属性（如死锁检测、电源管理协议）。
  3.​IP的“Golden”属性与潜在冲突​
• ​默认假设​：SoC验证基于IP功能正确，聚焦集成问题​（例：IP地址映射错误、时钟门控信号遗漏）。
• ​假设失效场景​：若SoC测试发现IP功能缺陷（如DDR控制器时序违例），需回归IP验证并重新交付。