首先FileList是什么一、字面含义filelist file文件 list列表直译文件列表是通用命名不是单一固定工具不同场景含义不一样。在形式验证Formal Verification 场景中filelist 是一个文本格式的文件清单用于向形式验证工具如 Synopsys Formality、Cadence Conformal、OneSpin 等一次性声明所有需要加载的设计文件、库文件、约束与辅助文件是大型芯片项目中管理验证输入、保证一致性、避免漏文件的核心配置文件。通俗来说FileList是在做形式化验证的时候可以把一个案例所有的RLT源文件一次性发送验证二、典型格式与内容.f/.list1.形式验证的 filelist 通常以 .f 或 .list 为后缀每行一条指令支持文件路径Verilog/SystemVerilog/ 网表 .v/.sv/.vgC 类比gmain.cpp uart.cppmain.cpp、uart.cpp 就是待编译源码和这里的 .sv/.v 完全对应。作用按依赖顺序加载设计代码底层模块先写上层顶层后写避免 “未定义模块” 报错。2.包含目录incdir告诉工具遇到“includexxx.svh去哪里找 类比g-I./include-I./ip/def main.cpp-I 头文件搜索路径和 incdir 功能一模一样。作用代码里写 include “param.vh” 时工具自动去 incdir 目录查找头文件否则报头文件找不到。3.宏定义define给RLT代码开关或设常量类似于C语言#define4.嵌套 filelist-f / -F5.库路径-y / libext三、在主流形式验证工具中的用法Synopsys Formality等价性检查最常用#1.包含目录头文件路径incdir./rtl/includeincdir./ip/amba/include #2.宏定义defineFORMALdefineNO_SIM #3.RTL 设计文件按依赖顺序底层先./rtl/top.sv./rtl/core/core.v./rtl/periph/uart.v./rtl/periph/spi.v #4.网表文件等价性检查Golden vs Revised./netlist/top_gate.v #5.标准单元库/IP./lib/tsmc180/stdcells.v./ip/ddr/ddr_wrapper.v #6.黑盒 stub形式验证常用./stub/ddr_phy_stub.v #7.嵌套子 filelist-f./ip/axi/axi_filelist.f关键语法说明incdir路径指定 include 搜索路径。define宏编译时宏开关如 FORMAL 关闭仿真逻辑。-f 子filelist相对 Makefile / 脚本路径-F相对 filelist 自身路径推荐。-y 库目录 libext.v.sv自动搜索库文件无需关心编译顺序module 名 文件名。顺序敏感被依赖模块必须先出现否则工具报 “未定义模块”。我的安装包怎么能支持FileList主要是分四层1.第一层provekit CLI是用户入口接受-f filelist.f,用python解析并校验filelist校验源文件、filelist存不存在、语法是否合规,把top模块、验证模式等信息传给任务生成和底层引擎2.第二层其实就是生成sby验证任务把用户的模式、top模块、filelist路径在[script]里写入read_verilog_file_list -f filelist.f然后交给pk-verify执行read_verilog_file_list -f filelist.f 是 pk-compile 里新增的命令用来解析 VCS 风格 filelist自动处理宏、include 和源文件列表ProveKit 在生成验证任务时会把用户的 -f filelist.f 转成这条底层命令。pk-verify 是 ProveKit 的验证调度引擎由原 SymbiYosys 改名而来。它读取 .pkjob 任务文件调用 pk-compile 完成设计读入和形式化预处理再驱动 Z3 等求解器执行 BMC/prove最后返回 PASS 或 FAIL。3.第三层pk-compile执行read_verilog_file_list命令用新写的filelist.cc解析VCS风格filelist设置宏和include路径再逐个读Verilog源文件最后执行prep做形式化预处理为后续验证生成模型。4.第四层z3跑模型