Transcript Formal Processor Verification

Number Systems
Number of symbols = base of the system

Most intuitive -- base 10 (decimal system)
 counting on fingertips
 symbols -- 0 1 2 3 4 5 6 7 8 9

Computers use base 2 (binary system)
 only two symbols - 0 / 1
 Many physical reasons for choosing

Other useful bases
 8 - octal
 16 - hexadecimal
–1–
52011
Representing a number in base B
General expression :
A number U3 U2 U1 U0 in base B is effectively
U 3 x B 3 + U 2 x B 2 + U 1 x B1 + U 0 x B 0
Examples :
234 in base 10 is
2 x 102 + 3 x 101 + 4 x 100
1011 in base 2 is
1 x 22 + 0 x 22 + 1 x 21 + 1 x 20 = 1 x 101 + 1 x 100 in base 10
–2–
52011
Why Don’t Computers Use Base 10?
Implementing Electronically



Hard to store
Hard to transmit
Messy to implement digital logic functions
Binary Electronic Implementation



Easy to store with bistable elements
Reliably transmitted on noisy and inaccurate wires
Straightforward implementation of arithmetic functions
0
1
0
3.3V
2.8V
0.5V
0.0V
–3–
52011
Octal and hexadecimal
Octal uses 0-7 for representing numbers
Hexadecimal uses 0-9, a, b, c, d, e and f as digits
a = decimal 10, b=decimal 11 and so on
They are useful because
translation from binary is easy
Consider 101100110101
rewrite as 101 100 110 101 and you get 5465 in octal
rewrite as 1011 0011 0101 and you get b35 in hex
Much more readable in octal and hex than in binary
Also much easier to calculate equivalent decimal value
It will really pay to learn to interpret hex numbers in this course
–4–
52011
Encoding Byte Values
Byte = 8 bits



Binary 000000002
Decimal:
010
Hexadecimal
0016
to
to
to
111111112
25510
FF16
 Base 16 number representation
 Use characters ‘0’ to ‘9’ and ‘A’ to ‘F’
 Write FA1D37B16 in C as 0xFA1D37B
o Or 0xfa1d37b
–5–
0
1
2
3
4
5
6
7
8
9
A
B
C
D
E
F
0
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
0000
0001
0010
0011
0100
0101
0110
0111
1000
1001
1010
1011
1100
1101
1110
1111
52011
Machine Words
Machine Has “Word Size”

Nominal size of integer-valued data
 Including addresses

Most current machines are 32 bits (4 bytes) or 64 bits
 32 bits Limits addresses to 4GB
 Becoming too small for memory-intensive applications

High-end systems are 64 bits (8 bytes)
 Potentially address  1.8 X 1019 bytes

Machines support multiple data formats
 Fractions or multiples of word size
 Always integral number of bytes
–6–
52011
Data Representations
Sizes of C Objects (in Bytes)

C Data Type Compaq Alpha
 int
 long int
 char
 short
 float
 double
 long double
 char *
4
8
1
2
4
8
8
8
Typical 32-bit
Intel IA32
4
4
1
2
4
8
8
4
4
4
1
2
4
8
10/12
4
o Or any other pointer
–7–
52011
Byte Ordering
How should bytes within multi-byte word be
ordered in memory?
Conventions

Sun’s, Mac’s are “Big Endian” machines
 Least significant byte has highest address

Alphas, PC’s are “Little Endian” machines
 Least significant byte has lowest address
–8–
52011
Byte Ordering Example
Big Endian

Least significant byte has highest address
Little Endian

Least significant byte has lowest address
Example


Variable x has 4-byte representation 0x01234567
Address given by &x is 0x100
Big Endian
0x100 0x101 0x102 0x103
01
Little Endian
45
67
0x100 0x101 0x102 0x103
67
–9–
23
45
23
01
52011
Reading Byte-Reversed Listings
Disassembly


Text representation of binary machine code
Generated by program that reads the machine code
Example Fragment
Address
8048365:
8048366:
804836c:
Instruction Code
5b
81 c3 ab 12 00 00
83 bb 28 00 00 00 00
Assembly Rendition
pop
%ebx
add
$0x12ab,%ebx
cmpl
$0x0,0x28(%ebx)
Deciphering Numbers




