# SATinUVM：SAT-UVM 混合验证平台

**Repository Path**: di_zhao/SATinUVM

## Basic Information

- **Project Name**: SATinUVM：SAT-UVM 混合验证平台
- **Description**: SATinUVM 是一个面向数字 IC 子模块验证的流程管理与制品整合平台，把“形式化证明（SAT/SMT）”和“动态仿真（UVM）”两条互补的验证通路，统一收敛到**同一份冻结的 SVA 断言文件**上，并用 AI Coding 大模型半自动化生成断言，再经人工评审冻结后作为两条通路的唯一断言源。
- **Primary Language**: Unknown
- **License**: Not specified
- **Default Branch**: master
- **Homepage**: None
- **GVP Project**: No

## Statistics

- **Stars**: 0
- **Forks**: 0
- **Created**: 2026-09-09
- **Last Updated**: 2026-09-09

## Categories & Tags

**Categories**: Uncategorized

**Tags**: None

## README

# SATinUVM · 模式一 SAT-UVM 混合验证平台

> SAT 负责子模块完备证明 · UVM 负责全系统动态仿真 · 共享同一套 SVA 断言

SATinUVM 是一个面向数字 IC 子模块验证的**流程管理与制品整合平台**。它把“形式化证明（SAT/SMT）”和“动态仿真（UVM）”两条互补的验证通路，统一收敛到**同一份冻结的 SVA 断言文件**上，并用 AI Coding 大模型半自动化生成断言，再经人工评审冻结后作为两条通路的唯一断言源。

