AI 中文总结
本文提出字级符号仿真框架Forbench，保留仿真语义并增强符号支持，提供易用Python接口，可系统探索RTL行为，实验显示其在不损失覆盖率的前提下比现有符号方法显著加速，旨在降低形式化验证应用门槛。
AI 中文摘要
仿真因部署便捷、工作流程直观，仍是硅前验证的主流方法。但仿真仅在可行时间预算内探索有限的执行轨迹子集，常无法覆盖罕见边界情况，导致潜在漏洞未被发现。相比之下，形式化验证能提供数学上严格的正确性保证，但其实际应用受限于大规模设计的可扩展性挑战，以及从激励驱动操作转向以序列为中心的设计行为公理视图的思维转变，这使得编写精确属性以捕捉确切验证意图的难度增加。本文旨在降低验证中形式化方法的应用门槛，让仿真“更具形式化”。它引入了Forbench，这是一种字级符号仿真框架，保留了仿真熟悉的执行语义，但通过求解器支持的符号信号和状态转换对其进行增强，支持在符号输入和条件下系统地探索RTL行为。它提供了类似现有基于仿真框架的Python接口，用于定义约束、协调符号协同仿真以及执行属性检查。除了这种更易用的接口外，实验还表明，Forbench在不损失覆盖率的情况下，比现有符号方法实现了显著的加速。
英文摘要
Simulation remains the dominant approach in pre-silicon verification due to its ease of deployment and intuitive workflow. However, as simulation only explores a limited subset of possible execution traces within feasible time budgets, it often fails to explore rare corner cases, leaving latent bugs undetected. In contrast, formal verification offers mathematically rigorous guarantees of correctness. However, its practical adoption is constrained, not only by the scalability challenges over large-scale designs, but also by the change of mindset from stimulus-driven operations to the sequence-centric axiomatic view of design behaviors, introducing extra difficulty of writing precise properties to capture the exact verification intent. This paper aims to lower the barrier of applying formal methods in verification, by making simulation "more formal." It introduces Forbench, a word-level symbolic simulation framework that retains the familiar execution semantics of simulation but augments it with solver-backed symbolic signals and state transitions, enabling systematic exploration of RTL behaviors under symbolic inputs and conditions. It offers a Python interface, similar to the existing simulation-based frameworks, for defining constraints, coordinating symbolic (co-)simulations, and performing property checks. In additional to this more accessible interface, experiments also show that Forbench achieves notably speed-up over prior symbolic methods without the loss of coverage.
