4 布尔表达式与HDL信号引用

4.1 问题背景

PSL属性中的核心逻辑原子是布尔表达式。无论是描述“当条件成立时得到响应”的蕴含属性，还是约束“不允许出现某状态”的拒绝属性，最终都要落在具体的信号引用与布尔运算上。实际验证中，大量初学错误并不来自属性时态逻辑本身，而是来自信号引用方式不准确：向量位序写反、位选择方向错误、整向量直接当布尔量使用、跨模块路径缺失、运算符优先级歧义等。

4.2 核心概念

信号（Signal）：PSL中直接引用的HDL线网或寄存器量，通常为单比特标量，如 rst_n、hsel。标量信号可以被 PSL 直接当作布尔量使用，但工程上建议显式写成 (rst_n == 1'b1)，使验证语义更清晰。

向量（Vector）：多位宽总线量，如 haddr[31:0]、data[7:0]。向量不能直接作为布尔量参与 &&、|| 运算，必须通过比较运算或位选择将其转化为单比特值。

位选择与切片（Bit Select / Slice）：从向量中取出单比特或连续子段。Verilog 风格为 bus[i]、bus[msb:lsb]；VHDL 风格为 bus(i)、bus(msb downto lsb)。PSL 遵循 HDL 原生的位选择规则。

表达式运算符：PSL 布尔表达式支持逻辑非 !、逻辑与 &&、逻辑或 ||、关系比较 ==、!=、<、<=、>=、> 等。运算符优先级与 C/Verilog 基本一致，但复杂表达式必须加括号。

下图展示了从HDL信号引用到PSL求值上下文的核心路径：

4.3 原理机制：布尔表达式在 PSL 中的求值上下文

PSL 中的布尔表达式不是在仿真器任意时刻连续求值的组合逻辑，而是在时钟边界上采样后得到的确定真值。求值上下文由三部分决定：

• 时钟约束：表达式在 default clock 指定的边沿计算，例如 posedge clk；
• 采样语义：时钟边沿触发时，所有信号值取采样值，禁止组合竞争依赖；
• 不确定状态：形式验证中，X/Z 不参与真值判断，而是按未知态处理。

// 不推荐：向量隐式转布尔
assert always (bus) -> p;

// 推荐：显式比较
assert always (bus != 3'b000) -> p;

4.4 编写无歧义布尔表达式的流程步骤

1. 定位信号层次：确认信号在 PSL unit 或 HDL 设计层次中可见，必要时使用 hdlpath 完整路径；
2. 确认类型与位宽：区分标量/向量，记录位宽及位序声明；
3. 选择位选择或切片：对于总线信号，按需取出特定位或子段，保证索引方向与声明一致；
4. 选择运算符：使用逻辑运算符、关系运算符，将子表达式组合为单比特结果；
5. 加括号明确优先级：不依赖记忆中的优先级，为每个子表达式加括号；
6. 绑定时钟与采样上下文：检查 default clock 是否覆盖当前属性；
7. 语义检查：在验证工具中运行语法与静态检查，确认表达式无类型错误。

4.5 案例说明：AHB 桥接场景下的信号引用

假设一个 AHB-APB 桥接器，DUT 接口声明片段如下：

module ahb_apb_bridge (
  input wire        hclk,
  input wire        hresetn,
  input wire        hsel,
  input wire        hwrite,
  input wire [2:0]  hsize,
  input wire [31:0] haddr
);

PSL 属性要求：当主设备发起 4 字节或 8 字节写传输时，地址必须按传输宽度对齐。

unit psl_ahb_example {
  default clock = (posedge hclk);
  default disable iff (hresetn == 1'b0);

  // 规则1：4字节传输时，地址低2位必须为 0
  aligned_4byte: assert always 
    (hsel && hwrite && (hsize == 3'b010)) 
    -> (haddr[1:0] == 2'b00);

  // 规则2：8字节传输时，地址低3位必须为 0
  aligned_8byte: assert always 
    (hsel && hwrite && (hsize == 3'b011)) 
    -> (haddr[2:0] == 3'b000);
}

4.6 信号引用形式速查表

4.7 误区提醒

4.8 实践清单