硬件在设计制造之前通常通过寄存器传输级（RTL）仿真进行验证。为了测试与安全相关的信息流属性（如机密性和完整性），可以在设计中自动添加污点逻辑来跟踪信息如何流动。然而，最先进的污点逻辑仪器（如CellIFT）使基于仿真的测试开销过高：在Mega-BOOM（13.6万个单元）上，它使仪器化设计达到原始单元数的5.81倍，并导致143.72倍的仿真速度下降。简化污点逻辑可提高仿真速度，但不可避免地会牺牲精度。这种轻量级、不精确的污点逻辑会引入误报，最终可能导致更高的开销来检查这些误报。本文探讨了“精度实际上在哪里是必要的”这一研究问题，以克服误报带来的开销。它提出了CEGAR-T框架，该框架自动合成污点逻辑，在保证无假阳性（相对于精确的CellIFT基线）的同时最小化污点逻辑仪器开销。作者实现了CEGAR-T，并在开源RISC-V核心的时序侧信道安全指令集问题上进行了评估。在所有评估的核心上，CEGAR-T将仪器开销和仿真开销分别从几何平均5.64倍降至1.42倍、从34.65倍降至1.79倍，同时不损失CellIFT基线的精度效益。这项研究为预硅硬件安全验证提供了高效的自动化方案，显著降低了使用精确信息流跟踪的门槛。