Sharjeelimtiaz27/ai-autotrans-rv

# ai-autotrans-rv **AI-AutoTrans：面向 RISC-V 处理器的 AI 辅助安全断言自动翻译** [](LICENSE) [](https://www.python.org/downloads/) ## 概述 本仓库实现了 RISC-V 处理器更大规模的形式化安全验证流程中的**阶段 1（断言翻译阶段）**。 该流水线接收来自 MEMOCODE 2023（Chuah 等人）的 NS31A 安全断言，并使用基于 **RV-SigEx** 的固定模板方法，通过 NVIDIA NIM API 调用 DeepSeek V4-Flash/Pro，将它们自动翻译为 Ibex RTL SVA，最后由 QuestaSim 编译和 JasperGold FPV 进行端到端验证。 ## 流水线 — 工作原理 ``` INPUTS ══════════════════════════════════════════════════════════════════ rtl/ibex/original/*.sv assertion_dataset/ns31a_.csv (Ibex RTL — never modify) (NS31A source assertions — 9 modules) │ │ │ │ ▼ │ ┌───────────────────────┐ │ │ STEP 1A │ │ │ parse_rtl.py │ │ │ RV-SigEx parser │ │ │ (regex-based SV) │ │ └──────────┬────────────┘ │ │ │ ▼ │ results/signals/ │ _signals.json prompts/sequential_prompt.txt (ports, internals, prompts/combinational_prompt.txt pkg_types, connectivity) (fixed templates — never modify) │ │ └─────────────────┬───────────────────┘ │ ▼ ┌───────────────────────┐ │ STEP 1B │ │ translate.py │ │ │ │ DeepSeek V4-Flash │ │ NVIDIA NIM API │ │ temperature = 0.0 │ │ seed = 42 │ │ │ │ Translate security │ │ INTENT — every │ │ assertion group │ │ must translate │ └──────────┬────────────┘ │ ▼ assertions/translated/_bind.sv results/logs/_tar_log.json prompts/final/_final_prompt.txt │ ▼ ┌───────────────────────┐ ┌──────────────────────────┐ │ STEP 1C │ FAIL │ Retry (max 3) │ │ validate_compile.py ├───────►│ DeepSeek V4-Pro │ │ QuestaSim │ │ prompt + error log │ │ SVA syntax check │ │ fix syntax only │ └──────────┬────────────┘ └──────────────────────────┘ │ PASS ▼ ┌───────────────────────┐ ┌──────────────────────────┐ │ STEP 1D │ FAIL │ Retry (max 3) │ │ validate_fpv.py ├───────►│ DeepSeek V4-Pro │ │ JasperGold FPV │ │ prompt + error + stage │ │ Proven + │ │ fix assertion logic │ │ non-vacuous │ └──────────────────────────┘ └──────────┬────────────┘ │ PROVEN + NON-VACUOUS ▼ results/step1/_fpv_baseline.txt results/step1/_vacuity.txt results/step1/_cov.txt │ ▼ ╔══════════════════════════════╗ ║ TAR (Translation ║ ║ Acceptance Rate) ║ ║ ║ ║ proven_assertions ║ ║ ──────────────── × 100 ║ ║ total_ns31a_groups ║ ║ ║ ║ Computed per module by ║ ║ validate_fpv.py ║ ╚══════════════════════════════╝ NOTES ══════════════════════════════════════════════════════════════════ Steps 1A + 1B run on any laptop (no EDA tools needed). Steps 1C + 1D require QuestaSim + JasperGold licences (EDA server). LLM tier strategy: Flash → initial translation only (cheap first attempt) Pro → ALL retries: QuestaSim compile failures + JasperGold FPV failures (QuestaSim errors involve enum scope, struct fields, port widths — they need deep RTL reasoning, not just syntax pattern matching) After 3 failed retries at either step: assertion is DROPPED, error logged to errors/archive/ (never delete — paper evidence). ``` ## 三大贡献 1. **RV-SigEx — 基于 regex 的 SystemVerilog 信号提取器，用于 LLM prompt 接地。** RV-SigEx 从真实的 SV 中提取端口、内部信号、包类型（typedef enums，structs）和参数化位宽，将其转换为结构化的 JSON 并注入到每个 prompt 中。与构建完整解析树且难以处理高级 Ibex 结构（如位于单独文件中的包作用域枚举、结构体类型的端口、参数化数组）的 PyVerilog 不同，RV-SigEx 使用针对真实 RISC-V SV 风格调优的目标 regex 模式。LLM 只能看到 RTL 中实际存在的信号——它无法凭空捏造不存在的信号名称。 2. **无幻觉、可复现的 SVA 翻译，采用两层 LLM 成本策略。** RV-SigEx 接地 + 固定模板 + `temperature=0.0` + `seed=42` 共同消除了原始 LLM 翻译的两种失败模式：幻觉信号和不可复现的输出。两层模型策略——Flash 用于初始生成（便宜、快速），Pro 用于所有重试（针对 type-scope 和 struct-field 错误提供更深层的 RTL 推理）——在最大化修复质量的同时限制了成本。无需 GPU，无需 fine-tuning；仅使用 NVIDIA NIM 免费层额度。 该流水线涵盖了完整的 NS31A 语料库：**46 个安全 SVA**（形式化的 NS31A 断言，适配 Ibex 信号）和 **22 个安全属性**（仅包含英文描述，框架直接从中生成形式化的 SVA）。 3. **两步行业标准验证门控和 TAR 指标。** 每个翻译后的断言在计入结果前必须通过两道门控：首先是 QuestaSim SVA 编译（语法），然后是 JasperGold FPV 在干净的 RTL 上 Proven + non-vacuous（语义）。TAR（翻译接受率 = proven\_non\_vacuous / total\_ns31a\_groups）用于衡量经过机械验证的翻译质量——而非 LLM 自我报告或 BLEU/ROUGE。应用于从 NS31A 到 Ibex 的 9 个安全模块，无需人工移植任何断言。 ## 设置 ### 一键检查 完成以下步骤后： ``` python scripts/setup_env.py ``` ### 步骤 1 — Python 依赖 ``` python -m pip install -r requirements.txt ``` 安装：`pyverilog`、`pandas`、`openai`、`python-dotenv`。 ### 步骤 2 — NVIDIA NIM API 密钥 在 [build.nvidia.com](https://build.nvidia.com) 获取免费的 API 密钥（1000 个免费额度）。 在项目根目录创建一个 `.env` 文件： ``` NVIDIA_API_KEY=nvapi-...your-key-here... ``` `.env` 文件已被 gitignore——请勿将其提交。 **无需 GPU。无需付费订阅。只需免费的 NVIDIA 开发者账户。** ### 步骤 3 — Ibex RTL + NS31A 数据（已包含在仓库中） - `rtl/ibex/original/` — 干净的 Ibex RTL（只读，请勿修改） - `assertion_dataset/ns31a_.csv` — NS31A 断言源文件 ## 运行流水线 ### 本地模式 — 步骤 1A + 1B（笔记本电脑，无需 EDA 工具） **单模块：** ``` python scripts/run_step1.py --module pmp --mode local ``` **所有 9 个模块：** ``` python scripts/run_step1.py --all-modules --mode local ``` **单独执行步骤：** ``` python scripts/parse_rtl.py --module pmp # Step 1A: parse RTL python scripts/translate.py --module pmp # Step 1B: translate assertions python scripts/translate.py --module pmp --pro # Step 1B: use Pro model ``` **Dry-run（仅构建 prompt，不调用 API）：** ``` python scripts/translate.py --module pmp --dry-run ``` ### 服务器模式 — 步骤 1C + 1D（QuestaSim + JasperGold） ``` git pull python scripts/run_step1.py --all-modules --mode server ``` ### 检查流水线状态 ``` python scripts/run_step1.py --status ``` ## 笔记本电脑 + 服务器工作流程 ``` # --- LAPTOP（解析 + 翻译，无 EDA 许可证） --- python scripts/run_step1.py --all-modules --mode local git add assertions/translated/ results/logs/ git commit -m "Step1 local: all modules translated" git push # --- SERVER（QuestaSim + JasperGold） --- git pull python scripts/run_step1.py --all-modules --mode server git add results/ errors/ git commit -m "Step1 server: all modules validated" git push # --- LAPTOP（收集结果） --- git pull python scripts/run_step1.py --status ``` ## Ibex 安全模块 | 模块 | RTL 文件 | 类型 | Bind 文件 | |--------|----------|------|-----------| | PMP | `ibex_pmp.sv` | Combinational | `pmp_bind.sv` | | CSR | `ibex_cs_registers.sv` | Sequential | `csr_bind.sv` | | DO | `ibex_controller.sv` | Sequential | `do_bind.sv` | | ETI | `ibex_controller.sv` | Sequential | `eti_bind.sv` | | CF | `ibex_controller.sv` | Sequential | `cf_bind.sv` | | MT | `ibex_controller.sv` | Sequential | `mt_bind.sv` | | MA | `ibex_load_store_unit.sv` | Sequential | `ma_bind.sv` | | IE | `ibex_id_stage.sv` + `ibex_ex_block.sv` | Sequential | `ie_bind.sv` | | RU | `ibex_wb_stage.sv` | Sequential | `ru_bind.sv` | `ibex_controller.sv` 支持 4 个逻辑模块（DO、ETI、CF、MT）。 PMP 是组合逻辑——没有 `@(posedge)`、`##N` 或 `$past()`。 时钟：`clk_i`。复位：`rst_ni`（低电平有效）。 ## 仓库结构 ``` ai-autotrans-rv/ ├── README.md ├── requirements.txt ← pyverilog, pandas, openai, python-dotenv ├── .env ← NVIDIA_API_KEY (gitignored — never commit) │ ├── prompts/ ← prompt templates │ ├── sequential_prompt.txt ← FIXED sequential SVA template │ ├── combinational_prompt.txt ← FIXED combinational SVA template │ └── final/ ← assembled prompts per module (gitignored) │ ├── scripts/ ← Python pipeline scripts │ ├── setup_env.py ← environment checker (run first) │ ├── run_step1.py ← master orchestrator │ ├── parse_rtl.py ← 1A: RV-SigEx (regex-based SV parser) │ ├── translate.py ← 1B: DeepSeek V4-Flash translation │ ├── validate_compile.py ← 1C: QuestaSim compile loop │ └── validate_fpv.py ← 1D: JasperGold FPV baseline │ ├── rtl/ │ └── ibex/ │ ├── original/ ← clean Ibex RTL (parser input — never modify) │ └── trojaned_rtl/ ← trojaned RTL for assertion testing │ ├── assertion_dataset/ ← NS31A source CSV files (one per module) │ ├── assertions/ │ └── translated/ ← SVA bind files (pipeline output) │ ├── results/ │ ├── signals/ ← MODULE_signals.json (parser output) │ ├── logs/ ← MODULE_tar_log.json (translation log) │ ├── raw/ ← LLM raw output per module (gitignored) │ └── step1/ ← FPV reports, vacuity, COV files │ └── errors/ └── archive/ ← QuestaSim + JasperGold error logs (NEVER DELETE) ``` ## 需求摘要 | 工具 | 用途 | 适用步骤 | 安装 | |------|---------|-------------|---------| | Python 3.10+ | 流水线脚本 | 所有步骤 | python.org | | pyverilog | RTL 解析 | 步骤 1A | `pip install pyverilog` | | pandas | CSV 处理 | 步骤 1B | `pip install pandas` | | openai | NVIDIA NIM API 客户端 | 步骤 1B | `pip install openai` | | python-dotenv | .env 文件加载 | 步骤 1B | `pip install python-dotenv` | | NVIDIA NIM 账户 | 免费 API 额度 | 步骤 1B | build.nvidia.com | | QuestaSim | SVA 编译 | 步骤 1C | EDA 服务器 | | JasperGold | 形式化验证 | 步骤 1D | EDA 服务器 | **步骤 1A + 1B 完全在笔记本电脑上运行。无需 GPU。无需付费订阅。** ## LLM 模型层级 | 模型 | ID | 用途 | |-------|----|---------| | DeepSeek V4-Flash | `deepseek-ai/deepseek-v4-flash` | 仅用于初始翻译（步骤 1B） | | DeepSeek V4-Pro | `deepseek-ai/deepseek-v4-pro` | 所有重试：QuestaSim 编译（步骤 1C）+ JasperGold FPV（步骤 1D） | 两者均通过 NVIDIA NIM 调用（OpenAI 兼容 API，`https://integrate.api.nvidia.com/v1`）。 `temperature=0.0`，`seed=42` 以保证可复现性。 ## RV-SigEx — RISC-V 信号提取器 `scripts/parse_rtl.py` 实现了 **RV-SigEx**，一个基于 regex 的 SystemVerilog 信号提取器。 **提取内容：** - 端口声明（inputs/outputs），包含位宽和方向 - 内部信号（logic/wire/reg 以及 typedef 类型的 enum/struct 变量） - Parameters - 包类型（来自 ibex_pkg.sv 的 typedef enum/struct），按模块过滤 - 连通性（assign 语句 + always_comb 块赋值） **在 Ibex 上验证（9 个模块）：** | 模块 | RTL 文件 | Inputs | Outputs | Internals | PkgTypes | |--------|----------|--------|---------|-----------|----------| | pmp | ibex_pmp.sv | 7 | 1 | 12 | 4 | | csr | ibex_cs_registers.sv | 44 | 27 | 109 | 9 | | do/eti/cf/mt | ibex_controller.sv | 38 | 27 | 39 | 7 | | ma | ibex_load_store_unit.sv | 13 | 18 | 20 | 0 | | ie | ibex_id_stage.sv + ibex_ex_block.sv | 64 | 77 | 89 | 15 | | ru | ibex_wb_stage.sv | 15 | 15 | 18 | 1 | 完整统计信息：[`results/signals/parser_stats.txt`](results/signals/parser_stats.txt) **可复现性：** 每次重新运行时 `git diff results/signals/` 结果均为空。 **通用用法：** ``` python scripts/parse_rtl.py --sv-file path/to/any_module.sv python scripts/parse_rtl.py --sv-file path/to/any_module.sv --pkg-file path/to/pkg.sv ``` ## TAR 指标 ``` TAR = proven_assertions / total_ns31a_groups × 100 (per module) ``` - `proven_assertions` — 通过 JasperGold FPV（Proven + non-vacuous）的断言，无需任何人工干预 - `total_ns31a_groups` — 源 CSV 中的 NS31A 断言组数量 TAR 由 `validate_fpv.py` 计算并存储在 `results/logs/_tar_log.json` 中。 翻译步骤（步骤 1B）的目标是 100% 的翻译覆盖率；TAR 则会进一步筛选，仅保留经过形式化验证的内容。 ## 与其他论文的关系 | 论文 | 作用 | |-------|------| | ISCAS（我们团队） | 上游背景 — 在 §1 中引用 | | Chuah MEMOCODE 2023 | NS31A 断言语料库的来源 | | AutoAssert/TrustAssert DATE 2026 | 不同的问题（生成，而非翻译） | | SecMetric 期刊论文 | 下游配套 — 承接阶段 2-5 | ## 致谢 基于 **lowRISC Ibex** RISC-V 处理器（Apache 2.0）构建。 NS31A 断言语料库来自 **Chuah 等人，MEMOCODE 2023**。 由爱沙尼亚研究委员会资助 **PSG837**。 ## 开发工具 | 工具 | 作用 | |------|------| | [Claude Code](https://claude.ai/code) (Anthropic) | 流水线代码开发、脚本优化、bug 修复和手稿撰写协助 | | [NVIDIA NIM](https://build.nvidia.com) | 为所有 DeepSeek V4-Flash 和 V4-Pro API 推理调用提供免费开发者额度 | ## 引用 ``` @inproceedings{imtiaz2026bec, title = {{AI}-{AutoTrans}: {AI}-Assisted Automatic Translation of Security Assertions for {RISC-V} Processors}, author = {Imtiaz, Sharjeel and Reinsalu, Uljana and Ghasempouri, Tara}, booktitle = {Baltic Electronic Conference (BEC)}, year = {2026} } ``` ## 许可证 MIT — 详见 [LICENSE](LICENSE) 文件。 **联系方式：** sharjeel.imtiaz@taltech.ee

标签：AI辅助翻译, DeepSeek, DLL 劫持, FPV, HDL, Ibex, JasperGold, LLM, NS31A, NVIDIA NIM, Python, QuestaSim, RISC-V, RTL, SVA, SystemVerilog断言, Unmanaged PE, 人工智能, 代码生成, 处理器安全, 大语言模型, 安全工程, 安全断言, 寄存器传输级, 形式化验证, 无后门, 模板匹配, 渗透测试工具, 熵值分析, 用户模式Hook绕过, 硬件安全, 硬件验证, 自动化验证, 自动翻译, 芯片设计, 逆向工具