形式化验证问题请教

zhang9yeah · 发表于 2022-1-9 21:55:38

马上注册，结交更多好友，享用更多功能，让你轻松玩转社区。

您需要登录才可以下载或查看，没有账号？注册

x

   最近在做formality比对时，遇到两个问题，请大神帮忙解答一下，谢谢！问题描述如下：
      1、带上拉电阻的PAD在比对时报多驱动，应如何设置？
      2、代码中例化的PLL在比对时报AVDD和AVSS管脚比对失败，应如何设置？
   背景信息如下：
      1、做rtl VS pre netlist的形式化验证，在RTL中UART_RX管脚用了带上拉电阻的IO PAD类型
      2、RTL中例化PLL时注释掉了AVDD和AVSS的电源地管脚，且DC综合时PLL设置了don't touch属性
      3、formality验证时读取的是rtl和综合生成的ddc文件
      4、从比对结果的逻辑锥结构上看，UART_RX管脚的输入电平不一致，RTL输入低电平，netlist输入高电平
      5、PLL的AVDD和AVSS管脚看不出明显差别

夏尔 · 发表于 2022-2-9 18:52:55

关注一波

dqwuf2008 · 发表于 2022-2-10 08:31:03

关注

杰克淡定 · 发表于 2022-2-10 14:00:18

IO PAD和PLL在DC和formality流程中，都是以db形式存在。formality比不过的原因在于它们的lib与你RTL调用时的端口不一致，特别是电源地端口，如果RTL中注释掉了，那对应的lib也要注释掉

zhang9yeah · 发表于 2022-3-16 22:50:24

杰克淡定发表于 2022-2-10 14:00
IO PAD和PLL在DC和formality流程中，都是以db形式存在。formality比不过的原因在于它们的lib与你RTL调用时 ...

您说得对，RTL中例化PLL时未包含AVDD和AVSS管脚，所以比对报错，后面通过在fm中设置set_dont_verify，将AVDD和AVSS设置成不比对点就好了，另外，UART_RX管脚在PADC中增加了一个buffer，若是手动在vg网表中注释掉buffer，比对就可通过，由此看来，有没有可能是padc中的buffer的驱动能力比上拉电阻类型PAD的驱动能力强导致无法上拉到高电平，进而比对失败？

zyffpga · 发表于 2022-3-17 15:58:18

关注一下

[求助] 形式化验证问题请教

马上注册，结交更多好友，享用更多功能，让你轻松玩转社区。

站长推荐 /2