这里是设计代码:
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:通过始终阻塞和单个时钟断言,我们可以验证输出端口。但是我想通过多时钟声明来做到这一点,如果可能的话,始终不要阻塞。
免责声明:我尚未对此进行测试。
您是否尝试过:
#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的每个姿势上更新为新值,并且您将有个断言检查同一件事(这不是问题)。 编辑:我从第3行中删除了n
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;