# Formality自动化验证进阶：用Python封装TCL命令流实现批量LEC检查 在芯片设计流程中，每一次RTL代码的修改、综合优化、物理实现后的ECO，都意味着一次逻辑等价性检查（LEC）的必然性。对于中高级验证工程师而言，手动执行Formality检查，重复加载设计、设置约束、匹配比较点、验证结果，不仅耗时费力，更在频繁迭代中成为效率瓶颈。当项目需要同时验证多个版本网表、或对同一设计在不同工艺角下进行一致性检查时，这种重复劳动带来的疲惫感尤为明显。 我们真正需要的，不是对单个流程的熟练操作，而是一套能够将Formality的TCL命令流**工程化、自动化、批量化**的解决方案。这篇文章将分享如何利用Python脚本，深度封装Formality的TCL交互，构建一个从SVF文件智能生成、多版本网表自动对比、到结果解析与报告自动化的完整工具链。这套方法的核心，是将工程师从重复性操作中解放出来，将精力聚焦于真正的调试与分析。 ## 1. 理解Formality的TCL命令流与自动化切入点 Formality的操作本质是一系列TCL命令的顺序执行。一个典型的手动验证流程，可以抽象为以下几个核心阶段： 1. **环境与模式初始化**：启动`fm_shell`，进入`setup`模式。 2. **指导文件加载**：通过`set_svf`命令加载由综合工具（如Design Compiler）生成的SVF文件，工具自动进入`guide`模式处理指导信息后返回`setup`模式。 3. **参考设计与实现设计加载**：使用`read_verilog`、`read_db`等命令分别加载参考设计（Reference， 通常是RTL或已知正确的网表）和实现设计（Implementation， 待验证的网表），并用`set_top`指定顶层模块。 4. **设计特定设置**：在`setup`模式下，处理时钟门控、扫描链、黑盒、常量设置等（例如`set_constant`）。 5. **比较点匹配**：执行`match`命令，进入`match`模式，工具尝试自动映射两个设计中的关键点（如寄存器、输出端口）。 6. **等价性验证**：执行`verify`命令，进入`verify`模式，进行形式化证明。 7. **结果报告与调试**：根据`verify`的结果（PASS/FAIL/INCONCLUSIVE），使用`report_unmatched_points`、`analyze_points`等命令进行问题定位。 要实现自动化，我们需要用程序模拟这一交互过程。但直接通过Python调用`fm_shell`并发送TCL命令面临几个挑战：**会话管理**（保持shell进程）、**输出解析**（从混杂的日志中提取关键信息）、**错误处理**（识别并响应TCL错误）以及**状态跟踪**（判断当前处于哪个模式）。 一个更稳健的策略是：**让Python生成完整的TCL脚本文件，然后调用Formality以批处理模式执行该脚本，最后解析其输出的日志文件**。这样，Python扮演了“脚本生成器”和“结果分析器”的角色，而Formality则作为纯粹的计算引擎。 > 提示：Formality的批处理模式通过`fm_shell -f <script.tcl>`调用，它会执行脚本中的所有命令然后退出，非常适合自动化集成。 ## 2. 构建核心Python类：封装Formality会话 我们将创建一个`FormalitySession`类，它负责管理一次完整的Formality验证会话所需的所有数据和操作。这个类是自动化框架的基石。 ```python import subprocess import re import os import json from pathlib import Path from dataclasses import dataclass, asdict from typing import List, Optional, Dict, Any @dataclass class FormalityConfig: """Formality会话配置数据类""" fm_shell_path: str = "fm_shell" # Formality可执行文件路径 work_dir: Path = Path(".") # 工作目录 svf_file: Optional[Path] = None # SVF指导文件路径 reference_files: List[Path] = [] # 参考设计文件列表 implementation_files: List[Path] = [] # 实现设计文件列表 lib_files: List[Path] = [] # 工艺库文件列表 (.db) top_module: str = "top" # 顶层模块名 auto_setup: bool = True # 是否启用自动设置模式 verification_timeout: str = "4:00:00" # 验证超时设置 (时:分:秒) custom_setup_commands: List[str] = None # 用户自定义的setup命令 class FormalitySession: """封装一次Formality验证会话""" def __init__(self, config: FormalityConfig): self.config = config self.work_dir = Path(config.work_dir) self.work_dir.mkdir(parents=True, exist_ok=True) self.tcl_script_path = self.work_dir / "run_fm.tcl" self.log_file_path = self.work_dir / "fm_run.log" self.result = { "status": "NOT_RUN", # NOT_RUN, RUNNING, PASS, FAIL, INCONCLUSIVE, ERROR "summary": "", "unmatched_points": 0, "failing_points": 0, "aborted_points": 0, "matched_points": 0, "error_messages": [] } def generate_tcl_script(self): """根据配置生成完整的TCL脚本""" tcl_lines = [] # 1. 设置基本变量与模式 tcl_lines.append("# ===== Auto-generated Formality TCL Script =====") tcl_lines.append("# Generated by Python Automation Framework") tcl_lines.append("") if self.config.auto_setup: tcl_lines.append("# Enable automated setup mode") tcl_lines.append("set synopsys_auto_setup true") tcl_lines.append("") # 2. 加载SVF指导文件 (如果提供) if self.config.svf_file and self.config.svf_file.exists(): tcl_lines.append(f"# Loading SVF guidance file") tcl_lines.append(f"set_svf {self.config.svf_file.resolve()}") tcl_lines.append("") else: tcl_lines.append("# No SVF file provided, proceeding without guidance") tcl_lines.append("") # 3. 加载参考设计 (Reference) tcl_lines.append("# --- Loading Reference Design ---") # 先加载库文件 for lib in self.config.lib_files: if lib.suffix == '.db': tcl_lines.append(f"read_db -r {lib.resolve()}") # 加载参考设计文件 for ref_file in self.config.reference_files: if ref_file.suffix in ['.v', '.sv']: tcl_lines.append(f"read_verilog -r {ref_file.resolve()}") elif ref_file.suffix == '.ddc': tcl_lines.append(f"read_ddc -r {ref_file.resolve()}") # 设置参考设计顶层 tcl_lines.append(f"set_top r:/WORK/{self.config.top_module}") tcl_lines.append("") # 4. 加载实现设计 (Implementation) tcl_lines.append("# --- Loading Implementation Design ---") # 加载库文件 (如果需要为实现设计单独指定) for lib in self.config.lib_files: if lib.suffix == '.db': tcl_lines.append(f"read_db -i {lib.resolve()}") # 加载实现设计文件 for impl_file in self.config.implementation_files: if impl_file.suffix in ['.v', '.sv', '.vg']: tcl_lines.append(f"read_verilog -i {impl_file.resolve()}") elif impl_file.suffix == '.ddc': tcl_lines.append(f"read_ddc -i {impl_file.resolve()}") # 设置实现设计顶层 (通常使用-auto自动推断) tcl_lines.append(f"set_top i:/WORK/{self.config.top_module} -auto") tcl_lines.append("") # 5. 执行用户自定义设置命令 tcl_lines.append("# --- Custom Setup Commands ---") if self.config.custom_setup_commands: for cmd in self.config.custom_setup_commands: tcl_lines.append(cmd) else: tcl_lines.append("# No custom setup commands provided") tcl_lines.append("") # 6. 设置验证参数并执行验证 tcl_lines.append("# --- Setting Verification Parameters ---") tcl_lines.append(f"set verification_timeout_limit {self.config.verification_timeout}") tcl_lines.append("set verification_failing_point_limit 50") tcl_lines.append("") tcl_lines.append("# --- Running Match & Verify ---") tcl_lines.append("match") tcl_lines.append("verify") tcl_lines.append("") # 7. 报告生成命令 tcl_lines.append("# --- Generating Reports ---") tcl_lines.append("report_verification -summary") tcl_lines.append("report_unmatched_points > unmatched_points.rpt") tcl_lines.append("report_failing_points > failing_points.rpt") tcl_lines.append("report_aborted_points > aborted_points.rpt") tcl_lines.append("quit") # 将TCL脚本写入文件 with open(self.tcl_script_path, 'w') as f: f.write('\n'.join(tcl_lines)) print(f"[INFO] TCL script generated: {self.tcl_script_path}") ``` 这个类首先定义了配置数据结构`FormalityConfig`，然后`FormalitySession`类利用这些配置生成一个可执行的TCL脚本。脚本结构清晰，包含了从设置、读入设计到验证、报告的全流程。注意我们使用了`-auto`参数让Formality自动推断实现设计的顶层，这在处理综合后网表时非常实用。 ## 3. 执行引擎与结果解析：从日志中提取关键信息 生成脚本只是第一步，我们还需要执行它并智能地解析输出结果。在`FormalitySession`类中继续添加执行和解析方法。 ```python def run(self): """执行Formality验证并捕获输出""" self.result["status"] = "RUNNING" # 构建命令行 cmd = [ self.config.fm_shell_path, "-f", str(self.tcl_script_path), "-output_log_file", str(self.log_file_path) ] print(f"[INFO] Starting Formality session...") print(f"[INFO] Command: {' '.join(cmd)}") try: # 执行Formality，捕获实时输出（可选） process = subprocess.Popen( cmd, stdout=subprocess.PIPE, stderr=subprocess.PIPE, text=True, cwd=self.work_dir ) stdout, stderr = process.communicate(timeout=3600) # 设置1小时超时 # 将标准输出也写入日志，便于调试 with open(self.log_file_path, 'a') as f: f.write("\n=== STDOUT ===\n") f.write(stdout) if stderr: f.write("\n=== STDERR ===\n") f.write(stderr) return_code = process.returncode self._parse_log_file() if return_code != 0: self.result["status"] = "ERROR" self.result["summary"] = f"Formality process exited with code {return_code}" print(f"[ERROR] Formality execution failed with return code {return_code}") else: print(f"[INFO] Formality execution completed. Status: {self.result['status']}") except subprocess.TimeoutExpired: self.result["status"] = "ERROR" self.result["summary"] = "Formality execution timed out after 1 hour" print("[ERROR] Formality execution timed out") except Exception as e: self.result["status"] = "ERROR" self.result["summary"] = f"Unexpected error: {str(e)}" print(f"[ERROR] Unexpected error during execution: {e}") return self.result def _parse_log_file(self): """解析Formality日志文件，提取验证结果""" if not self.log_file_path.exists(): self.result["status"] = "ERROR" self.result["summary"] = "Log file not found" return with open(self.log_file_path, 'r', encoding='utf-8', errors='ignore') as f: log_content = f.read() # 关键模式匹配：查找验证结果摘要 summary_pattern = r"Verification Results Summary\s*\n-+\s*\n.*?\n-+\s*\n(.*?)\n\n" match = re.search(summary_pattern, log_content, re.DOTALL) if match: summary_text = match.group(1) self.result["summary"] = summary_text.strip() # 解析具体数值 # 匹配 "Matched Points: 12345" 这样的行 matched_points_pattern = r"Matched Points:\s*(\d+)" unmatched_points_pattern = r"Unmatched Points:\s*(\d+)" failing_points_pattern = r"Failing Points:\s*(\d+)" aborted_points_pattern = r"Aborted Points:\s*(\d+)" for pattern, key in [ (matched_points_pattern, "matched_points"), (unmatched_points_pattern, "unmatched_points"), (failing_points_pattern, "failing_points"), (aborted_points_pattern, "aborted_points") ]: m = re.search(pattern, summary_text) if m: self.result[key] = int(m.group(1)) # 判断整体状态 if "Verification PASSED" in log_content: self.result["status"] = "PASS" elif "Verification FAILED" in log_content: self.result["status"] = "FAIL" elif "Verification INCONCLUSIVE" in log_content: self.result["status"] = "INCONCLUSIVE" else: # 如果没有明确状态，根据点数推断 if self.result.get("unmatched_points", 0) > 0 or self.result.get("failing_points", 0) > 0: self.result["status"] = "FAIL" elif self.result.get("aborted_points", 0) > 0: self.result["status"] = "INCONCLUSIVE" else: self.result["status"] = "UNKNOWN" # 提取错误和警告信息 error_pattern = r"Error:\s*(.*?)\n" warning_pattern = r"Warning:\s*(.*?)\n" errors = re.findall(error_pattern, log_content) warnings = re.findall(warning_pattern, log_content) if errors: self.result["error_messages"].extend([f"Error: {e}" for e in errors]) if warnings: self.result["error_messages"].extend([f"Warning: {w}" for w in warnings]) # 如果没有找到摘要，尝试其他模式 if self.result["status"] == "RUNNING": if "matched successfully" in log_content.lower() and "verification completed" in log_content.lower(): self.result["status"] = "PASS" self.result["summary"] = "Verification appears to have passed (parsed from alternative patterns)" ``` 解析器使用正则表达式从日志中提取关键信息。Formality的输出格式相对固定，这使得模式匹配成为可能。我们特别关注`Verification Results Summary`部分，它能提供匹配点、失败点、中止点等详细计数。 ## 4. 批量验证管理器：处理多版本网表对比 单个验证的自动化只是基础，真正的价值在于批量处理。假设我们有一个参考设计（RTL），和五个不同优化版本的综合后网表需要验证，手动操作需要重复五次。而通过Python，我们可以轻松构建一个批量验证管理器。 ```python class BatchLECManager: """管理多个Formality验证任务的批量执行""" def __init__(self, base_config: FormalityConfig): self.base_config = base_config self.tasks = [] # 存储各个验证任务 self.results = {} def add_implementation_variant(self, variant_name: str, impl_files: List[Path], custom_setup: List[str] = None): """添加一个实现设计变体进行验证""" config = FormalityConfig( fm_shell_path=self.base_config.fm_shell_path, work_dir=self.base_config.work_dir / variant_name, svf_file=self.base_config.svf_file, reference_files=self.base_config.reference_files.copy(), implementation_files=impl_files, lib_files=self.base_config.lib_files.copy(), top_module=self.base_config.top_module, auto_setup=self.base_config.auto_setup, verification_timeout=self.base_config.verification_timeout, custom_setup_commands=custom_setup if custom_setup else self.base_config.custom_setup_commands ) task = { "name": variant_name, "config": config, "session": None, "result": None } self.tasks.append(task) print(f"[INFO] Added verification task for variant: {variant_name}") def run_all(self, max_workers: int = 2): """并行执行所有验证任务""" from concurrent.futures import ThreadPoolExecutor, as_completed import threading print(f"[INFO] Starting batch LEC with {len(self.tasks)} tasks, max_workers={max_workers}") def run_task(task): """单个任务的执行函数""" print(f"[TASK] Starting: {task['name']}") session = FormalitySession(task['config']) task['session'] = session result = session.run() task['result'] = result print(f"[TASK] Completed: {task['name']} - Status: {result['status']}") return task['name'], result # 使用线程池并行执行（注意：Formality本身可能受license限制，实际并行数需调整） with ThreadPoolExecutor(max_workers=max_workers) as executor: future_to_name = { executor.submit(run_task, task): task['name'] for task in self.tasks } for future in as_completed(future_to_name): name = future_to_name[future] try: task_name, result = future.result() self.results[task_name] = result except Exception as e: print(f"[ERROR] Task {name} failed with exception: {e}") self.results[name] = { "status": "ERROR", "summary": f"Execution exception: {str(e)}" } return self.results def generate_summary_report(self, output_file: Path = None): """生成批量验证的汇总报告""" if not output_file: output_file = self.base_config.work_dir / "batch_lec_summary.md" report_lines = [ "# Batch LEC Verification Summary", f"Generated: {datetime.now().strftime('%Y-%m-%d %H:%M:%S')}", f"Total Tasks: {len(self.tasks)}", "", "## Summary Table", "", "| Variant Name | Status | Matched Points | Unmatched Points | Failing Points | Aborted Points | Notes |", "|--------------|--------|----------------|------------------|----------------|----------------|-------|" ] pass_count = 0 fail_count = 0 inconclusive_count = 0 error_count = 0 for task in self.tasks: result = task['result'] if not result: status = "NOT_RUN" notes = "Task was not executed" else: status = result.get('status', 'UNKNOWN') notes = result.get('summary', '')[:100] # 截取前100字符 # 统计 if status == "PASS": pass_count += 1 elif status == "FAIL": fail_count += 1 elif status == "INCONCLUSIVE": inconclusive_count += 1 elif status == "ERROR": error_count += 1 # 提取点数 matched = result.get('matched_points', 'N/A') if result else 'N/A' unmatched = result.get('unmatched_points', 'N/A') if result else 'N/A' failing = result.get('failing_points', 'N/A') if result else 'N/A' aborted = result.get('aborted_points', 'N/A') if result else 'N/A' report_lines.append( f"| {task['name']} | **{status}** | {matched} | {unmatched} | {failing} | {aborted} | {notes} |" ) report_lines.extend([ "", "## Statistics", "", f"- **PASS**: {pass_count}", f"- **FAIL**: {fail_count}", f"- **INCONCLUSIVE**: {inconclusive_count}", f"- **ERROR**: {error_count}", f"- **NOT RUN**: {len(self.tasks) - (pass_count + fail_count + inconclusive_count + error_count)}", "", "## Detailed Results", "" ]) # 添加每个任务的详细结果链接 for task in self.tasks: if task['session']: log_path = task['session'].log_file_path.relative_to(self.base_config.work_dir) report_lines.append(f"- [{task['name']}]({log_path})") with open(output_file, 'w') as f: f.write('\n'.join(report_lines)) print(f"[INFO] Summary report generated: {output_file}") return output_file ``` 这个批量管理器支持并行执行多个验证任务，并生成格式清晰的Markdown汇总报告。在实际项目中，你可能需要处理数十个不同优化策略、不同工艺角下的网表，这个框架可以轻松扩展。 ## 5. 高级功能：SVF文件智能处理与ECO场景适配 SVF（Setup and Verification Format）文件是Formality自动化验证的关键。它记录了综合工具对设计所做的所有转换（如寄存器合并、状态机重编码、重定时等）。但在实际工程中，我们常遇到以下问题： 1. **SVF文件缺失或不完整**：特别是使用第三方综合工具时。 2. **ECO（工程变更）场景**：只有部分网表被修改，需要增量验证。 3. **多版本SVF合并**：当设计经过多次综合迭代时。 我们可以扩展Python框架来处理这些复杂场景。首先，创建一个SVF处理器： ```python class SVFProcessor: """处理SVF文件的辅助类""" @staticmethod def extract_guidance_summary(svf_path: Path) -> Dict[str, Any]: """从SVF文件中提取指导信息摘要""" if not svf_path.exists(): return {"error": "SVF file not found"} summary = { "total_commands": 0, "guide_commands": {}, "retiming_operations": 0, "register_merges": 0, "black_box_declarations": 0, "constant_registers": 0 } try: with open(svf_path, 'r', encoding='utf-8', errors='ignore') as f: content = f.read() # 统计各类guide命令（简化示例，实际SVF是二进制格式，需要特殊解析） # 注意：实际SVF是二进制，这里假设有文本版本或使用Synopsys工具转换 guide_patterns = { "guide_retiming": r"guide_retiming", "guide_reg_merge": r"guide_reg_merge|guide_reg_merging", "guide_black_box": r"guide_black_box|set_black_box", "guide_constant": r"guide_reg_constant|set_constant.*register", "guide_change_names": r"guide_change_names" } for key, pattern in guide_patterns.items(): matches = re.findall(pattern, content, re.IGNORECASE) summary["guide_commands"][key] = len(matches) summary["total_commands"] += len(matches) # 特别统计 summary["retiming_operations"] = summary["guide_commands"].get("guide_retiming", 0) summary["register_merges"] = summary["guide_commands"].get("guide_reg_merge", 0) return summary except Exception as e: return {"error": f"Failed to parse SVF: {str(e)}"} @staticmethod def generate_minimal_svf_for_eco(reference_design: str, changed_modules: List[str]) -> List[str]: """为ECO场景生成最小化的SVF指导命令""" # 在实际项目中，这需要根据ECO变更的具体内容生成 # 这里提供一个框架示例 svf_commands = [ "# Minimal SVF for ECO verification", "guide", "# Assume only these modules have changes" ] for module in changed_modules: svf_commands.extend([ f"# Guidance for module: {module}", f"guide_change_names -module {module}", "# Add specific guidance based on ECO report" ]) svf_commands.append("setup") return svf_commands @staticmethod def check_svf_compatibility(svf_path: Path, design_version: str) -> bool: """检查SVF文件与设计版本的兼容性""" # 在实际应用中，这可能涉及检查时间戳、版本号或哈希值 # 这里返回一个简单的实现 if not svf_path.exists(): return False svf_mtime = svf_path.stat().st_mtime # 假设设计版本信息存储在某个文件中 design_version_file = svf_path.parent / f"{design_version}.info" if design_version_file.exists(): design_mtime = design_version_file.stat().st_mtime # 如果SVF比设计文件旧，可能不兼容 if svf_mtime < design_mtime - 3600: # 1小时容差 print(f"[WARNING] SVF file ({svf_path}) appears older than design version") return False return True ``` 对于ECO场景，我们还可以创建一个专门的验证类： ```python class ECOVerification: """处理工程变更(ECO)的特殊验证场景""" def __init__(self, base_session: FormalitySession): self.base_session = base_session self.eco_patches = [] # 存储ECO补丁信息 def apply_eco_patch(self, patch_file: Path, patch_type: str = "verilog"): """应用ECO补丁到实现设计""" # 在实际实现中，这可能涉及： # 1. 解析ECO补丁文件（可能是Verilog diff、TCL命令等） # 2. 修改实现设计网表 # 3. 生成临时网表文件供Formality验证 eco_temp_dir = self.base_session.work_dir / "eco_patches" eco_temp_dir.mkdir(exist_ok=True) if patch_type == "verilog": # 假设补丁是完整的Verilog模块 # 在实际项目中，需要更精细的网表修补 patched_netlist = eco_temp_dir / "patched_implementation.v" # 这里简化处理：直接使用补丁文件作为新网表 # 实际应合并到原网表中 import shutil shutil.copy2(patch_file, patched_netlist) # 更新session的配置，使用修补后的网表 self.base_session.config.implementation_files = [patched_netlist] self.eco_patches.append({ "patch_file": patch_file, "type": patch_type, "applied": True, "temp_netlist": patched_netlist }) print(f"[ECO] Applied patch from {patch_file}") return True return False def verify_eco_only(self, changed_modules: List[str]): """执行仅针对ECO变更的增量验证""" # 增量验证策略： # 1. 设置只验证特定模块 # 2. 使用set_dont_verify命令排除未变更模块 # 3. 减少验证范围，加快速度 original_setup = self.base_session.config.custom_setup_commands or [] # 添加增量验证设置 incremental_setup = original_setup.copy() # 设置只验证特定模块（示例） for module in changed_modules: incremental_setup.append(f"# Focusing on changed module: {module}") # 实际命令可能更复杂，取决于具体需求 # 还可以设置验证努力级别为较低，以快速获得结果 incremental_setup.append("set verification_effort_level medium") # 临时修改配置 self.base_session.config.custom_setup_commands = incremental_setup print(f"[ECO] Running incremental verification for modules: {changed_modules}") result = self.base_session.run() # 恢复原始设置 self.base_session.config.custom_setup_commands = original_setup return result ``` ## 6. 实战案例：多工艺角网表批量验证 让我们看一个完整的实战示例。假设我们有一个设计`my_design`，已经综合出五个不同工艺角（PVT条件）下的网表，我们需要批量验证它们与原始RTL的逻辑等价性。 ```python from datetime import datetime import sys def main(): """主函数：演示批量多工艺角LEC验证""" # 1. 基础配置 base_config = FormalityConfig( fm_shell_path="/tools/synopsys/formality/bin/fm_shell", work_dir=Path("./lec_results"), svf_file=Path("./syn_output/my_design.svf"), reference_files=[ Path("./rtl/my_design.v"), Path("./rtl/submodule1.v"), Path("./rtl/submodule2.v") ], lib_files=[ Path("./libs/tech_lib.db"), Path("./libs/ram_compiler.db") ], top_module="my_design", auto_setup=True, verification_timeout="2:00:00", # 2小时超时 custom_setup_commands=[ "# 禁用扫描链以进行功能验证", "set_constant -type port i:/WORK/my_design/test_mode 0", "set_constant -type port i:/WORK/my_design/scan_enable 0" ] ) # 2. 创建批量管理器 batch_manager = BatchLECManager(base_config) # 3. 定义不同工艺角的网表 pvt_corners = [ ("ss_0p9v_125c", [Path("./netlist/my_design_ss_0p9v_125c.vg")]), ("tt_1p0v_25c", [Path("./netlist/my_design_tt_1p0v_25c.vg")]), ("ff_1p1v_0c", [Path("./netlist/my_design_ff_1p1v_0c.vg")]), ("wc_0p8v_150c", [Path("./netlist/my_design_wc_0p8v_150c.vg")]), ("bc_1p2v_-40c", [Path("./netlist/my_design_bc_1p2v_-40c.vg")]) ] # 4. 为每个工艺角添加验证任务 for corner_name, netlist_files in pvt_corners: # 为某些特殊工艺角添加特定的设置命令 custom_setup = base_config.custom_setup_commands.copy() if "ss" in corner_name or "wc" in corner_name: # 慢速工艺角可能需要调整验证参数 custom_setup.append("# 慢速工艺角特殊设置") custom_setup.append("set verification_timeout_limit 3:00:00") # 延长超时 batch_manager.add_implementation_variant( variant_name=f"my_design_{corner_name}", impl_files=netlist_files, custom_setup=custom_setup ) # 5. 执行批量验证（最多同时运行2个） print(f"\n{'='*60}") print(f"Starting batch LEC for {len(pvt_corners)} PVT corners") print(f"Start time: {datetime.now().strftime('%Y-%m-%d %H:%M:%S')}") print(f"{'='*60}\n") results = batch_manager.run_all(max_workers=2) # 6. 生成报告 summary_report = batch_manager.generate_summary_report() # 7. 分析结果 print(f"\n{'='*60}") print("BATCH VERIFICATION COMPLETE") print(f"{'='*60}") # 读取并显示汇总报告 with open(summary_report, 'r') as f: print(f.read()) # 8. 如果有失败，提供调试建议 failing_tasks = [t for t in batch_manager.tasks if t['result'] and t['result']['status'] == 'FAIL'] if failing_tasks: print(f"\n{'!'*60}") print(f"WARNING: {len(failing_tasks)} tasks FAILED") print(f"{'!'*60}") for task in failing_tasks: print(f"\nFailed task: {task['name']}") print(f"Summary: {task['result']['summary']}") # 建议的调试步骤 print("Suggested debug steps:") print("1. Check unmatched points report:") print(f" {task['session'].work_dir}/unmatched_points.rpt") print("2. Check failing points report:") print(f" {task['session'].work_dir}/failing_points.rpt") print("3. Review Formality log for warnings/errors:") print(f" {task['session'].log_file_path}") print("4. Consider enabling more detailed logging:") print(" Add 'set verification_report_detail high' to setup") # 9. 保存详细结果到JSON文件（便于后续分析） results_json = { "timestamp": datetime.now().isoformat(), "total_tasks": len(batch_manager.tasks), "results": { task['name']: task['result'] for task in batch_manager.tasks } } json_path = base_config.work_dir / "detailed_results.json" with open(json_path, 'w') as f: json.dump(results_json, f, indent=2) print(f"\nDetailed results saved to: {json_path}") print(f"All task logs and reports are in: {base_config.work_dir}") return 0 if not failing_tasks else 1 if __name__ == "__main__": sys.exit(main()) ``` 这个脚本展示了完整的批量验证流程。通过并行执行，五个工艺角的验证时间可以大幅缩短。每个任务都有独立的工作目录，包含完整的日志和报告文件。 ## 7. 集成到CI/CD流程与最佳实践 将Formality自动化验证集成到持续集成/持续部署（CI/CD）流程中，可以确保每次代码提交或网表生成后都自动进行LEC检查。以下是一些集成建议和最佳实践： **CI/CD集成示例（GitLab CI）**： ```yaml # .gitlab-ci.yml 示例 stages: - synthesis - formal_verification - report synthesize_design: stage: synthesis script: - dc_shell -f scripts/synthesize.tcl artifacts: paths: - outputs/netlist/*.vg - outputs/svf/*.svf expire_in: 1 week formal_verification: stage: formal_verification dependencies: - synthesize_design script: - python scripts/run_batch_lec.py \ --reference ./rtl \ --implementation ./outputs/netlist \ --svf ./outputs/svf/design.svf \ --lib ./libs \ --top my_design \ --output ./lec_results artifacts: paths: - lec_results/ reports: junit: lec_results/junit_report.xml only: - main - merge_requests ``` **最佳实践表格**： | 实践领域 | 具体建议 | 理由与好处 | |---------|---------|-----------| | **环境配置** | 使用版本固定的Formality工具版本 | 避免工具版本差异导致的结果不一致 | | **文件管理** | 为每次验证创建时间戳目录 | 保留历史记录，便于问题追溯 | | **错误处理** | 实现完善的异常捕获和日志记录 | 快速定位自动化脚本自身的问题 | | **资源管理** | 根据服务器资源限制并行任务数 | 避免License过载或内存耗尽 | | **结果解析** | 不仅解析PASS/FAIL，还提取关键指标 | 建立验证质量的历史趋势分析 | | **报告生成** | 生成人类可读和机器可读（JSON）两种报告 | 便于人工审查和自动化仪表板集成 | | **调试支持** | 失败时自动收集相关日志和报告 | 加速工程师的调试过程 | **性能优化技巧**： 1. **增量验证**：对于大型设计，如果只有部分模块修改，使用`set_dont_verify`命令排除未修改区域。 2. **分层验证**：对层次化设计，先验证子模块，再验证顶层，便于问题定位。 3. **缓存设置**：对于重复验证的相同参考设计，可以缓存设置阶段的结果。 4. **智能超时**：根据设计规模动态调整`verification_timeout_limit`。 ```python # 智能超时设置示例 def calculate_timeout_heuristic(design_size_k gates: int) -> str: """根据设计规模启发式设置验证超时""" if design_size_k < 10: return "0:30:00" # 30分钟 elif design_size_k < 100: return "2:00:00" # 2小时 elif design_size_k < 1000: return "6:00:00" # 6小时 else: return "12:00:00" # 12小时 ``` **常见问题与解决方案**： | 问题现象 | 可能原因 | 解决方案 | |---------|---------|---------| | 大量Unmatched Points | SVF文件缺失或过时 | 确保使用正确的SVF，检查`synopsys_auto_setup`设置 | | 验证时间过长 | 设计规模大或约束复杂 | 启用多核验证：`set_host_options -max_cores 4` | | 内存不足 | 设计太大或同时运行过多任务 | 减少并行任务，增加物理内存，使用64位版本 | | 时钟门控不匹配 | 时钟门控单元处理不当 | 设置`set verification_clock_gate_hold_mode low` | | 扫描链导致失败 | 扫描使能信号未置为常量 | 添加`set_constant`命令禁用扫描模式 | 在实际项目中，我遇到过最棘手的一个情况是，一个大型SoC设计在某个工艺角下总是出现零星的不匹配点。通过自动化脚本，我们快速排除了网表生成问题，最终发现是工艺库中某个特定条件下的单元建模存在细微差异。没有自动化框架，这种跨多个工艺角的系统性验证几乎不可能手动完成。