相关阅读Formalityhttps://blog.csdn.net/weixin_45791458/category_12841971.html?spm1001.2014.3001.5482Formality在启动和运行时会创建一些目录和文件本文旨在对它们进行说明。默认行为在使用fm_shell命令或formality命令打开Formality后首先会在当前工作目录生成以下这些子目录和文件子目录FM_WORK该子目录包含了容器和共享工艺库相关信息。如果当前工作目录下已经存在名为FM_WORK的子目录则名字会变为FM_WORK1以此类推。在正常退出Formality使用exit命令或quit命令后会自动删除。子目录FM_INFO默认情况下Formality会创建FM_INFO信息目录用于记录当前Formality运行环境、系统资源、工具配置和执行状态等辅助信息。该目录主要用于问题排查、运行状态分析以及向Synopsys技术支持提供诊断信息。FM_INFO目录中可能包含以下文件cmd记录启动Formality时使用的命令行。cpuinfo保存Linux系统中/proc/cpuinfo文件的副本即处理器相关信息。disk记录Formality启动时系统可用的磁盘空间。env记录启动Formality时的全部环境变量。guidance.perf记录SVF指导信息的性能摘要该文件经过加密。guidance.summary记录SVF指导信息被接受或拒绝的汇总结果。host记录运行Formality的主机信息。limits记录操作系统对Formality进程施加的资源限制。meminfo保存Linux系统中/proc/meminfo文件的副本即系统内存相关信息。milestones记录Formality运行过程中的里程碑信息该文件经过加密。monitor周期性记录主机负载和可用磁盘空间采样间隔通常约为10分钟。vars.tcl记录当前会话中取值不同于默认值的Tcl变量。需要注意的是FM_INFO目录是在Formality的Tcl解释器启动之前创建的。因此是否生成该目录不能通过普通的Formality Tcl变量进行控制而需要通过环境变量进行设置。如果不希望Formality生成FM_INFO目录可以在启动Formality前设置FORMALITY_DISABLE_INFO_DIRECTORY环境变量。日志文件formality.log该文件记录了未打印到屏幕上的信息。例如在验证过程中屏幕可能显示一条信息提示参考设计中的常量被传播并引导查看formality.log文件以获取更多信息。如果当前工作目录下已经存在名为formality.log的文件则名字会变为formality1.log以此类推。锁文件formality.lck对于日志文件formality.logFormality会创建一个关联的锁文件formality.lck用于指示该日志文件正被一个活跃的Formality会话使用。如果此时其他Formality会话尝试写入日志则会出现FM-413错误。在正常退出Formality使用exit命令或quit命令后会自动删除。日志文件fm_shell_command.log该文件记录了所有Formality执行过的命令。如果当前工作目录下已经存在名为fm_shell_command.log的文件则名字会变为fm_shell_command1.log以此类推。锁文件fm_shell_command.lck对于日志文件fm_shell_command.logFormality会创建一个关联的锁文件fm_shell_command.lck用于指示该日志文件正被一个活跃的Formality会话使用。如果此时其他Formality会话尝试写入日志则会出现FM-413错误。在正常退出Formality使用exit命令或quit命令后会自动删除。除了以上五个子目录和文件当使用set_svf命令加载SVF文件时会创建formality_svf子目录SVF子目录formality_svf该目录包含了一个文件svf.txt记录了使用set_svf命令加载的所有SVF文件的内容包括手动执行的guide类命令该子目录还包含验证时用到的子网表这个需要在另一篇文章说明。如果当前工作目录下已经存在名为formality_svf的子目录则名字会变为formality1_svf以此类推。自定义行为可以通过一些启动时的选项来改变默认行为如下所示-name_suffix file_name_suffix选项该选项用于定义生成的子目录和文件的名字后缀例如-name_suffix tmp会导致生成名为FM_WORK_tmp的子目录。如果指定的子目录和文件已存在则会报错。-overwrite选项配合-name_suffix filename_suffix使用如果指定的子目录和文件已存在则会进行覆盖。-work_path path_name选项指定上面谈到的六个子目录和文件的生成目录默认为当前工作目录注意该选项并不改变当前工作目录。如果指定的目录不存在则会创建。-create_unique_work_directory选项该选项用于创建一个独立的FM_RUN工作目录并将Formality运行过程中生成的临时文件和子目录统一保存在该目录下例如FM_WORK、FM_INFO等。默认情况下FM_RUN目录创建在当前工作目录中如果同时使用-work_path path_name选项则FM_RUN目录创建在path_name指定的路径下。使用命令生成的文件使用write_container命令可以将容器的数据不包括用户设置比如set_constant命令保存在.fsc后缀的文件中建议在进入Preverify模式前保存容器因为设计可能因为svf或upf被转换之后的会话可以使用read_container命令读取保存的容器。使用save_session命令可以将整个会话包括用户设置保存在.fss后缀的文件中可以使用restore_session命令重新启动会话。