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

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}

类中的CCD_ 1约束消除了这些(a＝1、b＝1(中的一个，留下这3个组合：

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

内联with约束强制b=0，留下以下两个组合：

{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可以取任何值。

您可以对c0进行实验，那么满足表达式的唯一方法是如果b == 0。