– 10 –
Value:
Pad to 4 bytes:
Split into bytes:
Reverse:
0x12ab
0x000012ab
00 00 12 ab
ab 12 00 00
52011
Representing Integers
int A = 15213;
int B = -15213;
long int C = 15213;
Linux/Alpha A
6D
3B
00
00
Linux/Alpha B
93
C4
FF
FF
– 11 –
Decimal: 15213
Binary:
0011 1011 0110 1101
3
Hex:
B
6
D
Sun A
Linux C
Alpha C
Sun C
00
00
3B
6D
6D
3B
00
00
6D
3B
00
00
00
00
00
00
00
00
3B
6D
Sun B
FF
FF
C4
93
Two’s complement representation
(Covered later)
52011
Alpha P
Representing Pointers
int B = -15213;
int *P = &B;
Alpha Address
1
Hex:
Binary:
Sun P
EF
FF
FB
2C
F
F
F
F
F
C
A
0
0001 1111 1111 1111 1111 1111 1100 1010 0000
A0
FC
FF
FF
01
00
00
00
Sun Address
Hex:
Binary:
E
F
F
F
F
B
2
C
1110 1111 1111 1111 1111 1011 0010 1100
Linux P
D4
F8
FF
BF
Linux Address
Hex:
Binary:
B
F
F
F
F
8
D
4
1011 1111 1111 1111 1111 1000 1101 0100
Different compilers & machines assign different locations to objects
– 12 –
52011
Representing Floats
Float F = 15213.0;
Linux/Alpha F
00
B4
6D
46
Sun F
46
6D
B4
00
IEEE Single Precision Floating Point Representation
Hex:
Binary:
15213:
4
6
6
D
B
4
0
0
0100 0110 0110 1101 1011 0100 0000 0000
1110 1101 1011 01
Not same as integer representation, but consistent across machines
Can see some relation to integer representation, but not obvious
– 13 –
52011
Representing Strings
char S[6] = "15213";
Strings in C


Represented by array of characters
Each character encoded in ASCII format
 Standard 7-bit encoding of character set
 Other encodings exist, but uncommon
 Character “0” has code 0x30
o Digit i has code 0x30+i

String should be null-terminated
Linux/Alpha S Sun S
31
35
32
31
33
00
31
35
32
31
33
00
 Final character = 0
Compatibility

Byte ordering not an issue
 Data are single byte quantities

– 14 –
Text files generally platform independent
52011
 Except for different conventions of line termination character(s)!
Boolean Algebra
Developed by George Boole in 19th Century

Algebraic representation of logic
 Encode “True” as 1 and “False” as 0
And

Not

Or
A&B = 1 when both A=1 and
B=1
& 0 1
0 0 0
1 0 1
~A = 1 when A=0
~
0 1
1 0
– 15 –

A|B = 1 when either A=1 or
B=1
| 0 1
0 0 1
1 1 1
Exclusive-Or (Xor)

A^B = 1 when either A=1 or
B=1, but not both
^ 0 1
0 0 1
1 1 0
52011
Application of Boolean Algebra
Applied to Digital Systems by Claude Shannon


1937 MIT Master’s Thesis
Reason about networks of relay switches
 Encode closed switch as 1, open switch as 0
A&~B
A
Connection when
~B
A&~B | ~A&B
~A
B
~A&B
– 16 –
= A^B
52011
Algebra
Integer Arithmetic





Addition is “sum” operation
Multiplication is “product” operation
– is additive inverse
0 is identity for sum
1 is identity for product
Boolean Algebra






– 17 –
{0,1}, |, &, ~, 0, 1 forms a “Boolean algebra”
Or is “sum” operation
And is “product” operation
~ is “complement” operation (not additive inverse)
0 is identity for sum
1 is identity for product
52011
Boolean Algebra  Integer Ring






Commutativity
A|B = B|A
A&B = B&A
Associativity
(A | B) | C = A | (B | C)
(A & B) & C = A & (B & C)
Product distributes over sum
A & (B | C) = (A & B) | (A & C)
Sum and product identities
A|0 = A
A&1 = A
Zero is product annihilator
A&0 = 0
Cancellation of negation
~ (~ A) = A
– 18 –
A+B = B+A
A*B = B*A
(A + B) + C = A + (B + C)
(A * B) * C = A * (B * C)
A * (B + C) = A * B + B * C
A+0 = A
A*1 =A
A*0 = 0
– (– A) = A
52011
Boolean Algebra  Integer Ring


Boolean: Sum distributes over product
A | (B & C) = (A | B) & (A | C) A + (B * C)  (A + B) * (B + C)
Boolean: Idempotency
A|A = A
A +AA
 “A is true” or “A is true” = “A is true”

A&A = A
Boolean: Absorption
A | (A & B) = A
A *AA
A + (A * B)  A
 “A is true” or “A is true and B is true” = “A is true”

A & (A | B) = A
Boolean: Laws of Complements
A | ~A = 1
A * (A + B)  A
A + –A  1
 “A is true” or “A is false”

Ring: Every element has additive inverse
A | ~A  0
A + –A = 0
– 19 –
52011
Boolean Ring



Properties of & and ^
{0,1}, ^, &, , 0, 1
Identical to integers mod 2
 is identity operation:  (A) = A
A^A=0
Property









