
左移正演变为系统级问题:Synopsys、Silvaco、Axiomise、Hiveware 专家谈验证与验证扩展
Semiconductor Engineering 圆桌讨论指出,左移正从验证扩展到系统级验证,工具与模型割裂的工作流让已通过验证的组件仍出现 bug 逃逸。Synopsys 的 Frank Schirrmeister 认为智能体 AI 可改善跨学科协调、识别瓶颈并优化工具使用,但无法取代仿真和硬件仿真等基础流程。
NEWS / 动态
按时间浏览,使用右上角筛选切换领域。

Semiconductor Engineering 圆桌讨论指出,左移正从验证扩展到系统级验证,工具与模型割裂的工作流让已通过验证的组件仍出现 bug 逃逸。Synopsys 的 Frank Schirrmeister 认为智能体 AI 可改善跨学科协调、识别瓶颈并优化工具使用,但无法取代仿真和硬件仿真等基础流程。

Synopsys、Silvaco、Axiomise与Hiveware专家在Semiconductor Engineering圆桌讨论中指出,AI智能体和数字孪生正让材料、晶体管结构与芯片架构等更多设计选项得以更早探索,但左移并未消除验证瓶颈。

Axiomise 的 Ashish Darbari 等人发文提出,数据通路验证的缺陷正从数值错误转向状态标志错误,即结果看似正确但异常标志缺失或误报。

Axiomise 的 Bing Xue 与 Ashish Darbari 撰文指出,传统仿真(含 UVM 测试平台与模糊测试)无法覆盖相干 NoC 中事务交织、虚拟通道、信用与路由表变化等状态空间,流控与信用记账错误、排序违规、一致性状态机错误、死锁及安全侧信道泄漏等深层缺陷可能在奇偶校验与 ECC 通过的情况下仍造成数据损坏或系统冻结。

Axiomise 工程师用 floatrix 在 fpnew FPU 的 BF16 除法器中发现一处下溢漏报:该单元内部以 FP32 计算,对极小结果判定为无下溢、无 inexact,但舍入到 BF16 后该值变为极小且 inexact,按 RISC-V BF16 规则应报下溢,由于标志逻辑绑定 FP32 而非 BF16,设计静默漏掉该异常。

Axiomise 创始人 Ashish Darbari 在 DVCon USA 后整理形式验证的 11 个常见问题,称团队近期对含 3.38 亿触发器、11 亿门的深度时序设计一次性整体编译,未做 cut-point 或 boxing,借助 Axiomise proof accelerators 在数秒内发现缺陷。

Axiomise 提出 ADEPT FV 形式验证流程,以 Avoid、Detect、Erase、Prove 四阶段贯穿设计全程,目标是尽早发现缺陷、证明正确性并持续构建覆盖率,从而减少流片风险。

Axiomise 的 Ashish Darbari 以案例形式展示了如何用形式验证穷尽验证串行数据包设计。这类设计因每个数据包状态依赖此前所有在途数据包的历史而难以验证,作者采用智能追踪器(smart tracker)抽象,结合不变量作为辅助属性与 assume-guarantee 流程,在保证不遗漏合法行为缺陷的同时改善证明收敛。

Axiomise 创始人兼 CEO Ashish Darbari 撰文分析形式验证虽在业界屡获成功却仍未被每位设计与验证工程师日常使用,原因集中在缺乏良好培训、缺乏覆盖从轻量 app 到端到端深度形式验证的完整方法论、流程常因人言而非基于指标的经验分析摇摆,以及项目内缺乏连续性应用。

Axiomise 的 Ashish Darbari 基于在 OneSpin Solutions 的 EDA 从业经历与 DVCon USA 讨论,提出成功部署形式验证的十条规则,强调形式验证成功靠方法论与纪律而非博士学位。

Axiomise 的 Ashish Darbari 撰文指出,Meltdown 与 Spectre 暴露的安全漏洞说明安全不只是软件问题,而是系统问题,需在设计前端就纳入架构考量。他认为动态仿真难以扩展、单纯仿真也不够,应引入形式化验证等手段;文中以他协助验证一款可定制 CPU 的经历为例,形式化测试平台发现了非特权访问特权内存区域等漏洞,部分源于设计疏漏或实现与规格不符。