Implication operator constraint is not bi directional

[Raj Pednekar]

https://www.edaplayground.com/x/j7K7

My code is here wanted to test some basic randomizations. (Constraints are bi directional)

I see that even with 

constraint a_b { (a == 0) -> b == 0; }

One of the solutions/o/p I am getting on printing is 

Value of a = 1, b = 0

Can it be explained.?

[EDA Playground]

I don't think implication constraints are bi-directional. I think you constraint means

    "If a is 0, then b should be 0."

It does not mean "if b is 0 then a should be 0".

[Raj Pednekar]

Implication operators constraints are bi-directional.

"If a is 0, then b will be 0. and if b=0 a will be 0"

I went through the SV LRM it mentions it as well.

on pg 164 for LRM 22nov 2005

[EDA Playground]

I' not sure I understand what is says in the LRM, because I don't think 

  constraint a_b { (a == 0) -> b == 0; }

constrains a to be 0 if b is 0. If I add this constraint, too:

  constraint b_a { (b == 0) -> a == 0; }

then 

Value of a = 1, b = 0

never occurs. I will ask my colleagues to see if they can shed any light on it. But, I think you need both constraints.

[EDA Playground]

So, a colleague replied to say this:

In maths:

• A ⇒ B is bidirectional, in the sense that it is formally equivalent to !B ⇒ !A
• A ⇒ B is not bidirectional, in the sense that it is NOT equivalent to B ⇒ A

In other words, if "A is true then B must be true" is bidirectional because if B is false then A must be false.  But, you cannot also say that "if B is true then A must be true".  And the same goes for SystemVerilog syntax such as

    constraint a_b { (a == 0) -> b == 0; }

We can say 

• if a is 0 then b is 0 and
• if b is not 0 then a is not 0  (that is what is meant by "bidirectional" in the LRM)

but we cannot say

• if b is 0 then a is 0

[Raj Pednekar]

Oh. I cleared a major misunderstanding. Thanks