📚 课程目录第4章属性建模与SoC接口协议

4. 属性建模与SoC接口协议

在SoC属性验证中，接口协议断言是覆盖面最广、复用价值最高的一类属性。AMBA系列协议（AXI、AHB、APB）定义了明确的握手、传输、乱序与超时规则，这些规则天然适合用SVA（SystemVerilog Assertion）表达。本节围绕这三类协议，说明如何把协议文本转化为可执行的断言，并给出可直接参考的建模示例。

一、三类协议的握手差异是断言建模的起点

AXI采用五通道独立握手：写地址AW、写数据W、写响应B、读地址AR、读数据R。每个通道都用VALID/READY一对信号完成握手，规则是“VALID一旦拉高必须保持到READY拉高”，且VALID不得依赖READY。AHB是流水线式总线，地址阶段与数据阶段重叠，HREADY控制流水推进，HTRANS表示传输类型。APB则是最简单的两拍握手：PSEL与PENABLE配合，PREADY结束传输。

断言建模的第一步，是把“握手成立”写成时序属性。以AXI写地址通道为例，核心断言是VALID保持与握手完成：

// AXI AW通道：VALID拉高后必须保持，直到READY采样为高
property p_aw_valid_stable;
  @(posedge ACLK) disable iff (!ARESETn)
  (AWVALID && !AWREADY) |=> AWVALID;
endproperty
a_aw_valid_stable: assert property(p_aw_valid_stable);

// 握手完成：VALID与READY同时为高的当拍即完成一次地址传输
property p_aw_handshake;
  @(posedge ACLK) disable iff (!ARESETn)
  AWVALID && AWREADY |=> ##1 !$stable(AWADDR) || AWVALID;
endproperty

这里需要说明参照约定：所有断言均在ACLK上升沿采样，disable iff (!ARESETn)表示复位期间不检查。VALID保持属性用“|=>”重叠蕴含，表示当前拍成立则下一拍继续成立，这是AXI握手断言的标准写法。

二、传输行为断言：地址、数据与响应的对应关系

握手只保证单拍信号合法，传输行为断言要保证跨通道的一致性。AXI写事务要求：AW与W可以乱序到达，但B响应必须对应已完成的写事务；WLAST必须与AWLEN匹配；写数据字节数必须与AWSIZE、AWLEN一致。读事务要求RLAST与ARLEN匹配，RID与ARID对应。

一个实用的传输断言是WLAST与AWLEN的匹配检查。假设AWLEN为4（即5拍数据），则WLAST应在第5拍数据出现：

// 记录AW握手时的AWLEN，检查WLAST出现在正确的数据拍
property p_wlast_match;
  @(posedge ACLK) disable iff (!ARESETn)
  (AWVALID && AWREADY) |-> ##[1:$] (WVALID && WREADY && WLAST)
    [*1] within (1 + AWLEN) [*1];
endproperty

更严谨的做法是用辅助计数器或局部变量记录AWLEN，在W通道逐拍递减，当计数归零时检查WLAST。这种“跨通道计数”是AXI传输断言最常见的实现方式，也是属性建模从单信号走向事务级的关键一步。

三、乱序行为断言：ID与顺序的约束

AXI允许不同ID的事务乱序完成，但同一ID的读数据必须按序返回。这是乱序断言的核心。对于读通道，若ARID相同，则R响应顺序必须与AR顺序一致；不同ARID之间可以交错。写通道同理，同一AWID的B响应必须按序。

乱序断言通常需要维护一个按ID分组的顺序队列。在SVA中可用数组或队列配合局部变量实现。简化版断言可检查：同一ID的连续两次读事务，第二次的RLAST不得早于第一次的RLAST出现。这类属性在验证DMA、多核缓存一致性等场景中尤为重要，因为乱序错误往往不会导致功能失败，却会在高并发下暴露数据错配。

四、超时行为断言：用时间窗口约束响应

超时断言用于检测“请求发出后长时间无响应”的异常。AXI协议本身不规定超时，但SoC集成中通常要求从设备在有限周期内响应。建模方式是：在请求握手后启动一个计数器，若在N拍内未收到响应，则报错。

// 读地址发出后，最多等待MAX_LATENCY拍必须收到RVALID
property p_read_timeout;
  @(posedge ACLK) disable iff (!ARESETn)
  (ARVALID && ARREADY) |-> ##[1:MAX_LATENCY] RVALID;
endproperty
a_read_timeout: assert property(p_read_timeout)
  else $error("Read timeout: no RVALID within %0d cycles", MAX_LATENCY);

AHB的超时断言可基于HREADY：若HTRANS为NONSEQ且HREADY长时间为低，说明从设备未完成响应。APB则检查PENABLE拉高后PREADY在限定周期内拉高。三类协议的超时建模思路一致，区别只在触发信号和响应信号不同。

五、从协议文本到断言库的落地方法

实际项目中，不建议为每个接口从零编写断言，而是建立可复用的协议断言库。落地方法分四步：第一，按协议通道拆分断言文件，如axi_handshake.sv、axi_order.sv、axi_timeout.sv；第二，用参数化宏控制MAX_LATENCY、ID_WIDTH等配置，使断言库适配不同项目；第三，为每条断言绑定覆盖点，统计握手、乱序、超时场景的触发次数；第四，在仿真回归中把断言失败与波形时间戳关联，便于缺陷定位。

需要特别注意的是，超时断言的阈值不能拍脑袋设定。合理做法是先跑一轮无超时约束的仿真，统计各从设备的实际最大响应延迟，再取该延迟的1.5至2倍作为MAX_LATENCY。阈值过小会产生大量误报，过大则失去检测意义。

建模建议：先用“握手—传输—乱序—超时”四层结构梳理协议规则，再逐层写断言。握手层保证单拍合法，传输层保证事务完整，乱序层保证ID语义，超时层保证活性。四层都覆盖后，接口协议属性验证才算完整。

最后，断言命名应体现协议、通道和行为，例如a_axi_aw_valid_stable、a_ahb_htrans_legal、a_apb_penable_timeout。清晰的命名在回归报告中能直接定位到协议层，大幅缩短从断言失败到根因分析的路径。