Yosys工具中组合环路检测问题的技术分析与解决方案

在数字电路设计验证过程中，组合逻辑环路（Combinational Loop）的检测是一个关键环节。近期在使用Yosys工具对CVA6浮点运算单元控制器进行BTOR格式转换时，工具错误地报告了组合环路的存在。本文将深入分析该问题的技术本质，并提供有效的解决方案。

问题现象

当用户尝试将CVA6 FPU控制器的miter电路转换为BTOR格式时，Yosys 0.48+77版本报告检测到组合逻辑环路。值得注意的是，这种环路仅在创建miter电路后出现，而原始设计中并不存在真正的组合环路。

技术分析

经过深入调查，发现该问题并非由miter电路创建引起，而是Yosys在原始设计源代码中检测到的潜在环路。核心问题在于：

1. 信号传播路径分析：

   • Sqrt_Q1信号通过Iteration_cell_b_BMASK_D[1]传播
   • 继而影响Iteration_cell_b_D[1]
   • 再传递至Iteration_cell_carry_D[1]
   • 最终反馈回Sqrt_quotinent_S信号
   • 形成完整的环路

2. 工具局限性：

   • Yosys在字级（word-level）分析时可能产生虚假环路检测
   • BTOR后端严格要求不能存在任何字级环路
   • 这种检测在逻辑综合（synth）后会消失，说明是字级特有的现象

验证方法

为确认该环路的真实性，可采用以下验证手段：

1. 使用基础检测脚本：

read_verilog -sv control_mvp.sv
prep -top control_mvp -flatten
scc -expect 0

2. 通过Verilator进行静态检查：

verilator --lint-only control_mvp.sv --top control_mvp

解决方案

针对此类问题，推荐以下解决方法：

1. 代码修改方案： 在信号赋值处采用逐位赋值方式，打破工具检测到的虚假环路。例如：

case (Format_sel_S)
    2'b00: begin
        Sqrt_quotinent_S = {...};
        // 添加逐位赋值
        Sqrt_quotinent_S[3] = Sqrt_quotinent_S[3];
        Sqrt_quotinent_S[2] = Sqrt_quotinent_S[2];
        Sqrt_quotinent_S[1] = Sqrt_quotinent_S[1];
        Sqrt_quotinent_S[0] = Sqrt_quotinent_S[0];
        ...
    end
endcase

2. 工具使用技巧：
   • 尝试使用splitnets -driver命令分离驱动网络
   • 在综合前进行适当的优化处理

结论

该案例展示了在高级综合工具中字级分析可能带来的虚假环路检测问题。开发者需要理解工具的工作原理和局限性，在必要时通过代码结构调整或特定工具命令来规避这类问题。对于Yosys工具而言，这不是一个功能缺陷，而是字级分析固有的技术限制。

在实际工程中，建议开发者在遇到类似问题时，首先通过多种工具交叉验证，确认环路的真实性，再选择最适合的解决方案，确保设计正确性的同时保持代码的可维护性。