Hardware-firmware co-verification is critical to design trustworthy systems. While formal methods can provide verification guarantees, due to the complexity of firmware and hardware, it can lead to state space explosion. There are promising avenues to reduce the state space during firmware verification through manual abstraction of hardware or manual generation of hints. Manual development of abstraction or hints requires domain expertise and can be time-consuming and error-prone, leading to incorrect proofs or inaccurate results. In this paper, we effectively combine the scalability of simulation-based validation and the completeness of formal verification. Our proposed approach is applicable to actual firmware and hardware implementations without requiring any manual intervention during formal model generation or hint extraction. To reduce the state space complexity, we utilize both static module-level analysis and dynamic execution of verification scenarios to automatically generate system-level hints. These hints guide the underlying solver to perform scalable equivalence checking using proofs. The extracted hints are validated against the implementation before using them in the proofs. Experimental evaluation on RISC-V based systems demonstrates that our proposed framework is scalable due to scenario-based decomposition and automated hint extraction. Moreover, our fully automated framework can identify complex bugs in actual firmware-hardware implementations.

翻译：硬件-固件协同验证对于设计可信系统至关重要。尽管形式化方法能够提供验证保证，但由于固件与硬件的复杂性，可能导致状态空间爆炸。目前存在通过手动抽象硬件或手动生成提示来缩减固件验证状态空间的有效途径，但手动构建抽象或提示需要领域专业知识，且耗时易错，可能导致错误证明或不精确结果。本文有效结合了基于仿真的验证的可扩展性与形式化验证的完备性。所提出的方法适用于实际固件与硬件实现，在形式化模型生成或提示提取过程中无需任何人工干预。为降低状态空间复杂度，我们利用静态模块级分析与验证场景的动态执行，自动生成系统级提示。这些提示引导底层求解器通过证明实现可扩展的等价性检查。提取的提示在用于证明前需通过实现有效性验证。基于RISC-V系统的实验评估表明，得益于场景分解与自动提示提取，所提框架具备可扩展性。此外，我们的全自动框架能够识别实际固件-硬件实现中的复杂缺陷。