Transcript SOP representation

ECE 697B (667)
Fall 2004
Synthesis and Verification
of Digital Systems
Boolean Functions
SOP Representation
Slides adopted (with permission) from A. Kuehlmann, UC Berkeley 2003
ECE 667 - Synthesis & Verification - Lecture 9b
1
Representation of Boolean Functions
• Sum of Products:
• 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’,ab’c,ab’c’,bc}
are covers of
f = ab + ac + bc.
ECE 667 - Synthesis & Verification - Lecture 9b
2
SOP
ac
bc
= onset minterm
ab
c
b
a
Note that each onset minterm
is “covered” by at least one of
the cubes!
None of the offset minterms is
covered
• Covers (SOP’s) can efficiently represent many practical logic
functions (i.e. for many, there exist small covers).
• Two-level minimization seeks the minimum size cover (least
number of cubes)
ECE 667 - Synthesis & Verification - Lecture 9b
3
Irredundant Cubes
• Let F = {c1, c2, …, ck} be a cover for f, i.e.
f = ik=1 ci
A cube ci F is irredundant if F\{ci}  f
Example: f = ab + ac + bc
ac
bc
bc
Not covered
ab
c
ac
b
a
ECE 667 - Synthesis & Verification - Lecture 9b
F\{ab}  f
4
Prime Cubes
• A literal j of cube ci  F ( =f ) is prime if
(F \ {ci })  {c”i }  f
where c”i is ci with literal j of ci deleted.
• A cube of F is prime if all its literals are prime.
F=ac + bc + a = F \{ci }  {c”i }
Example
f = ab + ac + bc
ci = ab; c”i = a (literal b deleted)
F \ {ci }  {c”i } = a + ac + bc c
Not equal to f since
offset vertex is covered
ECE 667 - Synthesis & Verification - Lecture 9b
bc
ac
a
b
a
5
Definitions - Prime, Irredundant, Essential
• Definition 1 A cube is prime if it is not contained in any other cube.
A cover is prime if all its cubes are prime.
• Definition 2 A cover is irredundant if all its cubes are irredundant.
• Definition 3 A prime of f is essential (essential prime) if there is a
minterm (essential vertex) in that prime that is in no other prime.
• Definition 4 Two cubes are orthogonal if they do not have any
minterm in common
– E.g.
c1= ab
c2 = b’c are orthogonal
c1= ab’
c2 = b’c are not orthogonal
ECE 667 - Synthesis & Verification - Lecture 9b
6
Prime and Irredundant Covers
Example:
f = abc + b’d + c’d is prime and irredundant.
abc is essential since abcd’abc, but not in b’d or c’d or ad
abc
abcd’
abcd
bd
c
b
a
d
cd
Why is abcd not an essential vertex of abc?
What is an essential vertex of abc?
What other cube is essential? What prime is not essential?
ECE 667 - Synthesis & Verification - Lecture 9b
7
PLAs - Multiple Output Functions
• A PLA is a function f : Bn  Bm represented in SOP form:
n=3, m=3
a
a
b
b
c
Personality Matrix
c
abc
10-11
0-0
111
00f1
ECE 667 - Synthesis & Verification - Lecture 9b
f2
f1f2f3
1 - 1 - - 1 - 1 1
- - 1
f3
8
PLAs (cont.)
• Each distinct cube appears just once in the AND-plane, and can
be shared by (multiple) outputs in the OR-plane, e.g., cube
(abc).
• Extensions from single output to multiple output minimization
theory are straightforward.
• Multi-level logic can be viewed mathematically as a collection of
single output functions.
ECE 667 - Synthesis & Verification - Lecture 9b
9
Shannon (Boole) Cofactors
Let f : Bn  B be a Boolean function, and x= (x1, x2, …, xn) the
variables in the support of f.
The cofactor fa of f w.r.t literal a=xi or a=x’i is:
fxi (x1, x2, …, xn) = f (x1, …, xi-1, 1, xi+1,…, xn)
fx’i (x1, x2, …, xn) = f (x1, …, xi-1, 0, xi+1,…, xn)
The computation of the cofactor is a fundamental operation in
Boolean reasoning !
Example:
f = abc + abc
fa = bc
c
c
b
a
ECE 667 - Synthesis & Verification - Lecture 9b
b
a
10
Generalized Cofactor
• The generalized cofactor fC of f by a cube C is f with the fixed
values indicated by the literals of C,
e.g. if C=xi x’j, then xi =1, and xj =0.
• if C= x1 x’4 x6
fC is just the function f restricted to the subspace
where x1 =x6 =1 and x4 =0.
• As a function, fC does not depend on x1,x4 or x6 anymore
(However, we still consider fC as a function of all n variables, it
just happens to be independent of x1,x4 and x6).
• x1f  fx1
Example: f= ac + a’c , af = ac, fa=c
ECE 667 - Synthesis & Verification - Lecture 9b
11
Fundamental Theorem
Theorem: Let c be a cube and f a function. Then c  f  fc  1.
Proof. We use the fact that xfx = xf, and fx is independent of x.
If : Suppose fc  1. Then cf=fcc=c. Thus, c  f.
f
c
ECE 667 - Synthesis & Verification - Lecture 9b
12
Proof (cont.)
Only if. Assume c  f
Then c  cf = cfc. But fc is independent of literals i  c.
If fc 1, then  m  Bn, fc(m)=0.
We will construct a m’ from m and c in the following manner:
mi’=mi, if xic and xic,
mi’=1, if xi  c,
mi’=0, if xi  c.
i.e. we made the literals of m’ agree with c, i.e. m’  c c(m’)=1
Also, fc is independent of literals xi,xi  c
fc(m’) = fc(m) = 0
C=xz
m= 000
m’= 101
m
ECE 667 - Synthesis & Verification - Lecture 9b
fc(m’) c(m’)= 0
contradicting c  cfc.
m’
13
Cofactor of Covers
Definition: The cofactor of a cover F is the sum of the cofactors of
each of
the cubes of F.
Note: If F={c1, c2,…, ck} is a cover of f, then Fc= {(c1)c, (c2)c,…, (ck)c}
is a cover of fc.
Suppose F(x) is a cover of f(x), i.e.
F ( x)   ci  
Then for 1jn,
i
i
i
j
 {ci }
