Systemverilog 中的多时钟断言

Question

这是设计代码：

module mul_clock (input clkA, clkB, in, output out);
  bit temp;
  reg x[2:0];

  always @ (posedge clkA)
    temp <= temp ^ in;

  always @ (posedge clkB)
    x <= {x[1:0], temp};

  assign out = x[2] ^ x[1];
endmodule

如何为 "Out" 编写断言，因为它是一个多时钟设计。

我已经试过了，但还是有一些错误。请帮助我修改此断言或编写另一个断言：

property p1;
  bit t;
  bit x[2:0];

  @(posedge clkA)
  (1'b1, t ^= in) |=> @(posedge clkB) (1'b1, x[0] = t) |=> @(posedge clkB) (out == x[2] ^ x[1], x[1] = x[0]) |=> @(posedge clkB) (out == x[2] ^ x[1], x[2] = x[1]);
endproperty

注意：始终阻塞和单个时钟断言，我们可以验证输出端口。但是我想通过多时钟断言来做到这一点，如果可能的话，没有任何总是阻塞。

Answer 1

免责声明：我没有测试过这个。

你试过了吗：

#1 @(posedge clkA) (1'b1, t ^= in) |-> 
#2 @(posedge clkB) (1'b1, x[0] = t) |=> 
#3 @(posedge clkB) (out == x[2] ^ x[1], x[1] = x[0]) |=>
#4 @(posedge clkB) (out == x[2] ^ x[1], x[2] = x[1]);

即在时钟切换中有重叠的含义。根据我的经验，非重叠蕴涵将导致断言不在下一个 clkB 上采样，而是跳过一个 clkB，然后在 clkB 上采样。

此外，我不太明白你为什么在整个断言中一直使用暗示。第 2 行不是第 3 行的先决条件，第 3 行和第 4 行也是如此。我阅读这篇文章的方式是断言应该从每个 clkA 开始，然后一个序列将 always 跟随。在那种情况下，下面的代码会更正确，尽管之前的代码可能仍然有效。

@(posedge clkA) 
    (1'b1, t ^= in) |-> 
@(posedge clkB) 
    (1'b1, x[0] = t) ##1 
    (1'b1, x[1] = x[0]) ##1 
    (out == x[2] ^ x[1], x[2] = x[1]);

最后，如果 clkA 比 clkB 快得多会怎样？多个断言将并行开始，并且在 clkB 的第一个 posedge 上不同意 t 的实际值。我必须承认，我对属性局部值的范围界定不清楚，但请检查这是否给您带来了麻烦。一个可能的修复方法是在属性范围之外声明变量 t。因此 t 将在 clkA 的每个 posedge 上更新为新值，并且您将有 n 断言检查相同的事情（这不是问题）。

编辑：我从第 3 行删除了 out == x[2] ^ x[1] 检查，因为 x 对于属性是本地的。因此，您无法检查此断言的其他一些实例所产生的值。

补充：如果上面的方法不起作用，或者如果启动并行断言检查同一事物似乎是一种浪费，则以下代码可能会起作用。

Edit2：将 x 放入属性并更改属性中的最后两行以将 x 更新为正确的值。

bit t;
always_ff@(posedge clkA)
     t ^= in;

property p1;
bit[2:0] x;
@(posedge clkB) 
    (1'b1, x[0] = t) |=> 
    (1'b1, x[1] = x[0]) ##0 (1'b1, x[0] = t) ##1 
    (1'b1, x[2] = x[1]) ##0 (1'b1, x[1] = x[0]) ##0 out == x[2] ^ x[1];
endproperty

最后的奖励提示：创建的触发器应该有重置。也就是说，x 和 temp 都应该在其各自的时钟域本地进行重置。根据您的选择，重置可以是同步的或异步的。这也必须添加到您的属性。另外：始终使用 always_ff 或 always_comb，切勿始终使用。

异步复位：

always_ff @ (posedge clkA or posedge arstClkA)
if(arstClkA)
    temp <= 0;
else
    temp <= temp ^ in;

Systemverilog 中的多时钟断言

Multiple Clock Assertion in Systemverilog

verilog

system-verilog

system-verilog-assertions