Reputation: 73
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
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
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