Transcript Basics - Boolean functions

ECE 697B (667)
Spring 2006
Synthesis and Verification
of Digital Circuits
Boolean Functions
and Circuits
Slides adopted (with permission) from A. Kuehlmann, UC Berkeley 2003
1
ECE 667 - Synthesis & Verification - Lecture 0
Synthesis Flow
a multi-stage process
Specification
Logic Extraction
module example(clk,
a, b, c, d, f, g, h)
input
clk, a, b, c, d, e, f;
Technology-Independent
aoutput g, h; reg g, h;
Optimization
b
a
Technology-Dependent
Mapping
h
always
@(posedge
clk)
begin
g1
e
0
G
g = a | b;
bif (d) beging0
if (c) h = a&~h;
f
g
else h = b;
h5
G
dcend else if (f) g = c; else a^b;
g
h3
if (c) h = 1; else h ^b;
bd
H
end e
fendmodule
h
h1
H
ae
c
clk
c
d
f
clk
What is Logic Synthesis?


X
D
Y
Given: Finite-State Machine F(X,Y,Z,  , ) where:
X: Input alphabet
Y: Output alphabet
Z: Set of internal states
 : X x Z Z (next state function, Boolean)
 : X x Z Y (output function, Boolean)
Target: Circuit C(G, W) where:
• G: set of circuit components  g
{Boolean gates, flip-flops, etc}
• W: set of wires connecting G
ECE 667 - Synthesis & Verification - Lecture 0
4
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 - Lecture 0
5
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 - Lecture 0
x2
x1
6
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
ECE 667 - Synthesis & Verification - Lecture 0
x2
x1
x2
x1
7
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 - Lecture 0
8
Boolean Operations - AND, OR, COMPLEMENT
Given two Boolean functions:
f : Bn  B
g : Bn  B
• The AND operation h = f  g is defined as
h = {x | f(x)=1  g(x)=1}
• The OR operation h = f + g is defined as
h = {x | f(x)=1  g(x)=1}
• The COMPLEMENT operation h = ^f (or f’ ) is defined as
h = {x | f(x) = 0}
ECE 667 - Synthesis & Verification - Lecture 0
9
Cofactor and Quantification
Given a Boolean function:
f : Bn  B, with the input variables (x1,x2,…,xi,…,xn)
• The Positive Cofactor h = fxi is defined as
h = {x | f(x1,x2,…,1,…,xn)=1}
• The Negative Cofactor h = fxi is defined as
h = {x | f(x1,x2,…,0,…,xn)=1}
• The Existential Quantification of function h w.r.t variable xi, h = $xi f is:
h = {x | f(x1,x2,…,0,…,xn)=1 f(x1,x2,…,1,…,xn)=1}
• The Universal Quantification of function h w.r.t variable xi, h = "xi f is:
h = {x | f(x1,x2,…,0,…,xn)=1 f(x1,x2,…,1,…,xn)=1}
ECE 667 - Synthesis & Verification - Lecture 0
10
Representation 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 - Lecture 0
11
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 - Lecture 0
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
12
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 - Lecture 0
13
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 - Lecture 0
x2
x1
x2
x1
14
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 - Lecture 0
15
List of Cubes
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.
F1={ab, ac, bc} and F2={abc, abc, abc, abc}
are covers of
f = ab + ac + bc.
ECE 667 - Synthesis & Verification - Lecture 0
16
Binary Decision Diagram (BDD)
f = ab+a’c+a’bd
Graph representation of a Boolean function
- vertices represent decision nodes for variables
root
- two children represent the two subfunctions
node
f(x = 0) and f(x = 1) (cofactors)
- restrictions on ordering and reduction rules
c+bd
can make a BDD representation canonical
b
a
b
b
c
c+d
c
c
1
d
d
0
0
ECE 667 - Synthesis & Verification - Lecture 0
1
17
Boolean Circuits (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 we have in
CAD
– 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 - Lecture 0
18
Definitions – fanin, fanout, support
Definition:
A Boolean circuit 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 gate g is assigned a Boolean function fg which computes
the output of the gate in terms of its inputs.
ECE 667 - Synthesis & Verification - Lecture 0
19
Definitions – fanin, fanout, support
The fanin FI(g) of a gate g are all predecessor vertices of g:
FI(g) = {g’ | (g’,g) N}
The fanout FO(g) of a gate g are all successor vertices of g:
FO(g) = {g’ | (g,g’) N}
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 - Lecture 0
20
Example – Boolean network
8
7
1
4
6
2
I
O
9
5
3
FI(6) = {2,4}
FO(6) = {7,9}
CONE(6) = {1,2,4,6}
SUPPORT(6) = {1,2}
ECE 667 - Synthesis & Verification - Lecture 0
21
Circuit Function
• Circuit functions are defined recursively:
if gi  I
 xi
hgi  
 f gi (hg j ,..., hgk ), g j ,..., g k  FI ( gi ) otherwise
• If G is implemented using physical gates that have positive
(bounded) delays for their evaluation, the computation of hg
depends in general on those delays.
• Definition:
A circuit C is called combinational if for each input assignment of
C for t the evaluation of hg for all outputs is independent of
the internal state of C.
Proposition:
A circuit C is combinational if it is acyclic.
ECE 667 - Synthesis & Verification - Lecture 0
22
SAT and Tautology
• Tautology:
– Find an assignment to the inputs that evaluate a given vertex to “0”.
• SAT:
– Find an assignment to the inputs that evaluate a given vertex to “1”.
– Identical to Tautology on the inverted vertex
• SAT on circuits is identical to the justification part in ATPG
– First half of ATPG: justify a particular circuit vertex to “1”
– Second half of ATPG (propagate a potential change to an output)
can be easily formulated as SAT (will be covered later)
– Basic SAT algorithms:
– branch and bound algorithm as seen before
• branching on the assignments of primary inputs only (Podem
algorithm)
• branching on the assignments of all vertices (more efficient)
ECE 667 - Synthesis & Verification - Lecture 0
23
Circuit Representations
For general circuit manipulation (e.g. synthesis):
Vertices have an arbitrary number of inputs and outputs
• Vertices can represent any Boolean function stored in different
ways, such as:
–
–
–
–
other circuits (hierarchical representation)
Truth tables or cube representation (e.g. SIS system)
Boolean expressions read from a library description
BDDs (e.g BDS system)
• Data structure allow very general mechanisms for insertion and
deletion of vertices, pins (connections to vertices), and nets
– general but far too slow for Boolean reasoning
ECE 667 - Synthesis & Verification - Lecture 0
24
Circuit Representations
For efficient Boolean reasoning (e.g. a SAT engine):
• Circuits are non-canonical
– computational effort is in the “checking part” of the reasoning
engine (in contrast to BDDs)
• Vertices have fixed number of inputs (e.g. two)
• Vertex function is stored as label, well defined set of possible
function labels (e.g. OR, AND,OR)
• on-the-fly compaction of circuit structure
– allows incremental, subsequent reasoning on multiple
problems
ECE 667 - Synthesis & Verification - Lecture 0
25
Boolean Reasoning Engine
Engine application:
- traverse problem data structure and build
Boolean problem using the interface
- call SAT to make decision
Engine Interface:
void INIT()
void QUIT()
Edge VAR()
Edge AND(Edge p1,
Edge p2)
Edge NOT(Edge p1)
Edge OR(Edge p1
Edge p2)
...
int SAT(Edge p1)
ECE 667 - Synthesis & Verification - Lecture 0
External reference pointers attached
to application data structures
Engine Implementation:
...
...
...
...
26
Basic Approaches
• Boolean reasoning engines need:
– a mechanism to build a data structure that represents the
problem
– a decision procedure to decide about SAT or UNSAT
• Fundamental trade-off
– canonical data structure
• data structure uniquely represents function
• decision procedure is trivial (e.g., just pointer comparison)
• example: Reduced Ordered Binary Decision Diagrams
• Problem: Size of data structure is in general exponential
– non-canonical data structure
• systematic search for satisfying assignment
• size of data structure is linear
• Problem: decision may take an exponential amount of time
ECE 667 - Synthesis & Verification - Lecture 0
27
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 - Lecture 0
28
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 - Lecture 0
29
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 - Lecture 0
0456
0 left
0 right
next
fanout
30
Hash Table
Algorithm HASH_LOOKUP(Edge p1, Edge p2) {
index = HASH_FUNCTION(p1,p2)
p
= &hash_table[index]
while(p != NULL) {
if(p->left == p1 && p->right == p2) return p;
p = p->next;
}
return NULL;
}
Tricks:
- keep collision chain sorted by the address (or index) of p
- that reduces the search through the list by 1/2
- use memory locations (or array indices) in topological order of circuit
- that results in better cache performance
ECE 667 - Synthesis & Verification - Lecture 0
31
Basic Construction Operations
Algorithm AND(Edge p1,Edge p2){
if(p1 == const1) return p2
if(p2 == const1) return p1
if(p1 == p2)
return p1
if(p1 == ^p2)
return const0
if(p1 == const0 || p2 == const0) return const0
if(RANK(p1) > RANK(p2)) SWAP(p1,p2)
if((p = HASH_LOOKUP(p1,p2)) return p
return CREATE_AND_VERTEX(p1,p2);
}
ECE 667 - Synthesis & Verification - Lecture 0
32
Basic Construction Operations
Algorithm NOT(Edge p) {
return TOOGLE_COMPLEMENT_BIT(p)
}
Algorithm OR(Edge p1,Edge p2){
return (NOT(AND(NOT(p1),NOT(p2))))
}
ECE 667 - Synthesis & Verification - Lecture 0
33
Cofactor Operation
Algorithm POSITIVE_COFACTOR(Edge p,Edge v){
if((c = GET_COFACTOR(p)) == NULL) {
if(p == v) {
if(IS_INVERTED(v)) return const0
else
return const1
}
left = POSITIVE_COFACTOR(p->left, v)
right = POSITIVE_COFACTOR(p->right, v)
if(IS_INVERTED(p)) return NOT(AND(left,right))
else
return AND(left,right)
SET_COFACTOR(p,c);
}
return c;
}
- similar algorithm for NEGATIVE_COFACTOR
- existential and universal quantification build from AND, OR and COFACTORS
Question: What is the complexity of the circuits resulting from quantification?
ECE 667 - Synthesis & Verification - Lecture 0
34