形式验证问题请教

clovis

做形式验证的时候遇到一个情况：
某个寄存器R_0，在DC报告中显示由于其为常数，被移除；但是在形式验证中将该寄存器映射成一个LAT1，且该寄存器通过验证，这个属于正常情况吗？我查阅了formality.log文件，显示R_0 在SVF文件读进来时被rejected了，不知道跟这个是否有关系？
另本次形式验证有几个failing points ，出错的DFF在网表中是找不到的，看了下是由于R_0_C是x引起的，这个情况也很奇怪，请高手帮我分析下，谢谢！