首先FileList是什么

一、字面含义
filelist = file（文件）+ list（列表），直译：文件列表，是通用命名，不是单一固定工具，不同场景含义不一样。

在形式验证（Formal Verification） 场景中，filelist 是一个文本格式的文件清单，用于向形式验证工具（如 Synopsys Formality、Cadence Conformal、OneSpin 等）一次性声明所有需要加载的设计文件、库文件、约束与辅助文件，是大型芯片项目中管理验证输入、保证一致性、避免漏文件的核心配置文件。
通俗来说FileList是在做形式化验证的时候可以把一个案例所有的RLT源文件一次性发送验证

二、典型格式与内容（.f/.list）

1.形式验证的 filelist 通常以 .f 或 .list 为后缀，每行一条指令，支持：

文件路径（Verilog/SystemVerilog/ 网表 .v/.sv/.vg）
C++ 类比

g++main.cpp uart.cpp

main.cpp、uart.cpp 就是待编译源码，和这里的 .sv/.v 完全对应。
作用
按依赖顺序加载设计代码；底层模块先写，上层顶层后写，避免 “未定义模块” 报错。

2.包含目录（+incdir+）：告诉工具遇到“include"xxx.svh"去哪里找
++ 类比

g++-I./include-I./ip/def main.cpp

-I 头文件搜索路径，和 +incdir+ 功能一模一样。
作用
代码里写 `include “param.vh” 时，工具自动去 incdir 目录查找头文件，否则报头文件找不到。

3.宏定义（+define+）：给RLT代码开关或设常量，类似于C语言#define

4.嵌套 filelist（-f / -F）
5.库路径（-y / +libext+）

三、在主流形式验证工具中的用法

1. Synopsys Formality（等价性检查最常用）

#1.包含目录（头文件路径）+incdir+./rtl/include+incdir+./ip/amba/include #2.宏定义+define+FORMAL+define+NO_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跑模型