本文是一篇关于硬件模糊测试（Hardware Fuzzing）的系统性综述（SoK），旨在系统化梳理当前硬件模糊测试技术在三个主要抽象层次上的研究现状与挑战，这三个层次分别是指令集架构（ISA）、微架构（Microarchitecture）以及寄存器传输级（RTL）。研究从输入刺激质量、变异策略、反馈机制、目标平台、参考模型以及覆盖率等多个关键维度，对现有硬件模糊测试方法进行了全面分析和横向比较。作者发现，不同抽象层次在挑战、目标和设计权衡上存在显著差异：ISA 层更关注指令序列的合法性与语义覆盖；微架构层侧重于触发深层流水线竞争或缓存行为；而 RTL 层则需要在门级或寄存器传输级上快速生成能触发设计缺陷的激励。文中进一步指出现有硬件模糊测试实践中存在的若干尚未满足的需求，包括智能输入生成、可靠且可扩展的黄金参考模型、表达力更强的反馈通道，以及跨层集成能力。基于这些洞察，作者提出了未来研究方向，涵盖混合模糊测试框架、AI 辅助测试生成、可扩展参考模型、标准化评估指标与基准测试，以及将人工引入循环的自动化引导探索与分析。整体目标是为了实现高效、可靠且全面的硬件验证解决方案。本文适合硬件安全研究人员、EDA 工具开发者、芯片验证工程师以及关注硬件供应链安全的蓝队成员阅读，有助于理解硬件模糊测试的技术边界和演进方向。

本文提出 Granite，一种用于对 RTL 级处理器设计进行模块化形式验证的方法论，旨在同时验证功能正确性和非泄漏性（nonleakage）。基于 ISA 泄漏契约，Granite 证明了带有推测执行、精确中断和 I/O 的流水线 RISC 设计的逐周期时序行为完全由契约中可观测的接口决定。对于遵循密码学常数时间纪律的程序（即不将秘密值影响任何可观测量的程序），该结果能够排除经已知或未知时序侧信道的信息泄漏。Granite 的规格仅约束功能正确性和信息流依赖，不规定指令的周期数、中断处理位置或子模块（如乘法器、内存）的具体延迟。其核心技术是'基于确定性的泄漏感知精化'，将正确性和机密性统一表示为与一族周期级确定性规格机器的轨迹等价。对于与秘密无关的非确定性，Granite 通过存在性参数化规格，使用仅作用于公开数据的不可信确定性函数来处理。子模块分别被证明满足其自身的泄漏感知规格，而这些证明组合成整体设计保证，因此适用于广泛的实现空间。作者声称这是首项在指令集级泄漏契约与微架构级逐周期执行（带线级观测）之间建立模块化和基础连接的工作。此外，该证明与一个认证静态分析相结合，可识别密码学常数时间代码，进而推导出关于硬件-软件密码实现的逐周期机密性的单一 Rocq 定理，从而从可信计算基（TCB）中消除了包括 ISA 契约在内的所有中间规格。