本仓库是“模式一”流程的完整工具实现：包含浏览器前端、零依赖本地验证服务（[server.js](file:///d:/code/SATinUVM260901/server.js)）、内置 OSS CAD Suite（sby/yosys/z3）以及一组演示物料。

---

## 目录

- [1. 这是什么](#1-这是什么)
- [2. 为什么是“模式一”](#2-为什么是模式一)
- [3. 核心特性](#3-核心特性)
- [4. 整体架构](#4-整体架构)
- [5. 目录结构](#5-目录结构)
- [6. 七阶段工作流](#6-七阶段工作流)
- [7. 快速开始](#7-快速开始)
- [8. AI 接口配置](#8-ai-接口配置)
- [9. 真实运行环境搭建](#9-真实运行环境搭建)
- [10. server.js 的 yosys 兼容降级链](#10-serverjs-的-yosys-兼容降级链)
- [11. server.js 的 UVM 兼容降级链](#11-serverjs-的-uvm-兼容降级链)
- [12. SVA 静态检查清单（10 项）](#12-sva-静态检查清单10-项)
- [13. 数据持久化与项目导入导出](#13-数据持久化与项目导入导出)
- [14. 演示物料与样本](#14-演示物料与样本)
- [15. 本地验证服务 API](#15-本地验证服务-api)
- [16. 常见问题](#16-常见问题)
- [17. 技术栈与依赖](#17-技术栈与依赖)

---

## 1. 这是什么

芯片子模块（尤其是控制密集型状态机，如 IOMMU 翻译控制）验证有两条主流路径：

- **形式化证明（Formal / SAT-SMT）**：基于 SymbiYosys(yosys + z3) 做 BMC（边界模型检测）/ k-induction，穷尽合法输入空间，能在仿真跑不到的边界发现 bug，但只能作用于**子模块**且对断言语法兼容性要求苛刻。
- **UVM 动态仿真**：用随机激励跑全系统，覆盖率驱动，能验证集成行为与跨模块握手，但**无法穷尽**，覆盖率到 100% 也不等于无 bug。

两条路径互补，但传统流程里它们用**两套断言**，容易漂移、对不上。模式一的关键约束是：

> **同一份 SVA 断言文件，SAT 与 UVM 都用它，谁都不能单独改。**

SATinUVM 把这条约束做成了一个可执行的工具：从 Spec 录入 → Prompt 生成 → AI 出断言 → 评审 → 冻结 → 并行验证 → 汇总报告，全程门控、全程留痕、全程可回流。

### SAT 与 UVM 的相互关系

**① 互补验证，各管一面**

| 维度 | SAT（形式证明） | UVM（动态仿真） |
| --- | --- | --- |
| 策略 | **穷尽**所有合法输入，数学证明 | **随机**激励跑有限用例，覆盖率驱动 |
| 擅长 | 边界条件、死锁、非法状态等仿真难触达的 bug | 集成行为、跨模块握手、时序交互 |
| 局限 | 只能作用于子模块，状态空间爆炸会超时 | 无法穷尽，100% 覆盖率 ≠ 无 bug |
| 结果 | 属性级 Pass/Fail/Inconclusive + 反例波形 | 用例通过率 + 功能/条件覆盖率 + cover 命中 |

SAT 能发现仿真跑不到的边界 bug（如演示 DUT 里 `devid_illegal && mode==TRANSLATED` 的 Spec 冲突），UVM 能验证 SAT 管不到的全系统集成行为。两者互补，缺一不可。

**② 共享同一份冻结 SVA——核心约束**

```
          ┌─────────────────────────┐
          │  dut_formal.frozen.sv    │
          │  （冻结，SHA-256 签名）   │
          └────────┬────────┬───────┘
                   │        │
          ┌────────┴──┐  ┌──┴────────┐
          │ 通路 A SAT │  │ 通路 B UVM │
          │ yosysCompat│  │ uvmCompat  │
          │  降级喂 sby│  │ 预处理喂vlog│
          └───────────┘  └───────────┘
```

阶段 5 冻结的 SVA 是唯一断言源，谁都不能单独改。冻结后任何修改都触发"解除冻结 → 重新评审 → 重新冻结"，杜绝两路用不同断言导致结果对不上。

**③ 同一份 SVA，两套降级——方向相反**

这是技术上的关键点。同一份 SVA，两个通路对它做的预处理完全相反：

| 语法 | SAT 侧（yosysCompat） | UVM 侧（uvmCompat） |
| --- | --- | --- |
| `assert property` | 拆成 immediate 断言（yosys 不支持 concurrent SVA） | **保留**原貌，仅补 `@(posedge clk)` |
| `bind` | 删掉，改成模块内直接实例化 | **保留**（仿真器支持） |
| `inside {}` | 降级为 `==` + `\|\|` | **保留** |
| `$isunknown` | 整条注释跳过 | **保留** |
| `disable iff` | 转成 `!R &&` 前置守卫 | **保留** |
| 上电复位 | 注入 POR `assume` | 不需要（tb 有真实复位序列） |

SAT 把 concurrent SVA 降级为 immediate 是因为 yosys 前端不支持；UVM 保留 concurrent SVA 原貌是因为商用仿真器原生支持。两条路走不同方向，但验证的是同一条断言。

**④ 顶层模块名共享**

SAT 通路运行时 `askTop` 确认的顶层模块名会记住并存入项目，UVM 通路运行时复用这个名字传给 server，让 `fixBindTarget()` 能校正 AI 猜错的 bind 目标。

> **一句话总结：SAT 证明"不可能出错"的边界，UVM 验证"正常能跑通"的路径，两者用同一份冻结 SVA 收敛到同一个验证结论。**

---

## 2. 为什么是“模式一”

| 通路 | 职责 | 绑定对象 | 工具 | 产出 |
| --- | --- | --- | --- | --- |
| 通路 A · SAT | 子模块**完备证明**（穷尽合法输入） | 子模块 DUT | SymbiYosys(BMC) | `sat_result.rpt`（属性级 Pass/Fail/Inconclusive + 反例） |
| 通路 B · UVM | 全系统**动态仿真** | 顶层 DUT | ModelSim SE-64 10.4（已适配）或 Questa/VCS/Xcelium | `uvm_sim.rpt`（用例通过率 + 功能/条件覆盖率 + cover 命中） |
| 共享源 | 两条通路**唯一断言源** | — | — | `dut_formal.frozen.sv`（冻结，SHA-256 签名） |

“模式一”即 SAT + UVM 并行、共享断言；另有模式二/三（SAT 局部 + UVM 局部等）不在本工具范围。

---

## 3. 核心特性

- **七阶段门控流程**：前一阶段制品未就绪则后一阶段锁死，强制按顺序收敛，避免跳步漏检。
- **5 段式标准化 Prompt**：把 Spec / 约束 / 输出约定 / 硬件规约 / 端口清单固定成模板，AI 生成质量稳定可复现。
- **AI Coding 多模型接入**：内置 DeepSeek / 通义千问 / 智谱 GLM / Kimi / OpenAI / Claude / 百度千帆 / 豆包 等商业预设，以及 Ollama / LM Studio / vLLM 本地部署；多档案切换，Key 不落前端 localStorage 之外。
- **AI 反馈回流闭环**：生成失败、自动检查、SAT 运行失败的问题清单可一键追加到 Prompt 末尾，迭代次数自增，强制 AI 逐条修复。
- **冻结即唯一源**：SVA 评审通过后冻结为 `dut_formal.frozen.sv`，计算 SHA-256 与版本号；冻结后任何修改都触发“解除冻结 → 重新评审 → 重新冻结”流程，杜绝两路用不同断言。
- **DUT + 断言绑定输出**：自动把载入的 DUT 设计源码与冻结断言合并为单文件 `dut_assert_bound.sv`，可直接整体编译，无需再单独 `bind`。
- **真实运行 / 导入 / 模拟三态数据源**：没装 EDA 工具也能用"模拟"跑通全流程演示；有工具就"真实运行"；已有结果报告就"导入"。
- **server.js 零依赖**：仅用 Node 内置 `http/fs/path/child_process`，无需 `npm install`；自动探测项目目录下的 OSS CAD Suite 并注入 PATH。
- **yosys 前端兼容降级链**（SAT 侧）：AI 生成的 SVA 常含 yosys 不支持的语法（`assert property` / `bind` / `inside` / 未打包数组参数 / `'{...}` / `##N`），server.js 在喂给 sby 前做 7 步等价降级，让 BMC 真跑得起来。
- **UVM 商用仿真器兼容降级链**（UVM 侧）：`uvmCompat()` 把冻结 SVA 预处理为 ModelSim/VCS/Xcelium 可编译的格式——给裸 `assert/cover property` 自动补 `@(posedge clk)`、注释掉 `?:` 内含 `##N` 的非法断言、清除 `//else $error` 注释中被误解析的 `else` 关键字；`stripAssertDup()` 跨文件去重断言模块；`fixBindTarget()` 自动校正 AI 猜错的 bind 目标模块名；`genTbTop()` 从 bind 语句自动生成 testbench 和 run.do；`dutPortDirs()` 解析端口方向让 tb 只驱动输入信号。
- **ModelSim SE-64 10.4 开箱即用**：UVM 通路已适配 ModelSim 10.4（2014.12），命令模板预置 `vlib work` → `vlog -sv` → `vsim -c -do run.do` 全流程；server.js 自动生成 `compile.bat`（绕过 cmd.exe `for %%f` 转义问题），自动拷贝 `modelsim.ini`，自动从日志解析用例结果与覆盖率。
- **日志一键复制**：SAT 运行日志与 UVM 仿真日志均带「复制」按钮，一键拷贝全文到剪贴板；日志区域移至表格上方，左右两栏视线对齐，高度统一限制 320px 内滚动。
- **10 项 SVA 静态检查**：复位保护、系统任务、bind、纯净性、状态参数化、端口一致、全局不变量、Spec 覆盖、cover 点、yosys 语法兼容。
- **自动验证结论**：报告根据 SAT 全 Pass、UVM 全过、覆盖率达标、无未命中 cover 点四条件自动判定“通过 / 有条件通过 / 不通过”。

---

## 4. 整体架构

```
┌─────────────────────────────────────────────────────────────┐
│  浏览器前端（index.html + css + js/*.js，无框架、无构建）      │
│  ┌──────────┐ ┌──────────┐ ┌────────┐ ┌──────────────────┐ │
│  │ store.js │ │  fsm.js  │ │prompt.js│ │  sva.js / ai.js  │ │
│  │ 持久化    │ │ FSM 解析 │ │5段生成 │ │ 静态检查/AI调用 │ │
│  └────┬─────┘ └──────────┘ └────────┘ └────────┬─────────┘ │
│       │ localStorage（全量存）         fetch /api/*          │
│       └────────────────┬────────────────────────┘           │
└────────────────────────┼────────────────────────────────────┘
                         │ HTTP（默认 :8898）
┌────────────────────────┼────────────────────────────────────┐
│  本地验证服务 server.js（Node 内置模块，零依赖）             │
│  ┌──────────┐  ┌──────────────┐  ┌────────────────────────┐ │
│  │静态托管   │  │ /api/sat     │  │ yosysCompat() 降级链   │ │
│  │ index.html│  │ 调 sby 做 BMC│  │  SVA→immediate 等价  │ │
│  └──────────┘  └──────┬───────┘  └───────────┬────────────┘ │
│                ┌──────┴───────┐  ┌───────────┴────────────┐  │
│                │ /api/exec    │  │ uvmCompat() 降级链      │  │
│                │ UVM 仿真命令 │  │  SVA→商用仿真器兼容    │  │
│                └──────┬───────┘  └───────────┬────────────┘  │
│                       │ spawn                 │               │
│  ┌────────────────────┼───────────────────────┼─────────────┐ │
│  │ OSS CAD Suite（SAT）│  ModelSim SE-64 10.4（UVM）         │ │
│  │ sby/yosys/z3/...   │  vlog/vsim/vlib                     │ │
│  └────────────────────┴──────────────────────┴─────────────┘ │
└──────────────────────────────────────────────────────────────┘
```

- **前端**：纯原生 JS，单页应用，7 个阶段视图靠 [app.js](file:///d:/code/SATinUVM260901/js/app.js) 里的 `s1()~s7()` 渲染。数据全量存在 `localStorage`（key `satinuvm_data_v1`），AI/EDA 设置另同步一份到服务端文件（`work/settings.json`），换端口/换浏览器不丢 API 配置。
- **服务端**：[server.js](file:///d:/code/SATinUVM260901/server.js) 既是静态文件服务器，又是 EDA 代理 + 双路 SVA 降级器（SAT 侧 `yosysCompat()`，UVM 侧 `uvmCompat()`）；浏览器沙箱不能起本地进程，所以阶段 6 的"真实运行"一律走它。
- **EDA 工具**：SAT 侧用仓库内置 `oss-cad-suite-windows-x64-20260828/`，server.js 启动时自动探测并把 `bin/`、`lib/` 注入 `PATH`；UVM 侧适配 ModelSim SE-64 10.4（命令模板里直接用全路径调用 `vlog.exe`/`vsim.exe`），也可改用 QuestaSim / VCS / Xcelium / WSL 内开源流程。

---

## 5. 目录结构

```
SATinUVM260901/
├── index.html              # 前端入口，加载 css 与 7 个 js
├── server.js               # 本地验证服务（静态托管 + EDA 代理 + SVA 降级）
├── smoke2.js               # 临时冒烟脚本（跑 iommu_sm + 修正断言的真实 sby，非必需）
├── README.md               # 本文档
│
├── css/
│   └── style.css           # 全部样式（顶栏、流程条、卡片、表格、报告）
│
├── js/
│   ├── store.js            # 数据模型 + localStorage 持久化 + 服务端设置同步
│   ├── fsm.js               # FSM 跳转规则解析与语法检查（源--(条件)-->目标）
│   ├── prompt.js            # 5 段式 Prompt 生成与结构完整性检查
│   ├── sva.js               # SVA 静态检查(10项) + 属性/cover/bind 解析 + SHA-256
│   ├── ai.js                # AI Coding 接口（OpenAI 兼容 + Anthropic Claude 两种协议）
│   ├── report.js            # 模式一验证报告生成与自动结论判定
│   └── app.js               # 主界面：7 阶段渲染与全部交互逻辑（最大文件）
│
├── oss-cad-suite-windows-x64-20260828/
│   └── oss-cad-suite/      # 内置 EDA 工具集（sby/yosys/z3/iverilog/verilator…）
│       ├── bin/  lib/  etc/ share/
│       ├── environment.bat / .ps1   # 官方环境脚本（本项目用自动注入，不直接调）
│       └── VERSION / README
│
├── test/                   # 演示物料与样本
│   ├── iommu_sm.sv                 # 演示 DUT：IOMMU 状态机（模块名固定 dut，8 状态 FSM）
│   ├── xxx_spec.md                 # 演示 Spec（IOMMU 翻译控制状态机功能规约）
│   ├── dut_assert_bound.sv         # DUT+断言绑定样本（自动生成器产出样例）
│   ├── dut_assert_bound (1~4).sv   # 多版本绑定文件（迭代历史）
│   ├── dut_formal.sv / .frozen.sv  # 断言文件与冻结样本
│   ├── dut_formal_bad.sv           # 含已知问题的断言（用于演示检查失败回流）
│   ├── dut_formal_deepseek.sv      # DeepSeek 生成样本
│   ├── signal_list.txt             # 信号清单样本
│   ├── fsm_transitions.txt / _bad  # FSM 跳转规则样本（好/坏）
│   ├── sva_gen_prompt.txt          # 5 段式 Prompt 样本
│   ├── sat_result.rpt              # SAT 形式证明结果样本
│   ├── uvm_sim.rpt                 # UVM 仿真结果样本
│   ├── demo_project.satinuvm.json  # 可导入的演示项目（阶段 1 顶栏「导入」用）
│   ├── ai_feedback.txt / (1).txt   # AI 反馈清单样本
│   └── OASIS-AI_2026_paper_2.pdf    # 相关论文参考
│
└── work/                   # 运行时工作目录（server.js 自动创建）
    ├── settings.json       # AI/EDA 设置的服务端持久化副本
    ├── sat_<时间戳>/       # 每次 /api/sat 的 BMC 运行目录
    │   ├── config.sby      # 自动生成的 SymbiYosys 配置
    │   ├── <src>.sv        # 经 yosysCompat 降级后的源码
    │   └── config/         # sby 标准布局：engine_0/ model/ src/ + PASS|FAIL|ERROR
    └── exec_<时间戳>/      # 每次 /api/exec 的 UVM 命令工作目录
        ├── *.sv            # 经 uvmCompat 预处理后的 DUT + SVA 源码
        ├── compile.bat     # 自动生成的编译脚本（逐文件 vlog -sv）
        ├── tb_top.sv       # 从 bind 语句自动生成的 testbench
        ├── run.do         # 自动生成的 vsim 运行脚本（run -all; quit -f）
        └── modelsim.ini  # 自动从安装目录拷贝
```

---

## 6. 七阶段工作流

顶栏流程条（`#stepper`）按 [app.js](file:///d:/code/SATinUVM260901/js/app.js) 的 `NAMES` 渲染七步，`unlocked(n)` / `done(n)` 做门控与完成态判定，未就绪的阶段显示锁图标且不可点击。

### 阶段 1 · 输入准备（产出 `xxx_spec.md` + `signal_list.txt`）

录入三件输入源，作为 5 段式 Prompt 的素材：

- **模块功能 Spec**：自由文本，含状态跳转、握手时序、异常条件、边界条件。可 `📂 载入文件`（`.md/.txt/.log`）或下载。
- **信号清单**：表格化录入信号名 / 方向（输入/输出/内部/时钟/复位）/ 说明。支持「批量粘贴」或从文件载入，解析规则见 [app.js `addSignalsFromText`](file:///d:/code/SATinUVM260901/js/app.js)（支持中英方向词：`input/输入`、`clk/时钟` 等）。
- **FSM 跳转规则**：每行一条 `源状态--(条件表达式)-->目标状态`。点「语法检查」由 [fsm.js](file:///d:/code/SATinUVM260901/js/fsm.js) 解析，检查括号配平、`and/or` 错误运算符、`$` 系统任务、顶层 `&` 与 `||` 未分组歧义，并做重复/条件重叠检测。

> 阶段 2 解锁条件：`spec / transitions / signals` 任一非空。

### 阶段 2 · 编写 5 段式 Prompt（产出 `sva_gen_prompt.txt`）

固定五段结构，由 [prompt.js](file:///d:/code/SATinUVM260901/js/prompt.js) 的 `build()` 用阶段 1 制品自动拼装：

1. **任务总述**：生成独立 `dut_formal.sv`，外部 `bind` 挂载，不修改 Chisel 生成的 RTL，SVA 同时供 SymbiYosys 与 UVM。
2. **硬性工程约束**（10 条）：仅 `property/assert/cover`、`bind` 外部绑定、必带 `disable iff(!rst_n)`、状态用 `localparam`、严格遵循 Spec 不脑补、兼容两套工具、每条加注释、全局不变量、bind 端口一一对应、结尾分号不附 `else $error`。
3. **输出格式与文件约定**：只输出断言模块 + bind 语句，不要 testbench / 激励。
4. **硬件 Spec 规约**：Spec 文本 + 状态列表 + 跳转规则 + 全局不变规则。
5. **信号端口列表**：`信号名<TAB>方向<TAB>说明`。

点「从阶段 1 自动生成」一键填充，可手动改。「结构检查」按 `sections()` 验证 5 段齐全。若上一版有 AI 反馈，可「把上一版问题清单回流到 Prompt」。

> 阶段 3 解锁条件：`prompt` 非空。

### 阶段 3 · AI 生成 SVA（产出 `dut_formal.sv`）

- 调用 AI 大模型生成断言，或「手动粘贴」/「载入文件」。每次生成结果入 `svaHistory`，可随时回看 / 设为当前。
- 生成完**就地预检**（[sva.js `checks`](file:///d:/code/SATinUVM260901/js/sva.js)），发现问题即记 AI 反馈并弹窗询问导出 txt。
- 直接编辑文本框会重置阶段 4 评审状态（`f('sva', ...)` 内置保护）。

> 阶段 4 解锁条件：`sva` 非空。

### 阶段 4 · 人工评审（产出评审记录）

- **自动静态检查（10 项 C1–C10）**：见 [第 11 节](#11-sva-静态检查清单10-项)。存在 `fail` 项时评审按钮禁用。
- **人工确认项（4 项）**：Spec 覆盖完整、无仿真/形式化不兼容语法、无过约束/欠约束、cover 点完备。全部勾选 + 自动检查无 fail → 可「评审通过」。
- **评审不通过**：点「评审不通过 → 回流修改 Prompt」会自增 `iterations`、重置人工勾选、跳回阶段 2，并把自动检查的 fail/warn 清单追加到 Prompt 末尾（[app.js `failToPrompt`](file:///d:/code/SATinUVM260901/js/app.js)）。
- **评审备注**：可选，写入最终验证报告。

> 阶段 5 解锁条件：`review.passed === true`。

### 阶段 5 · 冻结共享 SVA（产出 `dut_formal.frozen.sv` + `dut_assert_bound.sv`）

**关键里程碑**。点「执行冻结」：

- 计算 SVA 的 SHA-256（[sva.js `hashText`](file:///d:/code/SATinUVM260901/js/sva.js)，`file://` 下 `crypto.subtle` 不可用时退化为 FNV-1a）。
- 版本号 `v{freezeCount}.0`，`freezeCount` 自增。
- 冻结后 `dut_formal.sv` 若被改（`p.sva !== p.frozen.content`），页面显示「已偏离冻结版本」警告，需解除冻结重走流程，或「恢复为冻结版本」。

**DUT + 断言绑定**（[app.js `genBound`](file:///d:/code/SATinUVM260901/js/app.js)）：

- 把载入的 DUT 设计源码（与阶段 6 共用 `p.sat.dutSrcs`）与冻结断言合并为单文件 `dut_assert_bound.sv`，带文件头注释（项目、时间、断言版本、SHA-256、组成）。
- 自动解析 `bind` 目标模块名并校验是否在 DUT 文件中存在；若 DUT 文件已含断言模块则禁止再绑定（防重复定义）。
- 该单文件可直接整体交给 yosys(`read -formal -sv`) / 仿真器，无需再单独 `bind`。

> 阶段 6/7 解锁条件：`frozen` 非空。

### 阶段 6 · 并行验证（产出 `sat_result.rpt` + `uvm_sim.rpt`）

左右双通路，共用同一冻结 SVA。每路支持 4 种数据来源（状态 tag 颜色区分）：

| 来源 | 说明 | tag |
| --- | --- | --- |
| 真实运行 | 调 server.js 跑本地 EDA | `pass` 绿 |
| 导入 | 从本地 `.rpt/.txt/.log` 文件解析 | `info` 蓝 |
| 模拟 | 用演示假数据跑通流程 | `warn` 黄 |
| 手动 | 直接编辑表格 / 输入框 | `ice` 青 |

**通路 A · SAT-SMT 形式证明**：

- 「解析冻结 SVA 属性」：从冻结文件提取所有 `property` 声明与标签式 `assert property`（[sva.js `extractProps`](file:///d:/code/SATinUVM260901/js/sva.js)）。
- 「真实运行 SymbiYosys」：先 `askTop` 确认顶层模块（按 `bind` 目标 + DUT 文件实际模块自动识别，bind 目标不在文件里时回落首个真实模块），再 POST `/api/sat`。server.js 做 yosys 兼容降级 → 生成 `config.sby` → 跑 `sby -f config.sby`（BMC，深度 20，引擎 `smtbmc z3`，超时 15 分钟）。
- 结果映射：`DONE (PASS,` → 全 Pass；`FAIL` → 从日志正则定位失败断言名标 Fail，其余 Inconclusive；`ERROR` → 记 yosys 编译错误到 AI 反馈，弹窗询问导出 txt 回流。
- 「模拟运行」：最后一个属性置 Inconclusive，其余 Pass。
- 「导入 sat_result.rpt」：按 `属性名 : PASS/FAIL/INCONCLUSIVE` 每行一条解析，后续行作反例摘要。

**通路 B · UVM 全系统动态仿真**：

- 「解析 SVA cover 点」：提取所有 `cover property`（[sva.js `extractCovers`](file:///d:/code/SATinUVM260901/js/sva.js)）。
- 「真实运行 UVM」：POST `/api/exec`（带 SAT 确认过的顶层模块名 `top`），命令模板在设置里配。server.js 自动完成以下全流程：
  1. **文件名清洗**：把带空格/括号的文件名统一为 `[\w.\-]` 安全格式（`dut_assert_bound (4).sv` → `dut_assert_bound__4_.sv`）。
  2. **`uvmCompat()` 预处理**：给裸 `assert/cover property` 补 `@(posedge clk)`、注释 `?:` 内 `##N` 非法断言、清除 `//else $error` 注释中的 `else` 关键字。
  3. **`stripAssertDup()` 跨文件去重**：bound 版 DUT 常含与 frozen SVA 同名的断言模块和重复 bind，自动注释掉重复部分（大小写不敏感）。
  4. **`fixBindTarget()` bind 目标校正**：AI 常按 Spec 名猜 DUT 模块名（如写 `iommu_sm`），自动改绑到文件中的真实顶层（如 `dut`）。
  5. **`genTbTop()` 自动生成 testbench**：从 bind 语句提取 DUT 端口列表，`dutPortDirs()` 解析端口方向（输入用 `logic` 驱动、输出用 `wire` 不驱动），生成最小 tb_top.sv + run.do。
  6. **`compile.bat` 自动生成**：绕过 cmd.exe `for %%f` 转义问题，逐文件 `vlog -sv`。
  7. 执行命令模板（`{work}` 替换为工作目录），超时 30 分钟。
- 日志解析（[app.js `applyUvmText`](file:///d:/code/SATinUVM260901/js/app.js)）：识别 `TEST 名 : PASS/FAIL`、`FUNC_COVERAGE : xx`、`COND_COVERAGE : xx`、`COVER 名 : HIT/MISS`，自动填表。
- **日志一键复制**：SAT 运行日志和 UVM 仿真日志各带「复制」按钮（[app.js `copySatLog`/`copyUvmLog`](file:///d:/code/SATinUVM260901/js/app.js)），日志区域移到表格上方左右对齐。

### 阶段 7 · 汇总报告（产出 `mode1_verification_report.md`）

点「生成 / 刷新报告」由 [report.js `build`](file:///d:/code/SATinUVM260901/js/report.js) 合并两路结果，输出含：

- 报告头：时间、模块名、冻结 SVA 版本 + SHA-256 前 16 位 + 冻结时间、迭代次数、验证策略。
- 输入制品统计：Spec 字符数、信号数、FSM 跳转数 / 状态数、Prompt 是否编写。
- SAT 证明表：每属性 Pass/Fail/Inconclusive + 反例摘要。
- UVM 仿真表：用例通过率、功能/条件覆盖率（目标 ≥ 设置值，默认 95%）、cover 点命中表。
- 风险点：Inconclusive 属性、Fail 属性、未命中 cover 点。
- 自动结论：
  - 任一通路未运行 → **待验证**
  - 有 Fail 属性或失败用例 → **不通过**
  - 无 Fail 但有 Inconclusive / 未命中 cover / 覆盖率未达标 → **有条件通过**
  - 全 Pass + 全过 + 覆盖率达标 + 无未命中 cover → **通过**

---

## 7. 快速开始

### 7.1 启动服务

仓库自带 OSS CAD Suite 与前端，**不需要 `npm install`**（server.js 仅用 Node 内置模块）。

```powershell
# 在项目根目录
node server.js            # 默认端口 8898
# 或自定义端口
node server.js 9000
```

启动后控制台会打印：

```
SATinUVM 本地验证服务已启动: http://localhost:8898
已自动加载 OSS CAD Suite: d:\code\SATinUVM260901\oss-cad-suite-windows-x64-20260828\oss-cad-suite
工具检测: sby=true yosys=true z3=true wslSby=false
阶段 6「真实运行」将通过本服务执行 SAT/UVM。工作目录: d:\code\SATinUVM260901\work
```

浏览器打开 **http://localhost:8898** 即可。若端口被占用，控制台会提示用 `Get-NetTCPConnection -LocalPort 8898` 查 PID 后 `Stop-Process`，或直接访问旧实例。

> 也可双击 `index.html` 用 `file://` 直接打开（纯前端能跑，但阶段 6 真实运行与设置服务端持久化不可用，会静默降级为纯 localStorage）。

### 7.2 跑一遍演示流程

1. 顶栏「导入」→ 选 [test/demo_project.satinuvm.json](file:///d:/code/SATinUVM260901/test/demo_project.satinuvm.json)。
2. 或手动：阶段 1 载入 `test/xxx_spec.md`、`test/signal_list.txt`、`test/fsm_transitions.txt`。
3. 阶段 2 点「从阶段 1 自动生成」得到 Prompt。
4. 阶段 3 配好 AI 接口（见 [第 8 节](#8-ai-接口配置)）后「调用 AI 生成」，或直接「载入文件」`test/dut_formal.sv`。
5. 阶段 4 「运行自动检查」→ 勾 4 个人工项 → 「评审通过」。
6. 阶段 5 「载入 DUT 设计文件」选 [test/iommu_sm.sv](file:///d:/code/SATinUVM260901/test/iommu_sm.sv) → 「将 DUT 与断言绑定」→ 「执行冻结」。
7. 阶段 6 「解析冻结 SVA 属性」+「解析 SVA cover 点」→ 「真实运行 SymbiYosys」（或「模拟运行」体验流程）。
8. 阶段 7 「生成报告」→ 「下载报告」。

> 演示 DUT `iommu_sm.sv` 内置一处已知 Spec 冲突（断言 3.1.1 与 5.1 互斥），真实运行时 3.1.1 会在 `devid_illegal && mode==TRANSLATED` 场景报 Fail，属预期结果，用于演示“SAT 发现仿真难触达的边界 bug”。

---

## 8. AI 接口配置

顶栏「⚙ 设置」打开多档案面板（[app.js `openSettings`](file:///d:/code/SATinUVM260901/js/app.js)）。内置厂商预设（[ai.js `PRESETS`](file:///d:/code/SATinUVM260901/js/ai.js)）：

| 厂商 | 协议 | 默认地址 | 默认模型 |
| --- | --- | --- | --- |
| DeepSeek 深度求索 | openai | https://api.deepseek.com | deepseek-chat |
| 通义千问 Qwen（阿里百炼） | openai | https://dashscope.aliyuncs.com/compatible-mode/v1 | qwen-plus |
| 智谱 GLM | openai | https://open.bigmodel.cn/api/paas/v4 | glm-4-plus |
| Kimi 月之暗面 | openai | https://api.moonshot.cn/v1 | moonshot-v1-8k |
| OpenAI GPT | openai | https://api.openai.com/v1 | gpt-4o-mini |
| Anthropic Claude | anthropic | https://api.anthropic.com/v1 | claude-sonnet-4-5 |
| 百度千帆 ERNIE | openai | https://qianfan.baidubce.com/v2 | ernie-4.0-8k |
| 字节豆包（火山方舟） | openai | https://ark.cn-beijing.volces.com/api/v3 | doubao-pro-32k |
| 本地 Ollama | openai | http://localhost:11434/v1 | qwen2.5-coder:7b（无需 Key） |
| 本地 LM Studio | openai | http://localhost:1234/v1 | local-model（无需 Key） |
| 本地 vLLM | openai | http://localhost:8000/v1 | 自定义（无需 Key） |
| 自定义 | openai | — | — |

**两种协议实现**：

- OpenAI 兼容：`POST {apiBase}/chat/completions`，`Authorization: Bearer {apiKey}`，`temperature: 0.2`，非流式。
- Anthropic Claude：`POST {apiBase}/messages`，`x-api-key` + `anthropic-version: 2023-06-01` + `anthropic-dangerous-direct-browser-access: true`（直连浏览器），`max_tokens: 8192`。

**注意事项**：

- 选预设即自动填好官方默认地址与模型，通常只需再填 Key。
- 地址命中预设但模型名空时自动补齐官方默认模型（[ai.js `check`](file:///d:/code/SATinUVM260901/js/ai.js)）。
- 商用 API 多有浏览器跨域限制，本地模型需确认服务已启动且允许跨域；「🔌 测试连通性」发极小请求（`hi`，`max_tokens:4`）并返回耗时 ms。
- 返回内容自动去掉 markdown 代码围栏（` ```systemverilog ` … ` ``` `）。
- 设置存 localStorage 且同步到 `work/settings.json`，换端口/换浏览器不丢配置。

---

## 9. 真实运行环境搭建

### 9.1 SAT 形式证明（SymbiYosys）

**方式一（推荐，开箱即用）**：仓库已内置 `oss-cad-suite-windows-x64-20260828/`，server.js 启动时自动探测并把 `bin/`、`lib/` 加入 `PATH`，Windows 下额外设 `PYTHON_EXECUTABLE` 指向内置 `lib/python3.exe`（sby 依赖）。无需任何手动配 PATH。

**方式二（WSL 内安装）**：在 WSL 内 `apt install yosys oss-cad-suite` 或手动装 sby/z3 并加入 PATH。server.js 检测到本机无 `sby` 时会用 `wsl -e bash -lc "command -v sby"` 探测，命中则通过 WSL 跑 sby（路径用 `toWsl()` 转 `/mnt/d/...`）。

两者都没有时，阶段 6「真实运行 SymbiYosys」会返回安装提示。

### 9.2 UVM 动态仿真

#### 方式一（推荐，已验证）：ModelSim SE-64 10.4

安装 ModelSim 后，在设置里配置命令模板（`{work}` 会被替换为工作目录）。默认模板已预置：

```
cd /d {work} && copy /y C:\modeltech64_10.4\modelsim.ini . && C:\modeltech64_10.4\win64\vlib.exe work 2>&1 && call compile.bat 2>&1 && C:\modeltech64_10.4\win64\vsim.exe -c -do run.do work.tb_top 2>&1
```

如果 ModelSim 安装路径不同，把 `C:\modeltech64_10.4\` 改为你的实际路径即可。server.js 会自动完成：

- 把冻结 SVA + DUT 文件经 `uvmCompat()` 预处理后写入 `work/exec_<时间戳>/`
- 自动生成 `compile.bat`（逐文件 `vlog -sv`，绕过 cmd.exe 转义问题）
- 自动生成 `tb_top.sv`（从 bind 语句提取端口，自动判断输入/输出方向）
- 自动生成 `run.do`（`run -all; quit -f`）
- 自动拷贝 `modelsim.ini`（ModelSim 需要在工作目录找到库映射文件）
- 执行命令，超时 30 分钟

#### 方式二：其他商用仿真器

在设置里填命令模板即可（`{work}` 替换为工作目录）：

- QuestaSim：`vsim -c -do "run -all; quit -f" {work}`
- VCS：`make run`（工作目录内放 Makefile）
- Xcelium：`xrun ...`
- WSL 内开源流程：`wsl -e bash -lc "cd {work} && make run"`

> **注意**：非 ModelSim 的仿真器需要用户自行确保 testbench、编译脚本等文件就绪，server.js 的 `uvmCompat` 预处理和 `genTbTop` 自动生成 testbench 仍然会执行，但 `compile.bat` 和 `run.do` 是 ModelSim 专用格式。

---

## 10. server.js 的 yosys 兼容降级链

AI 生成的 SVA 常含 yosys 前端不支持的语法，直接喂给 sby 必报语法错误。[server.js](file:///d:/code/SATinUVM260901/server.js) 的 `yosysCompat(src, top)` 在生成 `config.sby` 前依次执行 7 步等价降级，每步都加 `[server 自动...]` 注释便于溯源：

| 步骤 | 函数 | 作用 |
| --- | --- | --- |
| 1 | `delUnusedArrayParams` | 删除“未被使用的未打包数组 localparam”（如 `localparam logic [1:0] a [2] = '{...}`），yosys 不支持且 AI 常生成此类冗余声明；仅删未被引用的（按名字出现次数判断） |
| 2 | `lowerConcurrentSVA` | **核心**：concurrent `assert/cover property` → immediate 断言 + 移位寄存器。`|=>` 下一拍蕴含用寄存器链 `d1<=ANTE; d2<=d1&&S1;...` 最终 `if(dK) assert(...)`；`|->` 同拍蕴含直接单拍；`disable iff(R)` 转成 `!R &&` 前置守卫；`or/and` → `\|\|`/`&&`；剥掉体内的 `@(posedge clk)` 统一走 `always @(posedge clk)`；`cover` 用 `if(guard) cover(1'b1)`，`assert` 用 `if(guard && !(expr)) assert(1'b0)` |
| 3 | `rewriteInside` | `lhs inside {a,b,c}` → `((lhs==a) \|\| (lhs==b) \|\| (lhs==c))`，yosys 不支持 `inside` |
| 4 | `dedupModules` | 同名 `module` 重复定义（多为 bound 文件二次载入所致）保留首份，其余整段注释 |
| 5 | `lowerBind` | **核心**：yosys 会**静默忽略 `bind`**（断言模块被当 unused 移除，BMC 变空证）。做法：整句删 bind 原文，再在目标模块体内按断言模块端口同名连接实例化（`.port(port)`）；bind 目标模块不存在时回退顶层模块（AI 常猜错 DUT 模块名） |
| 6 | `dedupInsts` | 多轮处理累积的同名 `dut_formal_assertions` 实例按实例名去重，保留首个，其余注释 |
| 7 | `addPorAssume` | **POR 上电复位假设**：BMC 允许“上电后从未复位”，寄存器初值自由，状态寄存器可能落在非法编码上撞“状态合法”类断言产生假失败。在顶层注入前 2 拍强制 `rst_n=0` 的 `assume`（仅 SAT 侧，UVM 用原文不受影响） |

**不可降级的形态**（[server.js `lowerConcurrentSVA`](file:///d:/code/SATinUVM260901/server.js) 内 `unlowerable` 判定）：整条注释跳过，宁可跳过也不给假结果——

- 含 `$isunknown`：BMC 上电初值自由且 x 建模为任意值，必假失败；其 2 态意图由“合法编码列表”类断言覆盖，UVM 侧仍用原文检查。
- 多拍序列 `##N`（`N≠1`）无法降级为 immediate 断言（直译必误报）。

生成的 `config.sby` 标准布局：

```ini
[options]
mode bmc
depth 20

[engines]
smtbmc z3

[script]
read -formal -sv <file1>.sv
prep -top <top> -flatten

[files]
<file1>.sv
```

每个运行结果落到 `work/sat_<时间戳>/`，含 `config/`（sby 标准布局：`engine_0/`、`model/`、`src/`）与 `PASS` / `FAIL` / `ERROR` 状态文件与 `status.sqlite`。

---

## 11. server.js 的 UVM 兼容降级链

与 SAT 侧的 `yosysCompat()` 对称，UVM 侧有 `uvmCompat()` 及配套函数，在 `/api/exec` 写文件前对冻结 SVA 做预处理，使其能被 ModelSim / VCS / Xcelium 等商用仿真器编译。SAT 侧的降级把 concurrent SVA 拆成 immediate 断言（因为 yosys 不支持 concurrent SVA），UVM 侧则**保留 concurrent SVA 原貌**，仅修补商用仿真器不接受的语法点。

| 步骤 | 函数 | 作用 |
| --- | --- | --- |
| 1 | `uvmCompat` | **核心**：① 给裸 `assert/cover property`（无 `@(...)`）自动补 `@(posedge clk)`——AI 生成的 SVA 常省略时钟事件，ModelSim 10.4 报 vlog-60；② 整条注释 `?:` 内含 `##N` 的断言（IEEE 1800 非法，ModelSim 正确拒绝）；③ 清除 `//else $error(...)` 行——ModelSim 10.4 把注释中的 `else` 误解析为 assert 的 else 分支，导致 vlog-60 |
| 2 | `stripAssertDup` | 跨文件去重：bound 版 DUT（= DUT 源码 + 断言模块 + bind）与 frozen SVA 含同名断言模块定义和重复 bind，vlog 报模块重复定义。以 frozen 为准，注释其余文件中的同名 module（大小写不敏感）和引用这些模块的 bind 语句 |
| 3 | `fixBindTarget` | bind 目标校正：AI 常按 Spec 模块名猜 DUT 顶层（如写 `iommu_sm`），但文件内实际模块名可能是 `dut`。检测到 bind 目标在 DUT 文件中不存在时，自动找到真实顶层（排除断言模块、排除被实例化过的模块）并改写 bind 目标 |
| 4 | `genTbTop` | 从 frozen SVA 的 `bind` 语句自动提取 DUT 名和端口列表，从断言模块端口声明提取信号类型，生成最小 `tb_top.sv`（含 clock 生成、复位序列、默认激励）和 `run.do`（`run -all; quit -f`） |
| 5 | `dutPortDirs` | 解析 DUT 模块 ANSI 端口方向（`input`/`output`/`inout`），让 `genTbTop` 对输出信号用 `wire` 声明（tb 不驱动，避免 ModelSim `vopt-3838` 混合驱动警告），仅对输入信号用 `logic` 驱动 |
| 6 | `compile.bat` | 自动生成编译脚本：逐文件 `vlog -sv <name>.sv`，绕过 cmd.exe `for %%f` 在 `/d /s /c` 模式下的 `%%f` → `%f` 转义问题 |
| 7 | 文件名清洗 | `handleExec` 入口把文件名统一为 `[\w.\-]` 安全格式（`dut_assert_bound (4).sv` → `dut_assert_bound__4_.sv`），与 `writeFiles` 的清洗规则一致，确保 `compile.bat` 引用的文件名与磁盘一致 |

**与 SAT 侧的关键区别**：

| 维度 | yosysCompat（SAT） | uvmCompat（UVM） |
| --- | --- | --- |
| 断言形式 | concurrent → immediate 等价降级 | 保留 concurrent SVA 原貌 |
| `@(posedge clk)` | 剥掉体内 `@(...)` 统一走 `always @(...)` | 给裸 assert **补上** `@(posedge clk)` |
| `bind` 语句 | 删掉原文，改成模块内直接实例化 | 保留 bind 原文（仿真器支持） |
| `inside` | 降级为 `==` + `\|\|` | 保留原文（仿真器支持） |
| `$isunknown` | 整条注释跳过 | 保留原文（仿真器支持） |
| `disable iff` | 转成 `!R &&` 前置守卫 | 保留原文（仿真器支持） |
| 上电复位假设 | 注入 POR `assume` | 不需要（仿真有真实复位序列） |

每个运行结果落到 `work/exec_<时间戳>/`，含经预处理的 `.sv` 源码、`compile.bat`、`tb_top.sv`、`run.do`、`modelsim.ini`。

---

## 12. SVA 静态检查清单（10 项）

阶段 4 「运行自动检查」由 [sva.js `checks`](file:///d:/code/SATinUVM260901/js/sva.js) 执行，每项返回 `pass/warn/fail`：

| ID | 标题 | 检查内容 |
| --- | --- | --- |
| C1 | 复位保护 disable iff | 每条 `assert property` 带 `disable iff`（含引用 `property` 声明时追溯声明体）；无 `assert property` 也 fail |
| C2 | 仿真专属系统任务 | 禁止 `$display/$write/$fopen/$fatal/$error/$finish/$stop/$monitor/$dumpvars/$random/...` 等 |
| C3 | bind 外部绑定 | 必须有 `bind dut mod inst (...)`，否则 fail |
| C4 | 断言模块纯净性 | 禁止 `assign/always/always_ff/always_comb/always_latch/initial` 等可综合逻辑 |
| C5 | 状态编码参数化 | 用 `localparam`（pass）/`parameter`（warn）/都没有（fail，疑似魔法数字） |
| C6 | bind 端口一致性 | bind 端口信号与阶段 1 信号清单一一核对；多余信号（疑似 AI 虚构）fail，缺信号 warn |
| C7 | 全局不变断言 | 覆盖三类：复位回 IDLE、状态 X/Z 未知态检查、非法/未定义状态禁止跳转；缺则 warn |
| C8 | Spec 状态覆盖 | FSM 跳转里的每个状态名都出现在 SVA 中；缺则 fail（可能脑补/漏写） |
| C9 | cover 点完备性 | 有 `cover property`；无则 warn |
| C10 | yosys 语法兼容性 | 未打包数组参数、`'{...}` 模式字面量、`?:` 表达式内的 `##`（IEEE 1800 非法）；命中则 fail（真实跑 SymbiYosys 必报错） |

检查结果中 `fail`/`warn` 项可一键写入 Prompt 末尾回流阶段 2。

---

## 13. 数据持久化与项目导入导出

- **数据模型**：[store.js `blank()`](file:///d:/code/SATinUVM260901/js/store.js) 定义单个项目的完整字段（阶段 1–7 全部制品 + `log` + `aiFbs` + `iterations` + `boundCode/boundTime` 等）。`localStorage` 单 key `satinuvm_data_v1` 全量存 `{projects, curId, settings}`。
- **多项目**：顶栏下拉切换 / 新建 / 重命名 / 删除。切换项目会重置到阶段 1 并清空当前会话报告。
- **导入导出**：导出为 `<模块名>.satinuvm.json`（单项目全量），顶栏「导入」可载回；导入时重生成 `id` 避免冲突。演示用 [test/demo_project.satinuvm.json](file:///d:/code/SATinUVM260901/test/demo_project.satinuvm.json)。
- **设置同步**：`Store.save()` 每次 localStorage 写入后顺带 POST `/api/settings` 同步到 `work/settings.json`；`Store.load()` 启动时从 `/api/settings` 拉回（脱离本地服务时静默降级）。
- **旧版迁移**：[store.js `load`](file:///d:/code/SATinUVM260901/js/store.js) 内置旧版单接口配置迁移为档案列表、旧项目补 `sat.dutSrcs/sat.log/uvm.log/boundCode/aiFbs` 等字段。
- **操作日志**：`Store.addLog(p, event, detail)` 记最多 100 条，显示在阶段 5「操作日志」卡片。

---

## 14. 演示物料与样本

`test/` 目录提供完整可复现样本：

| 文件 | 用途 |
| --- | --- |
| [iommu_sm.sv](file:///d:/code/SATinUVM260901/test/iommu_sm.sv) | 演示 DUT，IOMMU 翻译控制状态机，模块名固定 `dut`，8 状态 FSM，内置一处已知 Spec 冲突 |
| [xxx_spec.md](file:///d:/code/SATinUVM260901/test/xxx_spec.md) | 演示功能 Spec（状态列表、跳转规则、握手时序、异常/边界、全局不变） |
| [signal_list.txt](file:///d:/code/SATinUVM260901/test/signal_list.txt) | 演示信号清单 |
| [fsm_transitions.txt](file:///d:/code/SATinUVM260901/test/fsm_transitions.txt) | 演示 FSM 跳转规则（`fsm_transitions_bad.txt` 为错误样本） |
| [sva_gen_prompt.txt](file:///d:/code/SATinUVM260901/test/sva_gen_prompt.txt) | 演示 5 段式 Prompt |
| [dut_formal.sv](file:///d:/code/SATinUVM260901/test/dut_formal.sv) | 演示断言文件（`.frozen.sv` 为冻结版，`_bad.sv` 含问题，`_deepseek.sv` 为 DeepSeek 生成样本） |
| [dut_assert_bound.sv](file:///d:/code/SATinUVM260901/test/dut_assert_bound.sv) | DUT+断言绑定样本（`(1)~(4).sv` 为迭代历史） |
| [sat_result.rpt](file:///d:/code/SATinUVM260901/test/sat_result.rpt) | SAT 形式证明结果样本（导入用） |
| [uvm_sim.rpt](file:///d:/code/SATinUVM260901/test/uvm_sim.rpt) | UVM 仿真结果样本（导入用） |
| [ai_feedback.txt](file:///d:/code/SATinUVM260901/test/ai_feedback.txt) | AI 反馈清单样本 |
| [demo_project.satinuvm.json](file:///d:/code/SATinUVM260901/test/demo_project.satinuvm.json) | 可导入的完整演示项目 |
| [OASIS-AI_2026_paper_2.pdf](file:///d:/code/SATinUVM260901/test/OASIS-AI_2026_paper_2.pdf) | 相关论文参考 |

---

## 15. 本地验证服务 API

[server.js](file:///d:/code/SATinUVM260901/server.js) 暴露的 HTTP 接口（全部 CORS 放开，JSON 交互，请求体上限 80MB）：

| 方法 | 路径 | 作用 |
| --- | --- | --- |
| GET | `/api/tools` | 检测本机工具可用性：`{platform, sby, yosys, z3, iverilog, verilator, wslSby}` |
| POST | `/api/sat` | SAT 形式证明。入参 `{files:[{name,content}], top, mode?, depth?}`；内部 `yosysCompat` 降级 → 生成 `config.sby` → 跑 sby；返回 `{status, code, dir, log}`，`status` 从日志 `DONE (PASS/FAIL,...)` 正则提取 |
| POST | `/api/exec` | 通用命令执行（UVM 用）。入参 `{cmd, files?, top?}`，`{work}` 替换为工作目录；`top` 为前端确认过的顶层模块名（供 `fixBindTarget` 校正 bind 目标用）；返回 `{code, dir, log}` |
| GET | `/api/settings` | 读 `work/settings.json` |
| POST | `/api/settings` | 写 `work/settings.json`（body 为 settings 对象原文） |
| GET | `/` 或其他 | 静态文件托管（路径越界拦截，`.html/.js/.css/.json/.md/.txt/.svg/.ico` 带 MIME，无缓存） |

运行命令统一走 `runCmd(cmd, args, cwd, timeoutMs)`：`spawn` 起进程，stdout/stderr 合并收集（超 400KB 截断留后 200KB），超时强杀并标注「超时 N 分钟」。

---

## 16. 常见问题

**Q: 端口 8898 已被占用？**
A: 多为上次 server.js 实例没关。控制台会提示。直接访问旧实例即可，或 `Get-NetTCPConnection -LocalPort 8898` 查 PID 后 `Stop-Process -Id <pid>` 再启动。

**Q: AI 调用失败 / 连不通？**
A: 商用 API 多有浏览器跨域限制（表现为网络请求失败）；本地模型需确认服务已启动且允许跨域。先用「🔌 测试连通性」发极小请求验证。Claude 协议需带 `anthropic-dangerous-direct-browser-access: true` 直连浏览器。实在不行用「手动粘贴 SVA」。

**Q: SAT 真实运行报 yosys 编译错误？**
A: server.js 的降级链已处理大部分常见不兼容语法，但仍有降级不了的形态（`$isunknown`、`##N≠1`）会被整条注释跳过。看 `work/sat_<时间戳>/config/logfile.txt` 定位；阶段 6 会自动把编译错误记入 AI 反馈，弹窗询问导出 txt 回流 Prompt 让 AI 修复。

**Q: SAT 报“未检测到 SymbiYosys(sby)”？**
A: 三选一：① 确认 `oss-cad-suite-windows-x64-20260828/oss-cad-suite/bin/sby.exe` 存在（仓库自带）；② 把 OSS CAD Suite 的 `bin` 加入系统 PATH；③ WSL 内装 sby。

**Q: bind 目标模块在 DUT 文件里找不到？**
A: AI 常按 Spec 模块名写 bind（如写成 `iommu_sm`），与文件内实际模块名（如 `dut`）不一致。阶段 5「将 DUT 与断言绑定」与阶段 6「真实运行」都会自动回落到文件首个真实模块，并 toast 提示；server.js 的 `lowerBind` 也会在目标缺失时回退顶层。

**Q: 冻结后改了 SVA 怎么办？**
A: 阶段 5 会显示「已偏离冻结版本」警告。要么「恢复为冻结版本」，要么「解除冻结（重新迭代）」→ 回阶段 4 重新评审 → 重新冻结。

**Q: localStorage 存不下？**
A: 全量存一个 key，大 DUT 文件可能撑爆。载入 DUT 时单文件上限 6MB（[app.js `loadDutFiles`](file:///d:/code/SATinUVM260901/js/app.js) 检查），超了会 toast 阻止。必要时用「导出」存成 json 文件，或直接用 `dut_assert_bound.sv` 单文件编译，不依赖 localStorage。

**Q: UVM 真实运行报 `(vlog-60) SystemVerilog concurrent assertions not supported in action block`？**
A: 这是 ModelSim 10.4 把注释里的 `//else $error(...)` 当成 assert 的 else 分支所致。`uvmCompat()` 已自动清除这类注释行。如果仍出现此错误，确认已刷新页面（Ctrl+F5 加载最新前端），且 server.js 已重启（载入了最新 `uvmCompat` 代码）。

**Q: UVM 真实运行报 `Module 'xxx' is not defined`？**
A: AI 在生成 SVA 时按 Spec 名猜了 DUT 模块名（如 `iommu_sm`），但实际文件里顶层模块叫 `dut`。`fixBindTarget()` 会自动检测并校正 bind 目标。如果仍出现此错误，先在 SAT 通路（阶段 6 通路 A）点「真实运行 SymbiYosys」确认顶层模块名，该名字会记住并传给 UVM 通路。

**Q: UVM 真实运行报 `Failed to open design unit file "... .sv" in read mode`？**
A: 文件名含空格或括号（如 `dut_assert_bound (4).sv`），`writeFiles` 清洗后磁盘上是 `dut_assert_bound__4_.sv`，但 `compile.bat` 引用了原始名。已修复：`handleExec` 入口统一清洗文件名，确保 `compile.bat` 与磁盘一致。

**Q: ModelSim 安装路径不是 `C:\modeltech64_10.4\`？**
A: 在设置里修改 UVM 命令模板，把 `C:\modeltech64_10.4\` 全部替换为你的实际安装路径即可。

---

## 17. 技术栈与依赖

- **前端**：原生 HTML/CSS/JS，无框架、无构建、无打包。仅依赖浏览器 `fetch` / `crypto.subtle` / `localStorage` / `URL.createObjectURL` 等标准 API。
- **服务端**：Node.js（建议 ≥ 16），**零 npm 依赖**，仅用内置 `http` / `fs` / `path` / `child_process`。
- **SAT 工具**：OSS CAD Suite（Windows x64，20260828 版），含 sby/yosys/z3/iverilog/verilator/gtkwave 等，仓库内置。
- **UVM 工具**：ModelSim SE-64 10.4（已验证适配），也支持 QuestaSim / VCS / Xcelium / WSL 内开源流程，命令模板可配。
- **AI 模型**：OpenAI 兼容协议（DeepSeek/Qwen/GLM/Kimi/OpenAI/ERNIE/Doubao/Ollama/LM Studio/vLLM）或 Anthropic Claude 协议，任选其一。
- **数据格式**：SVA 为 SystemVerilog 断言（IEEE 1800 子集，SAT 侧经 yosysCompat 降级、UVM 侧经 uvmCompat 预处理）；报告为 Markdown；项目存档为 JSON。
- **目标平台**：Windows（OSS CAD Suite 与 ModelSim 均为 Windows 版；Linux/Mac 需自行装 sby 或用 WSL）。