PaperlayerView exact revision on arXiv

Source-linked AI summary

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

Sharjeel Imtiaz, Uljana Reinsalu, Tara Ghasempouri

arXiv:2609.10057v1cs.CRcs.AR

TL;DR

Porting a manually authored security-assertion corpus to structurally different RISC-V targets requires hours of RTL analysis per assertion, while raw LLM translation can hallucinate signals and produce varying outputs. AutoTrans extracts target RTL signals to ground prompts, uses a fixed prompt template with pinned inference parameters, and applies compilation and JasperGold FPV checks to translated assertions. Across 68 NS31A groups across nine Ibex modules, AutoTrans achieved 78% Auto TAR (53/68 groups) with zero human intervention.

  • Problem

    Porting a manually authored security-assertion corpus to structurally different RISC-V targets requires hours of RTL analysis per assertion, while raw LLM translation can hallucinate signals and produce varying outputs.

    Source: §I · p. 2

  • Method

    AutoTrans extracts target RTL signals to ground prompts, uses a fixed prompt template with pinned inference parameters, and applies compilation and JasperGold FPV checks to translated assertions.

    Source: §I · pp. 2–3

  • Results

    Across 68 NS31A groups across nine Ibex modules, AutoTrans achieved 78% Auto TAR (53/68 groups) with zero human intervention.

    Source: C. Translation and FPV Results (Steps… · p. 6, §V · p. 7

  • Takeaways & Limitations

    AutoTrans provides automatically translated assertions accepted only when formally proven correct and non-vacuous on the target RTL.

    Source: §I · p. 3, §V · p. 7

Abstract

from arXiv · show

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.

I. INTRODUCTION

Porting verified security assertions across structurally different RISC-V processors is costly, while raw LLM translation can hallucinate target signals and vary as models change. AutoTrans combines signal grounding, reproducible prompting, and formal verification to automate translation and measure acceptance on the target.

I. INTRODUCTION

  • Porting the NS31A corpus to a structurally different target such as Ibex requires rematching signals, widths, addressing modes, and clocking conventions, taking hours per assertion.The corpus contains 1,146 property instances across 68 groups and nine categories, and a complete corpus can take weeks to rework.Source: §I · p. 2
  • Prior approaches address parts of assertion translation but do not bridge semantic gaps between heterogeneous designs while guaranteeing formal correctness.The paper positions AutoTrans as addressing this combination of needs.Source: §I · p. 2
  • AutoTrans translates formally verified assertions across structurally different RISC-V targets, requiring each assertion to pass QuestaSim compilation and JasperGold FPV.The pipeline aims to preserve security intent without manual re-authoring, GPU use, or fine-tuning.Source: §I · p. 2
  • A lightweight regex-based extractor grounds prompts in signals available in the target RTL, addressing signal hallucination without EDA infrastructure or licenses.Source: §I · p. 3
  • A fixed prompt template and pinned inference parameters enforce byte-identical prompt assembly on every run, supporting reproducible translation without GPU or fine-tuning.Source: §I · p. 3
  • 78% Auto TAR and 100% Final TAR were achieved across 68 security property groups and nine Ibex modules.TAR counts only assertions formally proven correct and non-vacuous on the target RTL.Source: §I · p. 3

II. RELATED WORK

Prior security verification work establishes the value of target-specific assertions, but existing translation and LLM-generation approaches leave gaps in handling heterogeneous designs and formally validating ported properties.

A. Assertion-Based Security Verification

  • Security properties for open-source RISC-V designs have been shown to detect hardware Trojans, privilege violations, and illegal memory accesses, but depend on correct target-specific assertions.The reference processor corpus contains 1,146 manually authored properties across nine categories and requires significant RTL expertise per assertion.Source: A. Assertion-Based Security Verification · p. 3

B. Non-LLM Assertion Translation

  • NLP templates work within a design family but do not scale to heterogeneous targets where signal semantics differ.Source: B. Non-LLM Assertion Translation · p. 3
  • Transys translates through dependence-graph matching and performs strongly on syntactically similar designs, but requires EDA tools and struggles when a security model lacks a target structural counterpart.AutoTrans instead uses LLM reasoning grounded in the target RTL interface to address this semantic-gap case.Source: B. Non-LLM Assertion Translation · p. 3

C. LLM-Based Assertion Generation

  • LLM-based generation creates assertions from RTL or natural language rather than porting an existing verified corpus, and some approaches require GPU clusters for training.Source: C. LLM-Based Assertion Generation · p. 3
  • Prior prompt-based approaches report accuracy without a formal verification gate, while BLEU and coverage do not establish formal correctness on target RTL.AutoTrans requires each accepted assertion to be formally proven and non-vacuous on clean RTL; model drift can trigger FPV failure and retry rather than admit a wrong assertion.Source: C. LLM-Based Assertion Generation · p. 3

III. AUTOTRANS FRAMEWORK

AutoTrans separates security assertion translation from validation: it uses target RTL and source-processor properties to create bind files, then formally validates them and reports TAR.

A. Overview

  • The two-stage framework takes target RISC-V RTL and source-processor security properties as inputs, producing translated bind files and then formally validated assertions with a TAR report.Source: A. Overview · p. 3

B. Stage 1: Security SVA Translation

  • Stage 1 extracts target RTL signals, assembles a prompt with source security properties, and calls DeepSeek V4-Flash to generate a bind file.The bind file is a separate SystemVerilog module attached to target RTL at elaboration without modifying it.Source: B. Stage 1: Security SVA Translation · p. 3
  • Fig. 2 depicts Stage 1 as signal extraction to JSON, grounded prompt assembly, and DeepSeek V4-Flash SVA translation.Source: Figure 2 · p. 3

1) Step 1A: RTL Signal Extraction:

