comformal 形式验证中遇到的问题，菜鸟求助！

设计中调用了一个SRAM模块，同时也加上了： Add notranslate module *SRAM* -both

但是还是报错：
Error: top.v:216 Module 'SRAM' is referenced but not defined.

请问什么原因呢?

你的这个error是因为在读入设计的时候没有读入对应的memory的library。
Add notransltate module 只是让工具在读入library的时候只parse端口定义，而不去parse内部的function等描述而已，跟add black box有点类似。
在读入设计时还是需要读入对应的library model和design。
如果你那边没有对应的SRAM的library model(*.lib或*.v)的话，可以读入design，然后用write design的命令写一个只有端口定义的.v格式的模块出来。然后把写出来的这个blackbox重新读入就可以了。

BTW，对于写出来的.v模块，注意其data bus的升降序关系与设计调用中的一致性。