Двунаправленное ограничение с использованием оператора импликации

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

Оператор импликации a == 1 -> b == 0 логически эквивалентен (a == 0 || b == 0) (из 18.5.6).

, если b == 0, тогда уравнение уже выполнено, и a может принимать любое значение, все еще удовлетворяя ограничению.

, если вы пытаетесь смоделировать with a == 0, тогда b может принять любое значение.

Вы можете поэкспериментировать with a == 1, тогда единственный способ удовлетворить это выражение - если b == 0.

Answer 2

Ожидаются ваши результаты.

В стандарте IEEE 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, и это то, что вы видите.