j
F ( x) x j   (ci ) x j
i
is a cover of fxj(x)
ECE 667 - Synthesis & Verification - Lecture 9b
14
Cofactor of Cubes
Definition: The cofactor Cxj of a cube C with respect to a literal xj is
• C if xj and x’j do not appear in C
• C\{xj} if xj appears positively in C, i.e. xjC
•  if xj appears negatively in C, i.e. xjC
Example 1:
C = x1 x’4 x6,
Cx2 = C
(x2 and x2 do not appear in C )
Cx1 = x’4 x6 (x1 appears positively in C)
Cx4 = 
(x4 appears negatively in C)
Example 2:
F = abc + b’d + c’d
Fb = ac + c’d
(Just drop b everywhere and throw away cubes containing literal b)
ECE 667 - Synthesis & Verification - Lecture 9b
15
Shannon Expansion
f : Bn  B
Shannon Expansion:
f  xi f xi  xi f xi
Theorem: F is a cover of f. Then
F  x i Fx i  x i Fx i
We say that f (F) is expanded about xi.
xi is called the splitting variable.
ECE 667 - Synthesis & Verification - Lecture 9b
16
Shannon Expansion (cont.)
F  ab  ac  bc
Example
F  aFa  aFa  a(b  c  bc)  a(bc)
 ab  ac  abc  abc
ac
bc
ab
c
b
a
Cube bc got split into two cubes
ECE 667 - Synthesis & Verification - Lecture 9b
c
b
a
17
List of Cubes (Cover Matrix)
We often use a matrix notation to represent a cover:
Example: F = ac + c’d =
a c
c’ d
•
•
•
•
a b c d
 1 2 1 2
 2 2 0 1
