Formality：工具生成的文件

相关阅读

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命令）后会自动删除。

        

日志文件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文件的内容，该子目录还包含验证时用到的子网表。如果当前工作目录下已经存在名为formality_svf的子目录，则名字会变为formality1_svf，以此类推。

自定义行为

        可以通过一些启动时的选项来改变默认行为，如下所示：

-name_suffix file_name_suffix选项

        该选项用于定义生成的子目录和文件的名字后缀，例如，-name_suffix tmp会导致生成名为FM_WORK_tmp的子目录。如果指定的子目录和文件已存在，则会报错。

-overwrite选项

        配合-name_suffix filename_suffix使用，如果指定的子目录和文件已存在，则会进行覆盖。

-work_path path_name选项

        指定上面谈到的六个子目录和文件的生成目录（默认为当前目录），注意该选项并不改变当前工作目录。如果指定的目录不存在，则会创建。

使用命令生成的文件

        使用write_container命令可以将容器的数据保存在.fsc后缀的文件中，之后的会话可以使用read_container命令读取保存的容器。

        使用save_session命令可以将整个会话保存在.fsc后缀的文件中，可以使用restore_session命令重新启动会话。