2.2.1.2 二叉决策图（BDD/ROBDD）

文档摘要

2.2.1.2 二叉决策图（BDD/ROBDD） 2.2.1.2 二叉决策图（BDD/ROBDD）：变量序优化不是玄学——一次因引发的内存爆炸与三行代码救场实录凌晨两点十七分，EDA工具链在形式验证阶段卡死。服务器内存使用率冲上98%，显示三个进程各自吞下24GB虚拟内存，而它们本该在毫秒级完成一个16输入组合逻辑的等价性检查。日志里只有一行冰冷的警告：这不是第一次。过去三个月，团队已在五个不同模块的BDD建模中遭遇类似崩溃——有时是综合后网表，有时是手工编写的Verilog行为模型，共同点只有一个：所有失败案例的变量顺序（variable order）都未经显式控制，完全依赖Cudd库默认的输入端口声明顺序。我们曾以为ROBDD是“规整化”的代名词——唯一、规范、可判定。