AI芯片验证公司获种子轮融资
摘要
北京有理数科技由Axiom Math前形式化验证负责人张巨见与前月之暗面研究者刘俊杞创立，用AI自动完成芯片形式化证明。已跑通技术原型，在十几万行RTL代码的芯片项目中，验证了部分现有EDA工具无法判定的断言。
原文片段
前Axiom Math、Kimi研究者联手创业，用AI攻克芯片验证难题 动察 Beating AI 快讯，芯片设计最怕的事情之一，就是制造出来以后才发现逻辑错误。一旦出现问题，可能需要重新设计、重新流片，付出高昂成本。芯片验证就是要在制造前，尽可能找出这些隐藏的错误。 传统芯片验证主要依赖仿真测试，但芯片内部的运行状态组合可能达到天文数字，根本不可能逐个测试。形式化验证则利用数学方法，证明芯片在规定条件下始终遵守某条规则。例如，两个本来不能同时开启的电路，绝不能因为某种特殊操作而一起开启。 这种方法早已存在，但复杂芯片的数学证明非常困难。许多问题需要专家手工处理，现有工具也可能因为计算规…