企业官网建设流程全解析

相关阅读

Formalityhttps://blog.csdn.net/weixin_45791458/category_12841971.html?spm=1001.2014.3001.5482

Formality在启动和运行时会创建一些目录和文件，本文旨在对它们进行说明。

默认行为

在使用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.log，Formality会创建一个关联的锁文件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.log，Formality会创建一个关联的锁文件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命令重新启动会话。