or
a b c d
1 - 1 - - 0 1
Each row represents a cube
1 means that the positive literal appears in the cube
0 means that the negative literal appears in the cube
The 2 (or -) represents that the variable does not appear in the
cube. It implicitly represents both 0 and 1 values.
ECE 667 - Synthesis & Verification - Lecture 9b
18
Some Special Functions
Definition: A function f : Bn  B is symmetric with respect to
variables xi
and xj iff
f(x1,…,xi,…,xj,…,xn) = f(x1,…,xj,…,xi,…,xn)
Definition: A function f : Bn  B is totally symmetric iff any
permutation of
the variables in f does not change the
function
Symmetry can be exploited in searching the binary decision tree
because:
f xi x j  f xi x j
- That means we can skip one of four sub-cases
- used in automatic variable ordering for BDDs
ECE 667 - Synthesis & Verification - Lecture 9b
19
Unate Functions
Definition: A function f : Bn  B is positive unate in variable xi iff
f xi  f xi
This is equivalent to monotone increasing in xi:
f (m  )  f (m  )
for all min-term pairs (m-, m+) where
m j  m j , j  i
mi  0
mi  1
For example, m-3=1001, m+3=1011(where i=3)
ECE 667 - Synthesis & Verification - Lecture 9b
20
Unate Functions
Similarly for negative unate
monotone decreasing:
f xi  f xi
f (m  )  f (m  )
A function is unate in xi if it is either positive unate or negative unate
in xi.
Definition: A function is unate if it is unate in each variable.
Definition: A cover F is positive unate in xi iff xi  cj for all cubes cjF
ECE 667 - Synthesis & Verification - Lecture 9b
21
Example
f  ab  bc  ac
m+
c
f(m-)=1  f(m+)=0
b
a
positive unate in a,b
negative unate in c
m-
ECE 667 - Synthesis & Verification - Lecture 9b
22
The Unate Recursive Paradigm
• Key pruning technique based on exploiting the properties of
unate functions
– based on the fact that unate leaf cases can be solved
efficiently
• New case splitting heuristic
– splitting variable is chosen so that the functions at lower
nodes of the recursion tree become unate
ECE 667 - Synthesis & Verification - Lecture 9b
23
The Unate Recursive Paradigm
Unate covers F have many extraordinary properties:
– If a cover F is minimal with respect to single-cube
containment, all of its cubes are essential primes.
– In this case F is the unique minimum cube representation of
its logic function.
– A unate cover represents the tautology iff it contains a cube
with no literals, i.e. a single tautologous cube.
This type of implicit enumeration applies to many sub-problems
(prime generation, reduction, complementation, etc.). Hence, we
refer to it as the Unate Recursive Paradigm.
ECE 667 - Synthesis & Verification - Lecture 9b
24
Unate Recursive Paradigm
• Create cofactoring tree stopping at unate covers
– choose, at each node, the “most binate” variable for splitting
– recurse till no binate variable left (unate leaf)
• “Operate” on the unate cover at each leaf to obtain the result for that
leaf. Return the result
• At each non-leaf node, merge (appropriately) the results of the two
children.
a
b
c
merge
• Main idea: “Operation” on unate leaf is computationally less complex
• Operations: complement, simplify,tautology,generate-primes,...
ECE 667 - Synthesis & Verification - Lecture 9b
25
Recursive Complement Operation
• We have shown how tautology check (SAT check) can be
implemented recursively using the Binary Decision Tree
• Similarly, we can implement Boolean operations recursively
• Example COMPLEMENT operation:
Theorem:
f  x  fx  x  fx
g  x  fx  x  fx
Proof:
f  x  fx  x  fx
f  g  0
 g  f
f  g  1
ECE 667 - Synthesis & Verification - Lecture 9b
26
COMPLEMENT Operation
Algorithm COMPLEMENT(List_of_Cubes C) {
if(C contains single cube c) {
Cres = complement_cube(c) // generate one cube per
return Cres
// literal l in c with ^l
}
else {
xi = SELECT_VARIABLE(C)
C0 = COMPLEMENT(COFACTOR(C,^xi)) Ù ^xi
C1 = COMPLEMENT(COFACTOR(C,xi)) Ù xi
return OR(C0,C1)
}
}
ECE 667 - Synthesis & Verification - Lecture 9b
27
Complement of a Unate Cover
• Complement of a unate cover can be computed more efficiently
• Idea:
– variables appear only in one polarity on the original cover
(ab + bc + ac) = (a+b)(b+c)(a+c)
– when multiplied out, a number of products are redundant
aba + abc + aca + acc + bba + bbc + bca + bcc =
ab + ac + bc
– we just need to look at the combinations for which the
variables cover all original minterms
– this works independent of the polarity of the variables
because of symmetry to the (1,1,1,…,1) case
ECE 667 - Synthesis & Verification - Lecture 9b
28
Incompletely Specified Functions
F = (f, d, r) : Bn  {0, 1, *}
where * represents a don’t care.
• f = onset function • r = offset function • d = don’t care function -
f(x)=1  F(x)=1
r(x)=1  F(x)=0
d(x)=1  F(x)=*
(f,d,r) forms a partition of Bn. i.e.
• f + d + r = Bn
• fd = fr = dr =  (pairwise disjoint)
ECE 667 - Synthesis & Verification - Lecture 9b
29
Incompletely Specified Functions
A completely specified function g is a cover for F=(f,d,r) if
f g  f+d
(Thus gr = ). Thus, if xd (i.e. d(x)=1), then g(x) can be 0 or 1, but
if xf, then g(x)=1 and if xr, then g(x)=0.
(We “don’t care” which value g has at xd)
ECE 667 - Synthesis & Verification - Lecture 9b
30
Example:Logic Minimization
Consider F(a,b,c)=(f,d,r), where f={abc, abc, abc} and d ={abc, abc}, and
the sequence of covers illustrated below:
F1= abc + abc+ abc
Expand abca
on
off
Don’t care
F2= a+abc + abc
abc is redundant
a is prime
F3= a+abc
Expand abc  bc
F4= a+bc
ECE 667 - Synthesis & Verification - Lecture 9b
31