为什么Encounter Conformal会在正式验证期间报告未定义的设计实体？

如果设计网表中的设计实体名称与形式验证库中的实体的情况不匹配，则Encounter Conformal形式验证工具可以报告此错误。

例如，包含以大写形式指定的LPM_MULT宏功能的设计会导致以下错误：
// Running Conformal on the <design_name> design gives the following errors.
// Error:<file_name>:<line #> Design unit 'LPM_MULT' is referenced but not defined

在此示例中，综合后设计网表包含大写的名称LPM_MULT 。由于所有Altera宏功能模块的形式验证库模型都是小写的，因此Encounter Conformal无法在库中找到大写的LPM_MULT模型。

要解决此问题，请将综合后设计网表中的名称从大写更改为小写（在此示例中，将名称更改为lpm_mult ）。

有关使用Conformal进行形式验证的更多信息，请参考Quartus II手册第3卷中的Cadence Incisive Conformal Equivalency Checker Support （PDF）章节。