systemverilog条件约束求助

systemverilog验证这本书145页讲到约束关系操作符->
我的问题是:这个操作符究竟是什么意思?
操作符两边的约束究竟是if.else关系还是互斥关系?
因为下面两个例子我觉得矛盾:
其中147页例6.25中，
rand bit x;
rand bit [1:0]y;
constraint c_xy{(x==0)–>y==0;}
运行结果中x=y=0的概率是1/2；
这说明，不是互斥关系，但好像也不是if.else关系?
但146页又说是双向约束关系，所以就很疑惑
小弟盼复，谢谢！

->蕴含操作符是双向的，表示->两边的操作同时进行，一般与slove before合起来用。
上面的例子等价于
如果x=0，那么y一定为0；
x=1那么y可能是0或1。
要想概率为50%，必须使用solve x before y

slove...before 书中不太推荐，->都说了和case的效果类似。

->是说前者成立后者必须成立。