– 20 –
Commutative sum
Commutative product
Associative sum
Associative product
Prod. over sum
0 is sum identity
1 is prod. identity
0 is product annihilator
Additive inverse
Boolean Ring
A^B = B^A
A&B = B&A
(A ^ B) ^ C = A ^ (B ^ C)
(A & B) & C = A & (B & C)
A & (B ^ C) = (A & B) ^ (B & C)
A^0 = A
A&1 = A
A&0=0
A^A = 0
52011
Relations Between Operations
DeMorgan’s Laws

Express & in terms of |, and vice-versa
 A & B = ~(~A | ~B)
o A and B are true if and only if neither A nor B is false
 A | B = ~(~A & ~B)
o A or B are true if and only if A and B are not both false
Exclusive-Or using Inclusive Or
 A ^ B = (~A & B) | (A & ~B)
o Exactly one of A and B is true
 A ^ B = (A | B) & ~(A & B)
o Either A is true, or B is true, but not both
– 21 –
52011
General Boolean Algebras
Operate on Bit Vectors

Operations applied bitwise
01101001
& 01010101
01000001
01000001
01101001
| 01010101
01111101
01111101
01101001
^ 01010101
00111100
00111100
~ 01010101
10101010
10101010
All of the Properties of Boolean Algebra Apply
– 22 –
52011
Bit-Level Operations in C
Operations &, |, ~, ^ Available in C

Apply to any “integral” data type
 long, int, short, char


View arguments as bit vectors
Arguments applied bit-wise
Examples (Char data type)

~0x41 -->
~010000012

~0x00 -->
~000000002

0x69 & 0x55
0xBE
--> 101111102
0xFF
--> 111111112
-->
0x41
011010012 & 010101012 --> 010000012

0x69 | 0x55
-->
0x7D
011010012 | 010101012 --> 011111012
– 23 –
52011
Contrast: Logic Operations in C
Contrast to Logical Operators

&&, ||, !




View 0 as “False”
Anything nonzero as “True”
Always return 0 or 1
Early termination
Examples (char data type)






– 24 –
!0x41 -->
!0x00 -->
!!0x41 -->
0x00
0x01
0x01
0x69 && 0x55 --> 0x01
0x69 || 0x55 --> 0x01
p && *p (avoids null pointer access)
52011
Shift Operations
Left Shift:

x << y
Shift bit-vector x left y positions
 Throw away extra bits on left
 Fill with 0’s on right
Right Shift: x >> y

Shift bit-vector x right y
positions
 Throw away extra bits on right

Logical shift
 Fill with 0’s on left

Arithmetic shift
 Replicate most significant bit on
Argument x 01100010
<< 3
00010000
Log. >> 2
00011000
Arith. >> 2 00011000
Argument x 10100010
<< 3
00010000
Log. >> 2
00101000
Arith. >> 2 11101000
right
 Useful with two’s complement
integer representation
– 25 –
52011
Cool Stuff with Xor


void funny(int *x, int *y)
{
*x = *x ^ *y;
/* #1 */
*y = *x ^ *y;
/* #2 */
*x = *x ^ *y;
/* #3 */
}
Bitwise Xor is form of
addition
With extra property
that every value is its
own additive inverse
A^A=0
– 26 –
*x
*y
Begin
A
B
1
A^B
B
2
A^B
(A^B)^B = A
3
(A^B)^A = B
A
End
B
A
52011
Storing negative integers
sign-magnitude





of n bits in the word, the most significant bit is sign
1 indicates negative number, 0 a positive number
remaining n-1 bits determine the magnitude
0 has two representations
The range of valid values is -(2(n-1)-1) to (2(n-1)-1)
 Examples
o 8 bit words can represent -127 to +127
o 16 bit words can represent -32767 to +32767

Advantages
 Very straightforward
 Simple to understand

Disadvantage
 different machinery for addition and subtraction
 multiple representations of zero.
– 27 –
52011
One’s complement





The most significant bit is effectively sign bit
The range of numbers the same as signed magnitude
Positive numbers stored as such
Negative numbers are bit-wise inverted
Example
 4 bit storage – range -7 to +7
o -7 = 1000, +7 = 0111, +3 = 0011, -4 = 1011
 8 bit storage – range = -127 t0 128
 Zero has two representations :
o 0000 0000
o 1111 1111
 Hardly ever used for actual storage
 Useful for understanding 2’s compliment and some other
operations
– 28 –
52011
Two’s Complement
Unsigned
B2U(X) 
w1
 xi 2
Two’s Complement
i
B2T(X)   xw1 2
i0
w1

w2
 xi 2 i
i0
short int x = 15213;
short int y = -15213;

Sign
Bit
C short 2 bytes long
x
y
Decimal
15213
-15213
Hex
3B 6D
C4 93
Binary
00111011 01101101
11000100 10010011
Sign Bit

