Formality读入implement ddc时指定top问题

JekinBrown

小弟在用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。想知道有没有更好的设置方法。