Transcript Basics - Boolean functions

ECE 667
Spring 2013
Synthesis and Verification
of Digital Circuits
Boolean Functions
and their Representations
Slides adopted (with permission) from A. Kuehlmann, UC Berkeley 2003
1
ECE 667 Synthesis & Verification - Boolean
Functions
The Boolean Space B
B = { 0,1},
n
B2 = {0,1} X {0,1} = {00, 01, 10, 11}
Karnaugh Maps:
Boolean Cubes:
B0
B1
B2
B3
B4
ECE 667 Synthesis & Verification - Boolean Functions
2
Boolean Functions
Boolean Function: f ( x ) : B n  B
B  {0,1}
x2
x  ( x1, x2 ,..., xn )  B ; xi  B
n
x1
0 1
1 0
- x1, x2 ,... are variables
- x1, x1, x2 , x2 ,... are literals
- essentially: f maps each vertex of B n to 0 or 1
Example:
f  {(( x1  0, x2  0),0),(( x1  0, x2  1),1),
(( x1  1, x2  0), 1),(( x1  1, x2  1),0)}
ECE 667 Synthesis & Verification - Boolean Functions
x2
x1
3
Boolean Functions
- The Onset of f is { x | f ( x )  1}  f 1(1)  f 1
- The Offset of f is { x | f ( x )  0}  f 1(0)  f 0
- if f 1  B n , f is the tautology. i.e. f  1
- if f 0  B n (f 1   ), f is not satisfyable, i.e. f  0
- if f ( x )  g ( x ) for all x  B n , then f and g are equivalent
- we say f instead of f 1
- literals: A literal is a variable or its negation x, x and represents a logic function
Literal x1 represents the logic function f, where f = {x| x1 = 1}
Literal x1 represents the logic function g where g = {x| x1 = 0}
Notation: x’ = x
f = x1
f = x1
x3
x3
x
ECE 667 Synthesis & Verification - Boolean Functions 1
x2
x2
x1
4
Set of Boolean Functions
• Truth Table or Function Table:
x3
x2
x1
x1x2x3
000
1
001
0
010
1
011
0
100 1
101
0
110
1
111
0
• There are 2n vertices in input space Bn
n
2
• There are 2 distinct logic functions.
– Each subset of vertices is a distinct logic function: f  Bn
ECE 667 Synthesis & Verification - Boolean Functions
5
Boolean Operations - AND, OR, COMPLEMENT
Given two Boolean functions:
f : Bn  B
g : Bn  B
•
AND operation
f  g = {x | f(x)=1  g(x)=1}
• The OR operation
f + g = {x | f(x)=1  g(x)=1}
• The COMPLEMENT operation (^f or f’ )
f’ = {x | f(x) = 0}
ECE 667 Synthesis & Verification - Boolean Functions
6
Cofactor and Quantification
Given a Boolean function:
f : Bn  B, with the input variables (x1,x2,…,xi,…,xn)
• Positive Cofactor of function f w.r.t variable xi
fxi = {x | f(x1,x2,…,1,…,xn)=1}
• Negative Cofactor of f w.r.t variable xi
fxi’ = {x | f(x1,x2,…,0,…,xn)=1}
• Existential Quantification of function f w.r.t variable xi,
$x i
f = {x | f(x1,x2,…,0,…,xn)=1 f(x1,x2,…,1,…,xn)=1}
• Universal Quantification of function f w.r.t variable xi,
"xi
f = {x | f(x1,x2,…,0,…,xn)=1 f(x1,x2,…,1,…,xn)=1}
ECE 667 Synthesis & Verification - Boolean Functions
7
Representations of Boolean Functions
• We need representations for Boolean Functions for two
reasons:
– to represent and manipulate the actual circuit we are “synthesizing”
– as mechanism to do efficient Boolean reasoning
• Forms to represent Boolean Functions
–
–
–
–
–
–
Truth table
List of cubes: Sum of Products, Disjunctive Normal Form (DNF)
List of conjuncts: Product of Sums, Conjunctive Normal Form (CNF)
Boolean formula
Binary Decision Tree, Binary Decision Diagram
Circuit (network of Boolean primitives)
• Canonicity – which forms are canonical?
ECE 667 Synthesis & Verification - Boolean Functions
8
Truth Table
• Truth table (Function Table):
The truth table of a function f : Bn  B is a tabulation of abcd
0 0000
its values at each of the 2n vertices of Bn. (all mintems) 1 0001
2 0010
Example: f = a’b’c’d + a’b’cd + a’bc’d +
ab’c’d + ab’cd + abc’d +
abcd’ + abcd
(Notation for complement: a’ = a )
The truth table representation is
- intractable for large n
- canonical
Canonical means that if two functions are the
same, then the canonical representations of each
are isomorphic (identical).
ECE 667 Synthesis & Verification - Boolean Functions
f
3
4
5
6
0011
0100
0101
0110
0
1
0
1
0
1
0
7
8
9
10
11
12
13
14
0111
1000
1001
1010
1011
1100
1101
1110
0
0
1
0
1
0
1
1
15 1111 1
9
Boolean Formula
• A Boolean formula is defined as an expression with
the following syntax:
‘(‘ formula ‘)’
formula ::=
|
|
|
|
<variable>
formula “+” formula
formula “” formula
^ formula
(OR operator)
(AND operator)
(complement)
Example:
f = (x1x2) + (x3) + ^^(x4  (^x1))
typically the “” is omitted and the ‘(‘ and ‘^’ are simply reduced by
priority, e.g.
f = x1x2 + x3 + x4^x1
ECE 667 Synthesis & Verification - Boolean Functions
10
Cubes
• A cube is defined as the product (AND) of a set of
literal functions (“conjunction” of literals).
Example:
C = x1x’2x3
represents the following function
f = (x1=1)(x2=0)(x3=1)
c = x1
f = x1x2
x3
f = x1x2x3
x3
x3
x2
x1
ECE 667 Synthesis & Verification - Boolean Functions
x2
x1
x2
x1
11
Cubes
• If C  f, C a cube, then C is an implicant of f.
• If C  Bn, and C has k literals, then |C| covers 2n-k
vertices.
Example:
C = xy  B3
k = 2 , n = 3 =>
C = {100, 101}
|C| = 2 = 23-2.
• In an n-dimensional Boolean space Bn, an implicant
with n literals is a minterm.
ECE 667 Synthesis & Verification - Boolean Functions
12
List of Cubes - Cover
Sum of Products (SOP)
• A function can be represented by a sum of cubes (products):
f = ab + ac + bc
Since each cube is a product of literals, this is a “sum of products”
(SOP) representation
• A SOP can be thought of as a set of cubes F
F = {ab, ac, bc}
• A set of cubes that represents f is called a cover of f.
Sets:
F1={ab, ac, bc} and F2={abc, a’bc, ab’c, abc’}
are some of possible covers of Boolean function
f = ab + ac + bc.
ECE 667 Synthesis & Verification - Boolean Functions
13
Binary Decision Diagram (BDD)
f = ab+a’c+a’bd
Graph representation of a Boolean function
- vertices represent decision nodes for variables
- two children represent the two subfunctions
f(x = 0) and f(x = 1) (cofactors)
- restrictions on ordering and reduction rules
c+bd
can make a BDD representation canonical
- function is evaluated as sum of paths from
c
root to constant node 1
c
- paths form disjoint cubes.
1
0
root
node
b
c+d
b
b
c
d
d
0
ECE 667 Synthesis & Verification - Boolean Functions
a
1
14
Boolean Networks
•
•
•
Used for two main purposes
– as representation for Boolean reasoning engine
– as target structure for logic implementation which gets restructured in
a series of logic synthesis steps until result is acceptable
Efficient representation for most Boolean problems
– memory complexity is same as the size of circuits we are actually
building
Close to input representation and output representation in logic synthesis
ECE 667 Synthesis & Verification - Boolean Functions
15
Definitions – Boolean Network
Definition:
A Boolean network is a directed graph C(G,N) where G are the
gates and N GG is the set of directed edges (nets)
connecting the gates.
Some of the vertices are designated:
Inputs:
I G
Outputs:
O G, I O = 
Each node g is assigned a Boolean function fg which computes
the output of the gate in terms of its inputs.
ECE 667 Synthesis & Verification - Boolean Functions
16
Definitions – fanin, fanout, support
• The (immediate) fanin FI(g) of a gate g are all predecessor vertices of g:
FI(g) = {g’ | (g’,g) N}
• The transitive fanin FIT (g) is defined as follows:
if a FI(b) and b FI(c) then a FIT (c)
• The fanout FO(g) of a gate g are all successor vertices of g:
FO(g) = {g’ | (g,g’) N}
The transitive fanout is defined similarly
The cone CONE(g) of a gate g is the transitive fanin of g and g itself.
The support SUPPORT(g) of a gate g are all inputs in its cone:
SUPPORT(g) = CONE(g) I
ECE 667 Synthesis & Verification - Boolean Functions
17
Example – Boolean Network
8
7
1
4
6
2
I
5
O
9
3
Nodes = logic functions of arbitrary complexity
ECE 667 Synthesis & Verification - Boolean Functions
FI(6) = {2,4}
FO(6) = {7,9}
CONE(6) = {1,2,4,6}
SUPPORT(6) = {1,2}
18
Boolean Network Representations
• Vertices can have arbitrary number of inputs and outputs
– typically single-output functions are used
• Vertices can represent any Boolean function stored in different
ways, such as:
–
–
–
–
other circuits (hierarchical representation)
truth tables or cube representation
Boolean expressions read from a library description
BDDs, AIGs, etc.
• Data structure allow very general mechanisms for insertion and
deletion of vertices, pins (connections to vertices), and nets
ECE 667 Synthesis & Verification - Boolean Functions
19
AND-INVERTER Circuits
• Base data structure uses two-input AND function for vertices
and INVERTER attributes at the edges (individual bit)
– use De’Morgan’s law to convert OR operation etc.
• Hash table to identify and reuse structurally isomorphic circuits
f
f
g
g
Means complement
ECE 667 Synthesis & Verification - Boolean Functions
20
Data Representation
• Vertex:
– pointers (integer indices) to left and right child and fanout
vertices
– collision chain pointer
– other data
• Edge:
– pointer or index into array
– one bit to represent inversion
• Global hash table holds each vertex to identify isomorphic
structures
• Garbage collection to regularly free un-referenced vertices
ECE 667 Synthesis & Verification - Boolean Functions
21
Data Representation
Hash Table
one
6423
….
8456
….
Constant
One Vertex
zero
1345
….
0456
0 left
1 right
next
fanout
...
0455
0456
0457
...
7463
….
hash value
complement bits
left pointer
right pointer
next in collision chain
array of fanout pointers
ECE 667 Synthesis & Verification - Boolean Functions
0456
0 left
0 right
next
fanout
22