本文针对硬件信息流（information-flow）的形式化验证中可扩展性不足的问题，提出了一种名为“受保护等价谓词”（Guarded Equivalence Predicates）的方法。在硬件安全验证中，自组合（self-composition）技术将信息流验证转化为两个电路副本之间的安全性质检查，产生的关系性证明义务对通用的属性推演引擎（PDR）而言难以仅从位级逻辑中发现。最近基于PDR的技术利用副本对称性和全局跨副本等价谓词来利用这种重复结构，但当对应内部信号在整个可达状态空间中都不一致时，这些谓词效果有限，且无法捕获仅在特定控制上下文中相关的等式。作者观察到，在硬件信息流验证中，上下文相关关系自然存在：内部信号对可能只需在某个控制阶段、事务窗口、循环状态或协议区域内保持一致。为此，本文引入了受保护等价谓词，将该类关系暴露给PDR。与将提议的上下文等式作为假设不同，验证器将相应的失配条件作为辅助阻塞义务提交。保护条件是从关系性反例归纳（CTI）中通过CTI局部提取和状态分裂搜索提取的；只有后端证明不可达的候选者才会影响证明过程。在12个信息流验证基准测试和两个PDR后端的实验中，受保护谓词将两个上下文相关的基准超时转化为在1800秒时限内34.2-89.5秒内完成的证明，并在其他基准上将证明时间最多减少10.8倍。该方法为硬件安全验证提供了一种系统性的可扩展策略，尤其适用于需要检查不同运行轨迹下数据流一致性的复杂控制逻辑。