AI 中文总结
AutoTrans框架利用正则表达式信号提取、固定提示模板和形式化验证，自动翻译RISC-V安全断言，防止信号幻觉，实现78%自动接受率及100%最终接受率。
AI 中文摘要
在RISC-V处理器目标之间复用一组经过验证的安全断言仍然是硬件安全验证中最昂贵的瓶颈之一。手动翻译每个断言需要数小时。原始LLM翻译速度快但不可靠，会引入信号幻觉，即模型凭空捏造目标RTL中不存在的端口名称，并且产生的输出可能因模型更新甚至同一模型版本而异。本文提出了AutoTrans，一个解决上述缺点的自动化框架。首先，提出了一种新的基于正则表达式的轻量级System Verilog信号提取器，用于识别生成安全断言所需的信号。这一步对于防止信号幻觉是必要的。其次，引入了一个模板来创建提示和固定的推理参数，确保每次运行都生成字节完全相同的提示组装，使流水线输出对模型更新具有鲁棒性。此外，所引入的LLM提示模板能够仅从RISC-V处理器的英文安全描述中生成安全断言，无需手动编写。第三，集成了形式化验证流程（JasperGold FPV），该流程保证生成的安全断言能够验证RISC-V处理器的安全性，而不是静默地进入结果集。该工作流应用于Deepseek V4，将安全断言从一个RISC-V翻译到另一个（例如，从NS31A RISC-V到IBEX）。实验表明，AutoTrans在无需人工干预的情况下自动实现了78%的自动翻译接受率（TAR），在人工精炼后最终TAR达到100%。
英文摘要
Reusing a set of verified security assertions across RISC-V processor targets remains one of the most expensive bottlenecks in hardware security verification. Manual translation takes hours per assertion. Raw LLM translation is fast but unreliable, introducing signal hallucination, where the model invents port names absent from the target RTL and produces outputs that may vary across model updates or even within the same model version. This paper presents AutoTrans, an automated framework that addresses the above shortcomings. First, a new lightweight Regular Expression-based System Verilog signal extractor is proposed to identify the signals for generating security assertions. This step is necessary to prevent signal hallucination. Second, a template is introduced to create prompt and pinned inference parameters that guarantee a byte-identical prompt assembly on every run, making the pipeline output resilient to model updates. Moreover, the introduced template for LLM prompting is capable of generating security assertions from English-only security descriptions of RISC-V processors, with no manual authoring. Third, a formal verification process (JasperGold FPV) is integrated, which guarantees that the generated security assertions verify the security of the RISC-V processor rather than silently entering the result set. The workflow is applied on Deepseek V4 to translate security assertions from one RISC-V to another (e.g., for IBEX from NS31A RISC-V). The experiment shows that AutoTrans achieves 78\% Auto Translation Acceptance Rate (TAR) automatically and without human intervention and 100\% Final TAR after refinement by humans.
