Agnisys 与 Axiomise 合作加速 NoC 设计与形式化签核
Agnisys 与 Axiomise 宣布合作,将 Agnisys 的 IDS-NoC 自动 NoC 生成与 Axiomise 的 nocProve 形式化验证技术结合,面向 AI 处理器、GPU 和 AI 推理引擎等 NoC 设计。双方称该组合旨在缩短上市时间、提升复杂 NoC 设计的质量与验证置信度,减少流片前意外和重投片。
NEWS / 动态
按时间浏览,使用右上角筛选切换领域。
Agnisys 与 Axiomise 宣布合作,将 Agnisys 的 IDS-NoC 自动 NoC 生成与 Axiomise 的 nocProve 形式化验证技术结合,面向 AI 处理器、GPU 和 AI 推理引擎等 NoC 设计。双方称该组合旨在缩短上市时间、提升复杂 NoC 设计的质量与验证置信度,减少流片前意外和重投片。

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 的经历为例,形式化测试平台发现了非特权访问特权内存区域等漏洞,部分源于设计疏漏或实现与规格不符。

Axiomise 的 Ashish Darbari 讲述自己从印度工程师家庭出身、在 Birla Institute of Technology 学习电气电子工程,到在 TU Dresden 攻读计算逻辑硕士,最终选择形式验证方向博士offer的历程。他曾在 Intel、ARM、Imagination 和 OneSpin 任职,文章以其个人经历映照形式验证领域的发展。