形式化验证简介及
fm_shell脚本编写指南
►►►
形式化验证原理及作用
形式化验证是一种基于数学分析方法的验证技术，它通过算法引擎建立模型，对待测设计的状态空间进行穷尽分析的验证。在芯片设计中，形式化验证主要用于综合前后的等价性检查和RTL设计的功能验证。形式化验证的优势在于它可以提供精确、确定的结论，帮助开发人员减少迭代设计和测试的时间和成本 。
►►►
如何编写一个形式化验证脚本？
要编写一个fm_shell脚本进行形式化验证，
需要准备以下内容：
参考设计（Reference Design）：通常是RTL代码。
待比较设计（Implementation Design）：如综合后的网表。
容器（Containers）：用于存储参考设计和待比较设计，通常使用“r”表示参考设计容器，“i”表示待比较设计容器。
形式化验证相关约束：根据设计需求设置路径约束、常量等。
在fm_shell环境中，
可以使用以下基本指令：
`create_container`：创建新的容器。
`read_verilog`：读取Verilog文件到容器中。
`create_constraint_type`：创建新的约束类型。
`set_constraint`：设置约束条件。
`match`：执行比较点匹配。
`verify`：执行验证操作。
`report`：生成验证报告。
形式化验证的基本流程及参考包括：
Step 0 引导（Guidance）：添加综合产生的.svf文件，记录综合所有信息。
set_svf ./XXX/{DESIGN_NAME}.svfStep 2a 读RTL：读取参考设计与库文件，并设置顶层。
read_verilog -container r "{rtl_verilog_files}"read_sverilog -container r "{rtl_sverilog_files}"read_db “xxx.db”set_top r : /XXX/{DESIGN_NAME}
Step 2b 读网表：读取待比较设计与库文件，并设置顶层。
read_verilog -i ./XXX/{DESIGN_NAME}.syn.vset_top i : /XXX/{DESIGN_NAME}
Step 3 设置约束（Set up）：根据需要设置约束条件。
Step 4 匹配（Match）：执行比较点匹配。
matchreport_unmatched_pointsset_dont_verify {r:/work/xxx/xxx/xx/xxx/shift_x_reg70/\*dff.00.7\*}
Step 5 比对（Verify）：进行验证并生成报告。
verifyanalyze_points failingreport_constantsreport_dont_verify_pointsreport_failing_points > ../rpt/failing_points.rptreport_aborted_points > ../rpt/aborted_points.rptreport_unverified_points > ../rpt/unverified_points.rpt
注：此处省略step 1准备工作及环境配置
形式化验证工具如Cadence的JasperGold和Synopsys的VCFormal等，提供了丰富的功能和自动化程度高的操作，使得形式化验证在芯片设计中发挥着重要作用 。
✦
✧
END
✦
