实际测试过Synopsys VC Formal 2024.09 – SP1，经历过在浮点数比较模块的Formality验证一致性方面遇到难以处理的情况。
第一步 设置工艺库与link库路径
开启DC shell，在启动目录里创建.synopsys_dc.setup文件，写入set_app_var target_library slow_vdd1v0_typical.db，再写入set_app_var link_library { $target_library}，随后运用set_app_var search_path [list “/opt/PDK/2024/libs” “./rtl”]。
【新手避坑】
报错“Error: Cannot find design unit (LINK-1)”，通常是因为link_library忘记加星号“”，进而导致DC无法识别已编译模块。要马上检查.synopsys_dc.setup里星号是不是处在大括号第一位，并且确认search_path绝对路径不含有中文。
第二步 时钟约束的uncertainty最优值
实行create_clock -period 10 [get_ports CLK] -name sys_clk，接着击打set_clock_uncertainty -setup 0.3 [get_clocks sys_clk]。对于uncertainty，建议将其设定为0.3ns，此周期为10ns，原因在于，要留出20%的余量，以此来抵消PLL抖动，而且还要抵消布线延迟偏差，进而避免在流片之后出现setup违例。
【新手避坑】
“Warning: Can’t find clock ‘CLK’”这样报错呢，一般情况下是由于端口名的大小写出现了错误，或者是时钟没有连接到顶层的缘故。可以使用get_ports CLK去进行模糊匹配尝试找到真实名称，之后通过create_clock重新进行指定。要是uncertainty特别大从而让时序过度约束了，建议改用0.2ns。
第三步 两种综合方案对比与完整报错解决
针对方案A（保守功耗型）而言，其做法是将set_max_area设定为0，同时配合把set_max_dynamic_power也设定为0，且此做法仅仅是关闭功耗而不会对面积进行压制，它可以应用于那些依靠电池供电的低频芯片。具有性能优先特性的方案B：将set_max_delay设置为5，其范围是从所有输入端口，到所有输出端口，在此情况下能够插入额外的缓冲器，适用于CPU核的应用场景。
针对于高频出现的报错“Error: Design rule constraints violated (DRC) max_capacitance”的完整解决办法是这样的，先要使用report_constraint -all_violators > viol.rpt来查找出现违例的线网，接着运行insert_buffer -name buf_fix [get_nets clk_net] CLKBUF_X4M -new_cell_name buf1，最后通过compile_ultra -incremental来重新修正时序。
关于全定制模拟版图，或者开源Yosys+Coriolis流程，本方法是不适用的，因为在这些环境当中，缺少标准金属层电容模型。替代的方案是什么呢？是转用OpenLANE的自动脚本配置config.tcl里的那个SYNTH_MAX_FANOUT参数。另外，你在实测的时候，还遇到过哪种EDA工具链的奇怪报错呢？欢迎在评论区把它贴出来，咱们好一起排查。
