来自微信公众号 “数字芯片实验室”
本实验将通过Formality GUI的方式展示形式验证基本流程，然后创建相应的Tcl脚本执行相同的形式验证流程。
该Lab所需的所有reference、implemention和libraries文件包含在下面的目录底下
本文使用Formality GUI对Verilog RTL和DC生成的Verilog netlist进行形式验证。然后，根据Formality生成的“ fm\_shell\_command.log”文件，书写TCL脚本。
a.) 使用“fm\_shell –gui”启动Formality软件的GUI界面。
b.) 读入SVF文件"default.svf"
c.) 读入Verilog RTL文件“alu.v、cntrl.v、r4000.v、register.v”，顶层名设置为"mR4000"
d.) 读入Verilog netlist文件"mR4000.gates.v"，顶层名设置为"mR4000"
e.) 读入libraries文件"tc6a\_cbacore.db"
f.) Match、Verify
g.) 根据"fm\_shell\_command.log"文件书写相应的Tcl脚本文件"runme.fms"
set search_path ". ./rtl ./lib ./netlist_w_svf"
set_svf default.svf
read_verilog -r "alu.v cntrl.v r4000.v register.v"
set_top mR4000
read_db -i tc6a_cbacore.db
read_verilog -i mR4000.gates.v
set_top mR4000
match
verifyh.) 使用书写的脚本直接执行
"fm_shell -frunme.fms |tee runme.log"完成形式验证。
本文转载自公众号：芯片数字实验室
原文链接：https://zhuanlan.zhihu.com/p/128036886
未经作者同意，请勿转载！
推荐阅读
想了解更多内容，欢迎关注芯片数字实验室专栏
