如何在信号未知时禁用断言？MUX模块初始状态断言问题咨询

问题描述 #

我正在尝试给一个MUX模块写断言，目的是检查SEL1、SEL2和SEL3信号的互斥性，写了如下断言：

always @(posedge CLOCK)
  assert (SEL1 == 1 && SEL2 ==0 && SEL3 == 0);

运行后遇到了断言失败，第一次失败的提示是：

xmsim: *E,ASRTST (./testbench.sv,31): (time 5 NS) Assertion T_MUX.MUX1.__assert_1 has failed 
Starting 1st set of test vectors.

我判断这次失败不是SELx的有效值错误导致的，而是系统初始化、复位前的未知值（x态）引发的。想知道怎么针对未知初始状态正确编写断言检查器。

附MUX模块代码：

module MUX       
(                
  input wire       CLOCK  ,
  input wire [3:0] IP1    ,
  input wire [3:0] IP2    ,
  input wire [3:0] IP3    ,
  input wire       SEL1   ,
  input wire       SEL2   ,
  input wire       SEL3   ,
  output reg [3:0] MUX_OP
) ;              
                 
always @(posedge CLOCK)
  if (SEL1 == 1) 
    MUX_OP <= IP1 ;
  else if (SEL2 == 1)
    MUX_OP <= IP2 ;
  else if (SEL3 == 1)
    MUX_OP <= IP3 ;                     

always @(posedge CLOCK)
  assert (SEL1 == 1 && SEL2 ==0 && SEL3 == 0);
endmodule

解决思路 #

1. 先修正互斥性检查的逻辑错误 #

你当前的断言只检查了SEL1有效时其他选通信号为0的情况，完全不是完整的互斥性检查。互斥性要求任意时刻最多只有一个SELx为1，且必须有一个SELx为1，用SystemVerilog内置函数$onehot可以直接实现这个逻辑：

// 正确的互斥性检查：信号组中恰好一位为1
assert( $onehot({SEL1, SEL2, SEL3}) );

2. 处理初始未知态（x/z态）的问题 #

系统复位前或初始化阶段，信号会处于未知态，此时逻辑判断会返回x（视为假）导致断言误触发，有两种常用解决方法：

方法一：用复位信号屏蔽初始阶段的断言

在断言中加入复位条件，只在复位完成后执行检查。如果用并发断言（更推荐的SystemVerilog写法）：

property sel_mutex;
  @(posedge CLOCK) disable iff (!RESET_n) // 低有效复位时，复位期间禁用断言
    $onehot({SEL1, SEL2, SEL3});
endproperty
assert property(sel_mutex) else $error("SEL信号不满足互斥要求");

如果用过程块断言：

always @(posedge CLOCK)
  if (!RESET_n) begin
    // 复位阶段不做检查
  end else begin
    assert( $onehot({SEL1, SEL2, SEL3}) )
    else $error("SEL信号互斥性失败");
  end

方法二：忽略未知态的检查

如果设计允许初始阶段的未知态，可以先判断信号是否全为已知值（0/1），再执行断言：

always @(posedge CLOCK)
  if (!$isunknown({SEL1, SEL2, SEL3})) begin // 信号无x/z态时才检查
    assert( $onehot({SEL1, SEL2, SEL3}) )
    else $error("SEL信号不满足互斥要求");
  end

$isunknown函数会在信号包含x或z时返回1，取反后就只在信号状态明确时执行断言。

内容的提问来源于stack exchange，提问作者Carter