For 2’s complement, most significant bit indicates sign
 0 for nonnegative
 1 for negative
– 29 –
52011
Two’s compliment is effectively one’s
compliment with a “1” added to it.

It is a number’s additive inverse
 Number added to its own two’s compliment results in zero


Same circuitry can do arithmetic operations for positive and
negative numbers
The range is (-2n-1) to (2n-1-1)
Example : 13 + (-6)
13 in 4 bit binary is 1101
6 is 0110
It’s one’s complement is 1001
Two’s complement is 1010
Add 1101 and 1010 in 4 bits, ignoring the carry
The answer is 0111, with carry of 1, which in decimal is 7
– 30 –
52011
Power-of-2 Multiply with Shift
Operation

u << k gives u * 2k

Both signed and unsigned
Operands: w bits
True Product: w+k bits
*
u · 2k
Discard k bits: w bits
u
k
• • •
2k
0 ••• 0 1 0 ••• 0 0
• • •
UMultw(u , 2k)
•••
0 ••• 0 0
0 ••• 0 0
TMultw(u , 2k)
Examples

u << 3
==
u << 5 - u << 3 ==

Most machines shift and add much faster than multiply

– 31 –
u * 8
u * 24
52011
Unsigned Power-of-2 Divide with
Shift
Quotient of Unsigned by Power of 2

u >> k gives  u / 2k 

Uses logical shift
k
u
Operands:
Division:
Result:
x
x >> 1
x >> 4
x >> 8
– 32 –
/
2k
•••
•••
0 ••• 0 1 0 ••• 0 0
u / 2k
0 •••
•••
 u / 2k 
0 •••
•••
Division
15213
7606.5
950.8125
59.4257813
Binary Point
Computed
15213
7606
950
59
Hex
3B 6D
1D B6
03 B6
00 3B
.
•••
Binary
00111011 01101101
00011101 10110110
00000011 10110110
00000000 00111011
52011
Signed Power-of-2 Divide with Shift
Quotient of Signed by Power of 2

x >> k gives  x / 2k 

Uses arithmetic shift
Rounds wrong direction when u k< 0

x
Operands:
/
x / 2k
Division:
Result:
y
y >> 1
y >> 4
y >> 8
– 33 –
2k
RoundDown(x / 2k)
Division
-15213
-7606.5
-950.8125
-59.4257813
•••
•••
Binary Point
0 ••• 0 1 0 ••• 0 0
0 •••
•••
0 •••
•••
Computed
-15213
-7607
-951
-60
Hex
C4 93
E2 49
FC 49
FF C4
.
•••
Binary
11000100 10010011
11100010 01001001
11111100 01001001
11111111 11000100
52011
Correct Power-of-2 Divide
Quotient of Negative Number by Power of 2


Want  x / 2k  (Round Toward 0)
Compute as  (x+2k-1)/ 2k 
 In C: (x + (1<<k)-1) >> k
 Biases dividend toward 0
k
Case
1: No rounding
u
Dividend:
+2k +–1
1
/
2k
 u / 2k 
0 ••• 0 0
0 ••• 0 0 1 ••• 1 1
1
Divisor:
•••
•••
1 ••• 1 1
Binary Point
0 ••• 0 1 0 ••• 0 0
0 ••• 1 1 1
1
•••
. 1 ••• 1 1
Biasing has no effect
– 34 –
52011
Correct Power-of-2 Divide (Cont.)
Case 2: Rounding
k
x
Dividend:
+2k +–1
1
•••
•••
0 ••• 0 0 1 ••• 1 1
1
•••
•••
Incremented by 1
Divisor:
/
2k
 x / 2k 
0 ••• 0 1 0 ••• 0 0
0 ••• 1 1 1
1
Biasing adds 1 to final result
– 35 –
Binary Point
•••
.
•••
Incremented by 1
52011
Fractional Binary Numbers
2i
2i–1
4
2
1
•••
bi bi–1
•••
b2 b1 b0 . b–1 b–2 b–3
1/2
1/4
1/8
•••
b–j
•••
2–j
Representation


Bits to right of “binary point” represent fractional powers of 2
i
Represents rational number:
k
 bk 2
k  j
– 36 –
52011
Frac. Binary Number Examples
Value
5-3/4
2-7/8
63/64
Representation
101.112
10.1112
0.1111112
Observations



Divide by 2 by shifting right
Multiply by 2 by shifting left
Numbers of form 0.111111…2 just below 1.0
1/2 + 1/4 + 1/8 + … + 1/2i + …  1.0
– 37 –
52011
Representable Numbers
Limitation


Can only exactly represent numbers of the form x/2k
Other numbers have repeating bit representations
Value
1/3
1/5
1/10
– 38 –
Representation
0.0101010101[01]…2
0.001100110011[0011]…2
0.0001100110011[0011]…2
52011