形式验证的目的是比较功能的一致性比对综合后的网表netlist和RTL设计的功能是否一致比对PR后的网表和综合后网表功能是否一致。两处比对一致则代表最终PR后的网表功能符合设计者意图。在所有的IC设计中想要最终成功的设计者都不会放弃做形式验证且至少需要两次形式验证第一次是RTL和综合后的网表的比对这次比对简记为前FM第二次是综合后的网表和PR后的网表的比对这次比对简记为后FM。1 FM的逻辑框架不论是前FM还是后FM做形式验证的思路是一样的需要的东西如下1 参考文件就是那个被定义为永远正确的文件这里用ref来表示这里的ref文件就是RTL设计文件原因RTL经过功能仿真验证被认为RTL是符合设计者意图的正确设计2 用于比较的文件这里用imp来表示这里imp文件就是综合后的网表文件原因在综合过程中综合软件会对设计进行优化有些地方的优化可能不符合设计者意图从而导致功能错误3 明白ref文件和imp文件的底层表达ref文件是RTL的代码文件而imp文件是用具体器件表示的网表因此两者之间需要读入具体的器件的db文件软件才能明白文件具体想表达的意思。与此同时在综合过程中进行了优化也需要把优化的记录文件.svf文件读入软件才能比对优化处的功能2 FM的简单实现下面给出一个简单的FM的脚本在进行复杂的芯片验证时可在此基础框架上增删修改。步骤1设置顶层文件名字这个可以给自己提示该脚本是用于那个项目/模块的set top_design_name top_design_name步骤2设计FM的约束条件最开始约束条件可以不用设置用默认设置debug的时候可以加上。约束条件还有很多或者多种用法可参见使用手册和使用man指令set verification_failing_point_limit 0set hdlin_warn_on_mismatch_message {FMR_ELAB-147 FMR_VLOG-091}set verification_clock_gate_hold_mode anyset hdlin_ignore_full_case falseset hdlin_ignore_parallel_case falseset hdlin_unresolved_modules black_box……步骤3读入相应的db文件read_db ../../xxx.db步骤4 读入综合后的优化文件#set_synopsys_setup trueset_svf ../../../../xxxx.svf步骤5读入RTL设计文件到-r container里read_verilog -container r -libname WORK {module_a.v module_b.v module_c.v}set_top r:/WORK/$design_top_nameset_refernce r:/WORK/$design_top_nameset hdlin_unresolved_modules black_box步骤6读入网表文件到-i container里read_verilog -i libname WORK -05 ../../xxxxx.vgset_top i:/WORK/$design_top_nameset_implementation i:/WORK/$design_top_name步骤7将i-container和r-container里的内容进行匹配比对matchreport_unmatched_pointsset_dont_verify {r:/work/xxx/xxx/xx/xxx/shift_x_reg70/\*dff.00.7\*}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注1查找使用的命令用man比如 man read_verilog就会出来具体命令的使用方法注2关于formality的使用手册可在eetop社区里找到如下链接简单的应用框架在第81页。Formality® User Guide 2022-03 - 后端资料区 - EETOP 创芯网论坛 (原名电子顶级开发网) -注3formality的用户手册里可以找到相应的脚本模板3 start_guidebug工具可以通过FM的gui界面进行debug这个界面上存在问题分析、可能原因定位、电路的比较图对于debug很友好。用户手册里也有很大的篇幅介绍debug的方法技巧可直接学习用户手册。笔记一定要及时整理啊不然时间久了真的会忘记的………………笔记就简单整理到这里如有不妥之处欢迎大家批评指正
形式验证的目的是比较功能的一致性比对综合后的网表netlist和RTL设计的功能是否一致比对PR后的网表和综合后网表功能是否一致。两处比对一致则代表最终PR后的网表功能符合设计者意图。在所有的IC设计中想要最终成功的设计者都不会放弃做形式验证且至少需要两次形式验证第一次是RTL和综合后的网表的比对这次比对简记为前FM第二次是综合后的网表和PR后的网表的比对这次比对简记为后FM。1 FM的逻辑框架不论是前FM还是后FM做形式验证的思路是一样的需要的东西如下1 参考文件就是那个被定义为永远正确的文件这里用ref来表示这里的ref文件就是RTL设计文件原因RTL经过功能仿真验证被认为RTL是符合设计者意图的正确设计2 用于比较的文件这里用imp来表示这里imp文件就是综合后的网表文件原因在综合过程中综合软件会对设计进行优化有些地方的优化可能不符合设计者意图从而导致功能错误3 明白ref文件和imp文件的底层表达ref文件是RTL的代码文件而imp文件是用具体器件表示的网表因此两者之间需要读入具体的器件的db文件软件才能明白文件具体想表达的意思。与此同时在综合过程中进行了优化也需要把优化的记录文件.svf文件读入软件才能比对优化处的功能2 FM的简单实现下面给出一个简单的FM的脚本在进行复杂的芯片验证时可在此基础框架上增删修改。步骤1设置顶层文件名字这个可以给自己提示该脚本是用于那个项目/模块的set top_design_name top_design_name步骤2设计FM的约束条件最开始约束条件可以不用设置用默认设置debug的时候可以加上。约束条件还有很多或者多种用法可参见使用手册和使用man指令set verification_failing_point_limit 0set hdlin_warn_on_mismatch_message {FMR_ELAB-147 FMR_VLOG-091}set verification_clock_gate_hold_mode anyset hdlin_ignore_full_case falseset hdlin_ignore_parallel_case falseset hdlin_unresolved_modules black_box……步骤3读入相应的db文件read_db ../../xxx.db步骤4 读入综合后的优化文件#set_synopsys_setup trueset_svf ../../../../xxxx.svf步骤5读入RTL设计文件到-r container里read_verilog -container r -libname WORK {module_a.v module_b.v module_c.v}set_top r:/WORK/$design_top_nameset_refernce r:/WORK/$design_top_nameset hdlin_unresolved_modules black_box步骤6读入网表文件到-i container里read_verilog -i libname WORK -05 ../../xxxxx.vgset_top i:/WORK/$design_top_nameset_implementation i:/WORK/$design_top_name步骤7将i-container和r-container里的内容进行匹配比对matchreport_unmatched_pointsset_dont_verify {r:/work/xxx/xxx/xx/xxx/shift_x_reg70/\*dff.00.7\*}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注1查找使用的命令用man比如 man read_verilog就会出来具体命令的使用方法注2关于formality的使用手册可在eetop社区里找到如下链接简单的应用框架在第81页。Formality® User Guide 2022-03 - 后端资料区 - EETOP 创芯网论坛 (原名电子顶级开发网) -注3formality的用户手册里可以找到相应的脚本模板3 start_guidebug工具可以通过FM的gui界面进行debug这个界面上存在问题分析、可能原因定位、电路的比较图对于debug很友好。用户手册里也有很大的篇幅介绍debug的方法技巧可直接学习用户手册。笔记一定要及时整理啊不然时间久了真的会忘记的………………笔记就简单整理到这里如有不妥之处欢迎大家批评指正