Stage 1A parses target SystemVerilog into structured signal data, and Stage 1B combines that data with source assertions and templates in a reproducible prompt.

1) Step 1A: RTL Signal Extraction:

  • The custom Python regex parser extracts module type, parameters, ports, internal signals, and relevant package types into signals.json for downstream prompt assembly.It can merge declarations across files, resolve widths, and detect clock and reset by port-name convention for sequential modules.Source: 1) Step 1A: RTL Signal Extraction · p. 4

2) Step 1B: Prompt Assembly:

  • The prompt assembly loads signals.json and source assertion rows, selects a clocked or combinational SVA template by module type, then fills placeholders in one pass.Sequential templates mandate clocking and reset constructs, while the combinational template forbids clocking constructs; the filled prompt is saved for reproducibility auditing.Source: 2) Step 1B: Prompt Assembly · p. 4
  • For shared-RTL modules DO, ETI, CF, and MT, prompt assembly appends a logical suffix when deriving the assertion module name.Source: 2) Step 1B: Prompt Assembly · p. 4

3) Step 1C: DeepSeek Translation:

AutoTrans uses a two-tier DeepSeek V4 translation strategy with pinned inference settings, then parses responses into JSON logs and SVA bind files. Translation covers every assertion group, while acceptance is determined only after formal verification.

3) Step 1C: DeepSeek Translation:

  • V4-Flash performs initial translation at temperature=0.0 and seed=42, while V4-Pro is reserved for failure-triggered retries to concentrate higher-cost reasoning where needed.The workflow uses NVIDIA NIM and requires no GPU or fine-tuning.Source: 3) Step 1C: DeepSeek Translation · p. 4
  • The response is stripped of its <think> trace and parsed into a JSON mapping log and a complete SVA bind file, with shared Ibex controller targets rewritten to the correct module name.When a source signal has no direct target equivalent, the template directs the model to preserve security intent using the nearest available Ibex signals.Source: 3) Step 1C: DeepSeek Translation · p. 4
  • Translation coverage is 100% at Step 1C, but TAR is computed only after FPV acceptance at Step 2B.Source: 3) Step 1C: DeepSeek Translation · p. 5

C. Stage 2: Security SVA Validation

Stage 2 validates translated bind files through QuestaSim syntax compilation and JasperGold FPV, with distinct retry logic for syntax errors, logic failures, and vacuity. A module is locked after three failed retries.

C. Stage 2: Security SVA Validation

1) Step 2A: Syntax Validation:

  • On QuestaSim compilation failure, the retry prompt combines the original prompt, error log, and bind file, instructing V4-Pro to fix syntax while preserving assertion logic.After three failed retries, the module is locked for manual inspection.Source: 1) Step 2A: Syntax Validation · p. 5
  • JasperGold FPV parses proof and vacuity reports; counterexamples trigger logic rewriting, while vacuous results trigger antecedent rewriting.TAR is computed only after all assertions are proven and non-vacuous; three failed retries lock the module.Source: 2) Step 2B · p. 5

2) Step 2B:

TAR is a per-module acceptance metric computed after FPV, counting source assertion groups that are proven and non-vacuous on clean RTL. Auto TAR counts automated acceptances; Final TAR also includes targeted manual resolution of structural constraints with security intent unchanged.

