Bidirectional constraint using the implication operator

In the following code, if a==1, then b==0. Because of bidirection, if b==0, then my understanding is that a should be 1. However, the output is different from what I would expect.

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.

Upvotes: 1

Views: 951

Answers (2)

Serge
Serge

Reputation: 12384

The implication operator a == 1 -> b == 0 is logically equivalent to (a == 0 || b == 0) (from 18.5.6).

if b == 0 then the equation is already satisfied and a can take any value, still satisfying the constraint.

if you try to simulate with a == 0, then b can take any value.

You can experiment with a == 1 then the only way to satisfy the expression is if b == 0.

Upvotes: 1

toolic
toolic

Reputation: 62236

Your results are expected.

In the IEEE Std 1800-2017, section 18.5.6 Implication, there is an example similar to yours, with 4-bit variables.

Since you declare two 1-bit variables, there are 4 combinations:

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

The c constraint in the class eliminiates one of these (a=1, b=1), leaving these 3 combinations:

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

The inline with constraint forces b=0, leaving these 2 combinations:

{0,0}, {1,0}

This means that a could either be 0 or 1, and this is what you are seeing.

Upvotes: 1

Related Questions