Axiomise 谈芯片验证中的复杂性：从生物系统思维到 formal-first 工程

文章由 Axiomise 的 Vidya Chandran Darbari 与 Ashish Darbari 撰写，从结构生物学的研究经验出发，讨论芯片设计中“比特之间”的复杂性。作者认为，蛋白质相互作用图谱只标示可能的交互，并不能说明交互何时重要；类似地，芯片中链路能正确传输数据包、控制器能正确进入电源状态、互连能在其假设下正确仲裁，三者的组合仍可能违反需求，因此上下文条件必须写入验证而非仅留在集成说明中。 文章以边缘控制器融合摄像头与距离传感器数据为例：两组测量即使编码准确、传输无损、各自合理，若描述的是不同时刻却被当作同步处理，融合结果仍可能代表从未发生的情形。作者据此提出，时间戳关联、数据新鲜度、允许偏斜与缺失观测都应成为需求的一部分；复位、链路重训练和电源切换期间同样需要回答已接受事务如何处理、恢复后哪个状态存活等问题。 在故障分析部分，文章给出一个 chiplet 系统示例：事务超时，电源控制器在未完成流量排空时门控时钟，而唤醒请求又排在被阻塞流量之后，双方互相等待形成循环依赖。超时只是症状，延长超时无法消除机制；丢失信用、复位状态不一致或饥饿也可能产生同一症状，因此应设计能区分假设的干预实验。 作者由此主张把机制转化为架构义务：流量是否必须先排空才能门控时钟、唤醒投递是否必须独立于正常流量、中断正常序列后会发生什么。Axiomise 所提的 formal-first 指在架构仍可修改时提出这些问题，并强调 formal-first 不等于 formal-only，仿真、仿真加速、物理分析与系统验证提供不同证据，需要围绕可识别的问题连接起来。文章还指出，跨电源管理、流量控制与恢复的失败机制需要有人拥有跨系统义务，电源策略修订应触发对进展性论证的重新评估。