一句话：提出 SylQ-SV 专用 SystemVerilog 符号执行引擎，通过 SMT 查询缓存加速硬件验证。
硬件设计的符号执行能提供高覆盖率和安全验证结果，但长期受路径爆炸问题困扰，开销高昂。本文提出 SylQ-SV，一个面向 SystemVerilog 的专用符号执行引擎，通过 SMT 查询缓存缩短执行时间，并支持包括 SystemVerilog Assertions 在内的必要语言构造，以形成端到端验证流程。作者在 OR1200 CPU、含 Ibex 核的 OpenTitan SoC，以及 HACK@DAC 的两个 SoC（分别含 PULPissimo 和 CVA6 核）上评估，相比当前最优方法最多降低 17% 运行时间，并公开源码与实验数据。
Symbolic execution of hardware designs is a path-based analysis that can deliver high quality coverage and security verification results. Unfortunately, the technique has historically struggled with the path explosion problem and, despite recent advances, remains expensive. We present SylQ-SV, a dedicated SystemVerilog symbolic execution engine that uses SMT query caching to improve execution times, reducing run time by up to 17% over the state of the art. SylQ-SV provides language support for all necessary SystemVerilog constructs, including SystemVerilog Assertions, to provide end-to-end verification workflows of the open-source designs most commonly appearing in the literature. We evaluate SYLQ-SV on the OR1200 CPU, the OpenTitan SoC with Ibex core, and two SoC designs from the HACK@DAC competitions (with PULPissimo core and CVA6 core, respectively). We make the SylQ-SV source code and all data used in the evaluation publicly available.