AutoTrans: AI-Assisted Automatic Translation of Security Assertions for RISC-V Processors

A framework combining regex-based signal extraction, deterministic LLM prompting, and formal verification to automate cross-target security assertion translation

Sharjeel Imtiaz; Uljana Reinsalu; Tara Ghasempouri· 2026· DOI 10.48550/arXiv.2609.10057

The core problem

Reusing verified security assertions across different RISC-V processor targets is a major bottleneck in hardware security verification. Manual translation of assertions is time-consuming, often requiring hours per assertion. While large language models (LLMs) can accelerate this process, raw LLM translation suffers from signal hallucination—inventing port names not present in the target RTL—and produces outputs that vary across model updates or even within the same model version. This paper introduces AutoTrans, an automated framework designed to overcome these limitations. AutoTrans integrates three key components: a lightweight Regular Expression-based SystemVerilog signal extractor to prevent signal hallucination, a deterministic prompt template with pinned inference parameters to ensure byte-identical prompt assembly across runs, and a formal verification process using JasperGold FPV to guarantee that generated assertions actually verify the security of the RISC-V processor. The framework is evaluated on translating security assertions from the NS31A RISC-V to the IBEX RISC-V using Deepseek V4.

The experiment on translating security assertions from NS31A to IBEX using Deepseek V4 shows that AutoTrans achieves a 78% Auto Translation Acceptance Rate (TAR) automatically, without any human intervention. After refinement by humans, the Final TAR reaches 100%. This indicates that the framework significantly reduces manual effort while ensuring correctness. The deterministic prompting and signal extraction effectively mitigate signal hallucination and model variability, as evidenced by the high automatic acceptance rate. The formal verification step ensures that all accepted assertions are valid for the target processor.

Reusing verified security assertions across different RISC-V processor targets is a major bottleneck in hardware security verification. Manual translation of assertions is time-consuming, often requiring hours per assertion. While large language models (LLMs) can accelerate this process, raw LLM translation suffers from signal hallucination—inventing port names not present in the target RTL—and produces outputs that vary across model updates or even within the same model version. This paper introduces AutoTrans, an automated framework designed to overcome these limitations. AutoTrans integrates three key components: a lightweight Regular Expression-based SystemVerilog signal extractor to prevent signal hallucination, a deterministic prompt template with pinned inference parameters to ensure byte-identical prompt assembly across runs, and a formal verification process using JasperGold FPV to guarantee that generated assertions actually verify the security of the RISC-V processor. The framework is evaluated on translating security assertions from the NS31A RISC-V to the IBEX RISC-V using Deepseek V4.

AutoTrans comprises three main stages:

AutoTrans addresses two critical challenges in LLM-based assertion translation: signal hallucination and output variability. The regex-based signal extractor provides a ground truth for signal names, preventing the LLM from inventing ports. The deterministic prompt template and pinned inference parameters ensure reproducibility, making the pipeline robust to model updates. The integration of formal verification acts as a correctness filter, ensuring that only assertions that pass formal checks are accepted. The 78% automatic TAR demonstrates the effectiveness of these measures, while the 100% final TAR after human refinement highlights the potential for further automation. The framework is generalizable to other RISC-V targets and security descriptions, though its performance may depend on the quality of the English descriptions and the LLM's capabilities. Future work could explore extending AutoTrans to other hardware description languages and verification tools.

CS practitioners and researchers

Opening member content…