标签: system-verilog-assertions

我有一些来自1位串行端口的数据,它有多个字节的变量长度,如下所示:

byte expected_1 [$] = {8'hBA, 8'hDD, 8'hC0, 8'hDE};
byte expected_2 [$] = {8'h01, 8'h23, 8'h45, 8'h67, 8'h89, 8'hAB, 8'hCD, 8'hEF};  

在每个正时钟边沿,发送一位.我需要testbench对序列的追求(将来可能有数千个),所以我想在系统verilog中使用断言自动化该过程.新的2012标准允许将队列传递给属性,但队列是否可以通过递归属性发送？我收到一些关于分层引用的错误.

这是我迄今为止(从@格雷格帮助这里):

default clocking sck @(posedge sck); endclocking : sck  

sequence seq_serial(logic signal, logic [7:0] expected); // check each bit
  byte idx = 7;
  (signal == expected[idx], idx--)[*8];
endsequence : seq_serial

property recurring_queue(bit en, logic data, byte data_e [$])
  int queue_size = data_e.size;
  logic [7:0] expected = data_e.pop_front(); 

  if(queue_size != 0) (
    !en throughout (seq_serial(data, expected) ##1 …

以下两个属性有何不同？

property p1;
    @(posedge clk) disable iff (Reset) b ##1 c;
endproperty

property p2;
    @(posedge clk) (~Reset & b) ##1 c;
endproperty

assert property (p1);
assert property (p2);

对于这段代码，我看到两个断言都失败了。似乎禁用 iff (value) 的计算晚于表达式本身。有人可以解释一下吗？

module tb();
reg clk = 1;
always #5 clk = !clk;
reg rst = 1;
always @ (posedge clk)
    rst <= 0;

initial #11ns $finish();

assert property (@ (posedge clk) disable iff (rst) 1 |-> 0);
assert property (@ (posedge clk) rst |-> 0);
endmodule

后续，如何测试这一点：

always_ff @ (posedge clk or posedge rst) begin
    if (rst) q <= 0;
    else q <= d;
end

其中 rst 根据延迟被取消断言：

always_ff @ (posedge clk)
    rst <= rst_a;

似乎禁用 iff …

我有两个打包的信号数组,我需要为该属性创建一个属性和相关的断言,证明这两个数组在某些条件下是相同的.我正式验证并且该工具无法在单个属性中证明两个完整数组,因此我需要将其拆分为单个元素.那么有没有办法可以使用循环为数组的每个元素生成属性？目前,我的代码非常冗长,难以导航.

我的代码目前看起来像这样:

...
property bb_3_4_p; 
  @(posedge clk)
     bb_seq  
     |=>     
     bb_exp [3][4] == bb_rtl [3][4] ;
endproperty

property bb_3_5_p; 
  @(posedge clk)
     bb_seq  
     |=>     
     bb_exp [3][5] == bb_rtl [3][5] ;
endproperty

property bb_3_6_p; 
  @(posedge clk)
     bb_seq  
     |=>     
     bb_exp [3][6] == bb_rtl [3][6] ;
endproperty
...

...
assert_bb_3_4: assert property (bb_3_4_p);
assert_bb_3_5: assert property (bb_3_5_p);
assert_bb_3_6: assert property (bb_3_6_p);
...

这就像我希望我的代码看起来像:

for (int i = 0; i < 8; i++) 
  for (int j = 0; j < 8; j++) 
  begin   
     property bb_[i]_[j]_p;
        @(posedge …

最近出现了一个问题，通常的隐含运算符（|->）和impliesSystemVerilog中的运算符之间有什么区别。不幸的是我找不到一个明确的答案。但是，我收集了以下信息：

从SystemVerilog LRM 1800-2012：

• 第16.12.7节隐含和iff属性：

  property_expr1 implies property_expr2
  仅当property_expr1的值为false或property_expr2的值为true时，此形式的属性的值为true。

• §F.3.4.3.2 派生布尔运算符：

  p1 implies p2 ≡ (not p1 or p2)

• §F.3.4.3.4 派生的条件运算符：

  (if(b) P) ≡ (b |-> P)

但是，LRM并未真正指出实际的区别是什么。我假设在错误的先行情况下（成功与空前成功），它们的评估有所不同，但是我无法找到此假设的任何来源或证据。此外，我知道implies操作员与OneSpin等正式验证工具结合使用非常普遍。

有人可以帮我吗？

PS：似乎在下一本书中对此问题有一个答案：SystemVerilog断言手册，第三版。但是155美元对我来说太过分了，只是为了得到这个问题的答案:)

我有一个verilog模块的串行输出，我想使用system-verilog进行测试。

给定正确的串行输入“ SI”（其值为8'h9A），称为“ SO”的输出将输出类似于8'hC6的输出。

是否有一种无需明确描述每个信号的简单方法来编码/解码串行IO？

例如：

assert property @(posedge clk) $rose(EN) |-> ##[1:3] SI ##1 !SI[*2] ##1 SI[*2] ##1 !SI ##1 SI ##1 !SI
                                             ##[1:3] SO[*2] ##1 !SO[*3] ##1 SO[*2] ##1 !SO;

它看起来像一团混乱，几乎不可读。我非常想写

8'h9A ##[1:3] 8'hC6

但显然这是行不通的。任何建议或示例都将受到欢迎。提前致谢。

这个问题是关于系统verilog宏。
我有一个顶级模块、子模块和一个子子模块。在顶层模块中实例化的子模块中实例化的子子模块。

`define abc 如果我在子模块中定义宏，里面编写的代码是否`ifndef abc会在顶级模块/子子模块中编译

这是一个规范:如果信号a被置位,那么它必须被置位直到信号b被置位然后它应该在下一个时钟边沿取消置位.我正在阅读LRM的16.9.9(以及http://www.testbench.in/AS_06_SEQUENCES.html)和我理解的方式,上面提到的规范可以写成

   property a2b_notA;
        @(posedge clk) ($rose (a) ##0 (a throughout b)) |=> (~a);
   endproperty
   a_a2b_notA: assert property (a2b_notA);

然而,这在启动后第二个时钟边沿立即失败,我无法弄清楚原因.

有没有一种方法可以为SystemVerilog原语添加断言，或者仅在包装该原语的模块（单元）中添加断言？简单地添加一个断言不会编译

   primitive mux (q, d0, d1, s);
   output q;
   input s, d0, d1;

   table
   // d0  d1  s   : q 
      0   ?   0   : 0 ;
      1   ?   0   : 1 ;
      ?   0   1   : 0 ;
      ?   1   1   : 1 ;
      0   0   x   : 0 ;
      1   1   x   : 1 ;
   endtable
   //assert(s != x) else $error("s has value x"); - add this assertion
endprimitive

我试图了解何时$rose在断言中使用信号.例如,下面两个断言在哪些方面表现不同？

first:assert property 
        (@(posedge clk) $rose(reset) |-> (data == 0));

second: assert property
          (@(posedge clk) reset |-> (data==0));

它$rose是否与异步信号一起使用？

我想检查变量的当前值是否为“1”，则变量的先前值应该为“0”。我在系统 Verilog 断言中使用 $past。这里我检查cal_frame_mode是否=1，那么它是cal_frame_mode=0的先前值。我的代码如下。但是，我看到断言失败。当我检查波形时，它的行为正确。第一次检查后 2 个时钟后断言标记。如何在仅检查一个时钟周期后停止此断言？

property p_NOP_2_RX_CAL;
  @(posedge clk)
  (cal_frame_mode==3'b001) |-> ##2 $past(cal_frame_mode)==3'b000;  
endproperty

assert_nop2cal : assert property(p_NOP_2_RX_CAL);