EDA 形式化验证
motivation: 由于本人本质上还是爱好实用主义，但是同时又非常欣赏数学的美感，于是决定学习更应用的数学。（diff from pure math, as far as I know now）听说 EDA 形式化验证和我的研究方向有些联系，遂决定写点科普文，边写边学习。
EDA 就是 Electronic Design Automation, 即电子设计自动化，是用软件辅助芯片和电路的设计、仿真、验证和制造。
芯片：大致可以理解成集成电路(Integrated Circuit, IC). 但是完整芯片通常还包含封装与接口。
IC: 把晶体管、电阻等原件制造并连接在一小块半导体上的完整电路。
电路：由电源、导线和电子元件连接形成的路径，用于传输、处理或控制电信号。
完整电路：元件连接齐全、能实现预定功能。
半导体（Semiconductor）: 导电能力介于导体和绝缘体之间，且可被电压、温度、光或者掺杂控制的材料，比如硅。半导体的导电性可以人为控制，不全是材料本身的性质。
晶体管：是用小电信号控制较大电流的半导体器件，主要充当开关或放大器，是芯片的基本单元。
芯片设计：设计 IC 的功能、逻辑与物理结构，并确保它可制造、性能达标。
芯片仿真（Simulation）：在电脑中运行芯片设计模型，输入测试信号，观察输出与时序是否符合预期，从而在制造前发现错误。
芯片验证（Verification）：在制造前确认设计符合规格。主要包括仿真（Simulation）、形式化验证（Formal Verification）和硬件仿真（Emulation）。
形式化验证（Formal Verification）用数学模型与逻辑证明，检查设计在所有可能输入和状态下是否满足指定性质。通常：读取RTL，编写SVA性质与约束，工具穷举证明；失败则生成反例，工程师调试后迭代。也常做等价性检查，并与仿真配合。Cadence
RTL（Register Transfer Level，寄存器传输级）是描述数字电路中数据如何在寄存器间传递、处理的抽象层级。通常是文本代码文件，用SystemVerilog、Verilog或VHDL编写，例如.sv、.v、.vhd。
SVA（SystemVerilog Assertions）是用来描述、检查芯片时序行为与设计性质的断言语言，常用于仿真和形式化验证。