verilog - 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

注意:通过始终 block 和单个时钟断言，我们可以验证输出端口。但如果可能的话，我想通过多时钟断言来完成此操作，而不需要任何始终阻止。

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 上开始，然后总是遵循一个序列。在这种情况下，以下内容会更正确，尽管之前的代码可能仍然有效。

@(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 第一个 posege 上 t 的实际值存在分歧。我必须承认，我对属性本地值的范围很模糊，但请检查这是否会给您带来麻烦。可能的修复方法是在属性范围之外声明变量 t。因此，t 将在 clkA 的每个 pedge 上更新为新值，并且您将有 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 都应该在其各自的时钟域本地进行重置。重置可以是同步的，也可以是异步的，由您选择。这也必须添加到您的属性(property)中。另外:始终使用always_ff或always_comb，切勿使用always。

异步重置:

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