使用蕴涵运算符的双向约束

Question

在下面的代码中，如果a == 1则b == 0，因为双向，如果b == 0则我的理解是a应该为1。但是输出似乎有所不同。

class ex_sv;

rand bit a;
rand bit b;

constraint c {
   (a==1) -> (b==0);
 }
endclass

module ex_mod;

ex_sv h = new();

initial begin
for( int i = 0; i<10; i++ ) begin
 void'(h.randomize() with {b==0;});
 $display("ITER : %0d a = %0d b = %0d",i, h.a, h.b);
end
end

endmodule

xcelium> run
ITER : 0 a = 0 b = 0
ITER : 1 a = 0 b = 0
ITER : 2 a = 1 b = 0
ITER : 3 a = 0 b = 0
ITER : 4 a = 0 b = 0
ITER : 5 a = 1 b = 0
ITER : 6 a = 1 b = 0
ITER : 7 a = 0 b = 0
ITER : 8 a = 1 b = 0
ITER : 9 a = 1 b = 0
xmsim: *W,RNQUIE: Simulation is complete.

Answer 1

期待您的结果。

在IEEE Std 1800-2017中，第18.5.6节含义，有一个类似于您的示例，带有4位变量。

由于您声明了两个1位变量，所以有4种组合：

{0,0}, {0,1}, {1,0}, {1,1}

该类中的c约束消除了其中一个（a = 1，b = 1），离开这3种组合：

{0,0}, {0,1}, {1,0}

内联with约束力b = 0，剩下这2种组合：

{0,0}, {1,0}

这意味着a可以是0或1，这就是您所看到的。

Answer 2

隐含运算符a == 1 -> b == 0在逻辑上等效于(a == 0 || b == 0)（从18.5.6开始）。

如果b == 0则等式已经满足，并且a可以取任何值，但仍满足约束。

如果尝试模拟with a == 0，则b可以取任何值。

您可以尝试with a == 1，那么满足表达式的唯一方法是b == 0。