在线咨询
eetop公众号 创芯大讲堂 创芯人才网
切换到宽版

EETOP 创芯网论坛 (原名:电子顶级开发网)

手机号码,快捷登录

手机号码,快捷登录

找回密码

  登录   注册  

快捷导航
搜帖子
查看: 179|回复: 0

[求助] Formality读入implement ddc时指定top问题

[复制链接]
发表于 2024-12-6 23:06:42 | 显示全部楼层 |阅读模式

马上注册,结交更多好友,享用更多功能,让你轻松玩转社区。

您需要 登录 才可以下载或查看,没有账号?注册

x
小弟在用formality做形式验证,我的流程是:

1. DC综合时产生svf
2. 直接根据svf使用fm_mk_script -output fm.tcl *.svf 产生fm.tcl脚本
3. fm_shell -f fm.tcl
但是步骤2时,遇到两个问题,一大一小:
大问题:
先说一下DC有一个步骤前提:
我自定义了DC读入rtl代码、进行vhdl分析的design lib名称:

define_design_lib "RTL_DESIGN_LIB" -path ./LIBs/RTL_DESIGN_LIB

其余过程并无特殊。
综合后,fm_mk_script根据svf文件,会将define_design_lib的库作为reference design,将write_file -ddc/-verilog等命令输出的文件,作为implement design。
所以产生:

define_design_lib -r  -path ./LIBs/RTL_DESIGN_LIB RTL_DESIGN_LIB

set_top -vhdl_arch verilog r:/RTL_DESIGN_LIB/top
...<略>

read_ddc -i .....xxx.ddc
set_top -vhdl_arch verilog i:/RTL_DESIGN_LIB/top


好了,出现问题的地方已经被我标红在代码中。首先所有的路径都是正确的,但唯独对于implement design的顶层处理是错误的。fm_mk_script将我DC读入rtl代码、进行vhdl分析的design lib名称作为了implement design的lib名称,导致识别不了;我将RTL_DESIGN_LIB改成WORK就能正确识别;或者使用set_top -auto也可以(不过set_top -auto实际在terminal报出的信息就是i:/WORK/top
想请教各位有无解决方法,非常感谢!


另一个小问题并不重要,所以我摆到后面写:
其实从上文内容已经看到,fm_mk_script根据svf文件,会将write_file -ddc/-verilog等命令输出的文件,作为implement design。但是显然,我们在DC步骤进行write_file时,通常会把各式文件都写出,如果这些步骤统统记录到了svf文件中,fm_mk_script并不能知道你到底使用哪一个作为implement design,所以会多出一段类似”User interrupt “的注释行,将所有的write_file过程相关的信息都提供给用户选择;而我想默认使用ddc,所以笨方法是,在dc用set_svf -off和set_svf -append只记录ddc的write。想知道有没有更好的设置方法。
您需要登录后才可以回帖 登录 | 注册

本版积分规则

关闭

站长推荐 上一条 /2 下一条


小黑屋| 手机版| 关于我们| 联系我们| 隐私声明| EETOP 创芯网
( 京ICP备:10050787号 京公网安备:11010502037710 )

GMT+8, 2024-12-25 16:01 , Processed in 0.013486 second(s), 8 queries , Gzip On, Redis On.

eetop公众号 创芯大讲堂 创芯人才网
快速回复 返回顶部 返回列表