SVA断言面试题的4种写法：要求信号en_1为高电平的时候，断言这期间数据都保持不变。

SVA断言是一个对设计属性的描述，就和日常生活中的逻辑描述一样，条条大路通罗马，不拘细节，力求简洁易懂。

要求信号en_1为高电平的时候，数据都保持不变。容易想到的写法有很多：

第一种

always @(posedge clk1) begin    
  if (~en_1)        
    latch_data <= dat_clk1;    
  else        
    assert (dat_clk1==latch_data);
  end

这类似于一句话能说清楚的事情，长篇大论。不能一句话触及问题的本质。

第二种

@(posedge clk)  disable iff(reset)  
  en_1 && $stable(en_1) |-> $stable(data);


@(posedge clk)  
  en_1 && $past(en_1) |-> $stable(data);

最后还有一种比较巧妙的写法，如果我想要证明 A -> B ，我们可以利用逆否命题证明 ~B ->~A。

如果我们想要断言“信号en_1为高电平的时候，这期间数据都保持不变”，可以转换成“如果数据发生了变化，那么上一拍en_1一定为低电平”

@(posedge clk)  disable iff(reset)  
  !$stable(data) |-> !$past(en_1);

作者：验证哥布林
原文链接：https://mp.weixin.qq.com/s/2LXonDLERRihDaOh5k1lrg
微信公众号：

推荐阅读

更多IC设计技术干货请关注IC设计技术专栏