Systemverilog中的多时钟声明

问题描述 投票:3回答:1

这里是设计代码:

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

Note:通过始终阻塞和单个时钟断言,我们可以验证输出端口。但是我想通过多时钟声明来做到这一点,如果可能的话,始终不要阻塞。

verilog system-verilog system-verilog-assertions
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的第一个姿势上的t的实际值不一致。我必须承认我对属性本地值的作用域感到困惑,但是请检查这是否给您带来麻烦。可能的解决方法是在属性范围之外声明变量t。这样,t将在clkA的每个姿势上更新为新值,并且您将有

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;