Spinroot
A forum for Spin users
You are not logged in.
- Topics: Active | Unanswered
Pages: 1
#1 2012-06-08 10:27:56
- feng_lei_76
- Member
- Registered: 2011-05-13
- Posts: 43
Bit Complement Operation
I met a problem with the bit complement operation.
In the simple code below, ~x should be 0 and the assertion should be true, but SPIN621 detects an error. Is this a bug?
init
{
bit x = 1;
assert( ~x == 0)
}
Offline
#2 2012-06-09 18:38:41
Re: Bit Complement Operation
Hi -- note that ~ takes the one's complement. So in an integer expression like ~x
it computes the one's complement -- turning the positive value 1 into a negative value,
which in this case will be -2. (You can check this with a little C program, printing the value.)
Offline
#3 2012-06-09 19:35:00
- feng_lei_76
- Member
- Registered: 2011-05-13
- Posts: 43
Re: Bit Complement Operation
Thank you for the answer. I confirmed your explanation with SPIN. SPIN is trickier than C in this case because the bit data type is special in SPIN. Since the smallest operand in C is a byte, pan.c acutally interprets the bit 1 as 0x01 and then performs the complement. Therefore the answer is 0xFE, namely -2. The difficult part is that given a bit variable x (==1), its complement becomes -2, out of the scope of the bit data type.
To get the value of 0 from the complement, I have to introduce another bit data type y and do the following.
bit x = 1;
bit y;
y = ~x;
Now y is 0 indeed.
BR
Offline
Pages: 1