规范与自动化之间的差距挑战
半导体行业在尝试将人工智能集成到现有设计流程中时,面临着一个根本性的挑战。核心问题不在于大语言模型(LLMs)编写代码的能力,而在于构建这些代码的“规范”(Specifications)的质量。虽然人工智能可以在几秒钟内生成 SystemVerilog 断言(SVA),但这些结果完全取决于输入的准确性,而目前的行业输入往往是不完整或模糊的。
专家指出,人工智能的真正目标不应仅仅是从自然语言编写的规范中生成属性(Properties),而应协助制定更好、更精确的技术规范。用散文形式编写的规范无法被形式化验证工具(Formal Tools)直接处理,因为它们缺乏这些工具所要求的数学精确性。
工程师的角色在实践中会发生什么变化?
认为属性生成自动化会消除对专业验证工程师的需求是一种错误的想法。恰恰相反,这种转变提高了对技能水平的要求。工程师的角色将从花费时间手动编写断言,转向“审查和验证人工智能输出的正确性”阶段。
- 逻辑验证:工程师必须确保生成的断言覆盖了实际需求,而不仅仅是语法正确的代码。
- 复杂度管理:随着片上系统(SoC)复杂性的增加,解释形式化验证工具结果的能力变得至关重要。
- 应对模糊性:人工智能可能无法识别规范中的矛盾之处,这使得发现这些漏洞的负担落在了人类工程师身上。
技术风险:“空断言”陷阱
在这个领域使用人工智能面临的最危险挑战之一是所谓的“空断言”(Vacuous Assertions)。这些断言在编程上看起来是正确的,并能通过验证工具的测试,但实际上它们并没有验证设计的任何真实行为,因为它们的条件无论芯片性能如何都会自动满足。
这类错误可能会导致对设计安全性的虚假信心,从而在后期发现缺陷时造成高昂的成本,无论是验证工具的时间消耗,还是工程师在调试(Debugging)方面的时间投入。
迈向更可靠的方法论
为了从实验阶段过渡到稳定的工业应用,专家提出了几条路径:
- 使用 RAG 技术:通过“检索增强生成”(Retrieval-Augmented Generation)技术增强人工智能模型,将其与包含设计规则和已验证模式的专业知识库联系起来,而不是仅仅依赖模型在训练期间学到的内容。
- 基于形式化规范的设计:转向从一开始就编写“机器可读”(Machine-readable)的规范,从而缩小人类文本与数学逻辑之间的差距。
- 渐进式方法:首先在小型、有限且易于理解的设计模块(Blocks)上应用自动化,并在扩展到完整设计之前,将人工智能的输出与工程师手动编写的结果进行比较。