4. Versal可编程逻辑设计验证基础

Versal 的可编程逻辑部分虽然与经典 FPGA 同源，但器件规模、时钟资源、NoC 与 AI Engine 的耦合方式，使“能综合、能布线、能收敛”不再等于“可交付”。本节把 PL 设计验证拆成五道相互衔接的关口：RTL 设计规则、综合与实现检查、时序约束、DRC 检查、逻辑等效性验证。它们不是五个独立工具步骤，而是一条从代码语义到物理实现、再到功能等价确认的证据链。

RTL 设计规则：先让代码可综合、可约束、可复用

RTL 规则的核心不是“风格好看”，而是消除综合与实现阶段无法解释的歧义。第一类是时钟与复位规则：每个时钟域必须有明确的时钟源和复位策略，避免在 always 块中混用上升沿与下降沿，避免异步复位释放不经过同步器。第二类是组合逻辑规则：禁止组合环，避免在同一个 always 块中既产生锁存又产生寄存器，避免对同一信号在多处赋值。第三类是跨时钟域规则：单比特控制信号用两级触发器同步，多比特数据用握手或异步 FIFO，禁止直接对多比特总线做打拍。

一个常见的教学示例是：设计一个 100 MHz 到 200 MHz 的跨时钟域脉冲传递模块。若直接写 always @(posedge clk_b) pulse_b <= pulse_a;，综合器不会报错，但实现后可能因亚稳态导致脉冲丢失。正确做法是先在 clk_a 域把脉冲展宽为电平，再在 clk_b 域同步并边沿检测。这类规则应在 RTL 评审阶段用 lint 工具固化，而不是等到时序报告出来再回头改。

综合与实现检查：看资源、看拥塞、看 QoR

综合阶段要回答三个问题：逻辑是否被正确推断、资源是否在预算内、是否存在明显的结构性问题。综合日志中应重点检查：是否出现 latch 推断、是否出现大量分布式 RAM 替代 BRAM、是否出现 DSP 未被推断而用 LUT 搭建乘法器。实现阶段则关注布线拥塞、时钟资源冲突和长路径分布。Versal 的 SLR 结构使跨 SLR 路径天然更贵，若关键路径频繁跨越 SLR，应优先调整布局约束或复制逻辑，而不是一味加流水。

下表给出一个示例性的资源与 QoR 检查清单，数值为教学假设，用于说明观察口径：

时序约束：把设计意图写成工具能读的契约

时序约束的本质是把“设计意图”翻译成工具可验证的断言。主时钟用 create_clock 定义，生成时钟用 create_generated_clock 描述分频或倍频关系，输入输出延迟用 set_input_delay/set_output_delay 描述外部器件接口，跨时钟域路径用 set_clock_groups -asynchronous 或 set_false_path 明确豁免。约束不完整时，工具会“乐观”地认为路径无需检查，导致时序报告虚假收敛。

create_clock -name clk_a -period 10.000 [get_ports clk_a]
create_clock -name clk_b -period 5.000  [get_ports clk_b]
set_clock_groups -asynchronous -group {clk_a} -group {clk_b}
set_input_delay -clock clk_a -max 2.000 [get_ports data_in]
set_output_delay -clock clk_b -max 1.500 [get_ports data_out]

约束完成后必须做一次“约束覆盖率”检查：确认所有时钟都已定义、所有 I/O 都有延迟、所有跨时钟域路径都有明确处理。若某条路径既没有约束也没有豁免，它就会成为实现阶段的隐患。

DRC 检查：把物理规则问题挡在交付之前

DRC 检查覆盖电气规则与物理规则两类。电气规则包括 I/O 标准与 bank 电压匹配、差分对极性、时钟能力引脚使用是否正确；物理规则包括布线短路、未布线网络、过孔与金属密度等。Versal 中尤其要注意 GT 通道、PCIe 硬核和 NoC 连接相关的专用规则，这些接口的 DRC 违例往往不能靠改 RTL 解决，而要在约束或管脚分配阶段修正。

逻辑等效性验证：确认优化没有改变功能

逻辑等效性验证（LEC）用于确认综合、优化、插入流水或重定时之后，网表功能与原始 RTL 一致。典型流程是：以 RTL 为参考端，以综合后网表为实现端，先做“setup”建立映射关系，再运行“compare”。若出现非等效点，需区分是真实功能差异，还是因为未约束、黑盒、或时钟域处理导致的假失败。对于跨时钟域路径，LEC 通常需要设置 set_analyze_boundary 或等效的边界处理，否则同步器会被误判。

把五道关口串起来看，它们的关系可以用下面的信号链与检查点图表示：RTL 规则决定代码能否被正确解释，综合与实现检查暴露资源与结构问题，时序约束定义性能契约，DRC 保证物理可实现，LEC 确认功能等价。任何一环缺失，交付证据都不完整。

实际项目中，建议把上述检查固化为一次“签核前评审”：先看 RTL lint 是否清零，再看综合日志有无意外推断，再看实现后的 WNS/TNS 与跨 SLR 路径，再看 DRC 关键违例，最后看 LEC 的 compare 结果。只有五份证据同时成立，PL 设计才具备进入系统级验证与交付的条件。