2) Step 2B:

  • TAR counts source assertion groups proven and non-vacuous on clean RTL, and is computed per module at the end of Step 2B.Source: D. TAR Metric · p. 5
  • Auto TAR counts groups proven by the automated framework; Final TAR additionally counts groups proven after targeted manual resolution of JasperGold FPV structural constraints.The manual resolution preserves security intent unchanged.Source: D. TAR Metric · p. 5
  • TAR is deliberately conservative, accepting only assertions independently accepted by QuestaSim and JasperGold.Source: D. TAR Metric · p. 5

IV. EXPERIMENTS

Across nine Ibex modules, AutoTrans achieved 78% automated TAR and 100% Final TAR after targeted human resolution; the signal extractor parsed all nine modules without manual intervention.

A. Experimental Setup

  • Experiments translated 68 NS31A assertion groups across nine security categories to Ibex at commit bd25993, using QuestaSim compilation and JasperGold FPV.DeepSeek V4-Flash handled translation, with V4-Pro used for retries.Source: A. Experimental Setup · p. 5

B. Signal Extraction Results (Step 1A)

  • The extractor parsed all nine Ibex security modules without manual intervention, with CSR the most complex at 44 inputs, 27 outputs, 109 internals, and 9 package types.Empty git diff results/signals/ on every rerun confirmed reproducibility.Source: B. Signal Extraction Results (Step 1A) · p. 5

C. Translation and FPV Results (Steps 1C–2B)

  • 100% of the 68 NS31A entries produced at least one SVA property in the bind file.The 68 groups included source SVA examples and natural-language-only properties; the latter were translated into formal SVA without manual authoring before verification.Source: C. Translation and FPV Results (Steps… · pp. 5–6
  • 78% automated TAR (53/68 groups) was achieved using V4-Flash and V4-Pro retries without human intervention.PMP and CSR contributed 20 groups (29%) that passed directly from Flash output with zero retries or manual intervention.Source: C. Translation and FPV Results (Steps… · p. 6
  • 100% Final TAR (68/68 groups) was reached across all nine modules after targeted manual resolution of 16 groups across seven modules.JasperGold and QuestaSim errors identified structural root causes; fixes changed how properties were expressed, not the security properties they checked.Source: C. Translation and FPV Results (Steps… · p. 6

D. Reproducibility

AutoTrans makes signal extraction and prompt assembly deterministic, while pinned inference settings reduce sampling variance. JasperGold FPV gates outputs so model drift cannot add incorrect assertions to the result set.

  • Identical RTL and inputs produce byte-identical signals.json and prompts/final/ files, confirmed by empty git diffs on reruns.LLM output determinism is governed by temperature=0.0 and seed=42.Source: D. Reproducibility · p. 6
  • JasperGold FPV rejects output variations that affect correctness and triggers retries, so only formally proven, non-vacuous assertions enter the result set.The gate is designed to handle silent cloud-provider model-weight updates.Source: D. Reproducibility · p. 6

E. Signal Grounding Ablation

The signal-grounding ablation contrasts ungrounded and grounded translation; AutoTrans is also reported as the only compared approach combining parser grounding, reproducibility, no-GPU operation, and a hard FPV gate.

E. Signal Grounding Ablation

  • With signal grounding, all signals were valid, compilation passed, and TAR reached 100%; without it, 15 invalid names and Markdown fences blocked compilation.The ungrounded output produced three cascading QuestaSim errors, preventing JasperGold verification.Source: E. Signal Grounding Ablation · p. 6, Table IV · p. 6

F. Comparison with Related Approaches

  • AutoTrans is the only compared approach reported to combine no-GPU operation, parser-grounded prompts, pipeline-output reproducibility, and a hard FPV gate.The comparison distinguishes BLEU text similarity from formal correctness on target RTL.Source: F. Comparison with Related Approaches · p. 6, Table V · p. 6

G. Comparison with Prior Work

The comparison with prior work spans coverage, assertion count, automation, English-property handling, formal verification, and translation time. The conclusion reports AutoTrans results across 68 NS31A assertion groups in nine Ibex modules.

G. Comparison with Prior Work

V. CONCLUSION

  • In cross-architecture RISC-V security-assertion translation, AutoTrans achieved 78% Auto TAR with zero human intervention and 100% Final TAR overall across 68 NS31A groups in nine Ibex modules.Source: §V · p. 7
Loading 2609.10057v1…