3

这是设计代码：

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

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

4

1 回答 1

3

免责声明：我没有对此进行测试。

你有没有尝试过：

#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 的第一个 posedge 上不同意 t 的实际值。我必须承认我对属性本地值的范围模糊不清，但请检查这是否会给您带来麻烦。一个可能的解决方法可能是在属性范围之外声明变量 t。因此 t 将在 clkA 的每个 posedge 上更新为新值，并且您将有n 个断言检查相同的事情（这不是问题）。

编辑：我out == x[2] ^ x[1]从第 3 行删除了检查，因为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。

异步复位：

always_ff @ (posedge clkA or posedge arstClkA)
if(arstClkA)
    temp <= 0;
else
    temp <= temp ^ in;
于 2015-10-27T09:38:01.670 回答