01
形式化验证概述
什么是形式化验证、为什么需要形式化验证、形式化验证与传统仿真对比。
概念对比
02
环境搭建准备
Linux操作系统选择、虚拟机安装、磁盘分区与文件系统规划。
Linux虚拟机
03
基础工具链安装
GCC、G++、Make、CMake、Git版本控制工具安装与配置。
工具链Git
04
Python环境配置
Python3安装、pip包管理器、virtualenv虚拟环境、Jupyter Notebook搭建。
PythonJupyter
05
Tcl/Tk脚本语言
Tcl解释器安装、Tcl基础语法、Tcl在EDA工具中的应用。
TclEDA
06
Verilog/VHDL仿真器
Icarus Verilog(iverilog)安装与测试、GTKWave波形查看器。
仿真波形
07
Yosys开源综合工具
Yosys源码编译安装、基本综合流程、Verilog到BLIF转换。
综合BLIF
08
ABC逻辑综合与验证
ABC工具编译、逻辑优化命令、等价性检查入门。
逻辑优化等价性
09
SymbiYosys形式化框架
SymbiYosys安装、sby配置文件结构、基本验证流程。
框架sby
10
SMT求解器基础
Z3求解器安装、SMT-LIB标准简介、简单的约束求解示例。
Z3SMT
11
Boolean求解器
MiniSat、CryptoMiniSat安装与使用、CNF文件格式。
SATCNF
12
AIG与逻辑网络
AIG(And-Inverter Graph)概念、ABC中的AIG操作、逻辑等价性检查。
AIG等价性
13
有界模型检测(BMC)
BMC原理、SymbiYosys中BMC引擎配置、反例波形分析。
BMC反例
14
无界模型检测(UMC)
k-induction原理、UMC引擎配置、完整证明与收敛性。
UMC归纳
15
属性规范语言
SystemVerilog Assertions(SVA)基础、assert/property/cover指令。
SVA断言
16
SVA进阶语法
序列(sequence)、属性(property)、时钟与复位、多时钟域断言。
序列时钟域
17
覆盖分析与功能覆盖
cover指令使用、覆盖组定义、覆盖率报告解读。
覆盖cover
18
假设保证推理
assume指令、环境约束建模、假设与断言的关系。
assume约束
19
形式化验证项目结构
目录组织规范、Makefile编写、回归测试脚本。
项目结构Makefile
20
RTL代码风格与可验证性
可综合RTL风格、避免x态传播、同步复位vs异步复位。
RTLx态
21
接口协议验证
握手协议建模、AXI-lite协议断言、数据一致性检查。
AXI握手
22
数据通路验证
加法器/乘法器验证、流水线寄存器检查、数据冒险检测。
数据通路冒险
23
状态机验证
FSM编码风格、状态可达性分析、死锁与活锁检测。
FSM死锁
24
存储控制器验证
FIFO满空标志验证、双端口RAM一致性、地址越界检查。
FIFORAM
25
安全属性验证
信息流分析、非干扰模型、机密性属性形式化。
安全信息流
26
等价性检查
组合逻辑等价性、时序逻辑等价性、重定时验证。
等价性重定时
27
形式化验证与仿真协同
仿真波形导入形式化工具、形式化约束用于仿真、混合验证策略。
协同混合
28
性能优化与调试
引擎选择策略、抽象技术、反例分析技巧。
优化抽象
29
持续集成中的形式化验证
Jenkins/GitLab CI集成、每日回归、报告生成。
CI回归
30
综合案例实战
一个完整模块的形式化验证流程、从spec到sign-off的全过程。
实战sign-off