A modern VLSI chip has a zillion parts -- logic, control, memory, interconnect, etc. How do we design these complex chips? Answer: CAD software tools. Learn how to build thesA modern VLSI chip is a remarkably complex beast: billions of transistors, millions of logic gates deployed for computation and control, big blocks of memory, embedded blocks of pre-designed functions designed by third parties (called “intellectual property” or IP blocks). How do people manage to design these complicated chips? Answer: a sequence of computer aided design (CAD) tools takes an abstract description of the chip, and refines it step-wise to a final design. This class focuses on the major design tools used in the creation of an Application Specific Integrated Circuit (ASIC) or System on Chip (SoC) design. Our focus in this first part of the course is on key Boolean logic representations that make it possible to synthesize, and to verify, the gate-level logic in these designs. This is the first step of the design chain, as we move from logic to layout. Our goal is for students to understand how the tools themselves work, at the level of their fundamental algorithms and data structures. Topics covered will include: Computational Boolean algebra, logic verification, and logic synthesis (2-level and multi-level). Recommended Background Programming experience (C, C++, Java, Python, etc.) and basic knowledge of data structures and algorithms (especially recursive algorithms). An understanding of basic digital design: Boolean algebra, Kmaps, gates and flip flops, finite state machine design. Linear algebra and calculus at the level of a junior or senior in engineering. Exposure to basic VLSI at an undergraduate level is nice -- but it’s not necessary. We will keep the course self-contained, but students with some VLSI will be able to skip some background material.e tools in this class.
Using SAT for Logic
Loading...
来自 University of Illinois at Urbana-Champaign 的课程
VLSI CAD Part I: Logic
77 个评分
从本节课中
Boolean Representation via BDDs and SAT
Week 2 introduces two powerful and important representation techniques that allow us to do SERIOUS computational Boolean algebra, on industrial-scale designs.
与讲师见面
Rob A. RutenbarAdjunct Professor
Department of Computer Science
[music]. So, here in Lecture 4.3 we're going to
complete our exploration of Computational Boolean Algebra by completing our
discussion of Boolean SAT. And what we've seen so far is at, at a
high level, how to represent a SAT problem in a CNF form and how something like a
Boolean constraint propagation can help us answer the questions about satisfiability
or unsatisfiablity. But what you don't know yet is, how would
I actually take a realistic network of logic gates and turn it into this slightly
strange looking CNF form. And, how would I actually pose an
engineering relevant question like, are these two implementations of this big,
complicated Boolean function as logic gates, are these two things the same or,
or not? What's going on?
Turns out there's a surprisingly simple mechanical procedure for going from real
logic, with gates and wires, into CNF form.
And so we're going to walk through that and complete our discussion of Boolean
satisfiability in this lecture. I, I think it's first good to actually
just take a little bit of a step back, because what we really did this week in
the course is, you know, for the first half of the week we did binary decision
diagrams, and for the second half of the week we did Boolean satisfiability.
It's important to know that they're not, they're not the same.
They're complimentary. So, this is a kind of, of a slide that
says, you know, they're really not equal. You know, they're not, they're not really
exactly the same. And it's important to know both.
That's why we spent this entire week on these two really vital topics.
So look. Bdds often work well for many problems,
and SAT often works well for many problems.
But for both of them there is no guarantee that it will always work.
Sorry. It is just in the nature of solving things
that are exponentially hard, that sometimes your heuristic techniques might
not work. So, for a BDD, basically, what we can do
is we might be able to, we hope, build a BDD to represent the function.
And for the SAT side, we can solve for satisfiability with a yes or no answer on
that function. And those things are really different
things. Okay.
Now lets be all, lets be, lets be clear that sometimes I cannot build the BDD with
reasonable computer resources. And what typically happens is you run out
of memory. You just don't have enough gigabytes to
build the BDD. And on the SAT side, you sometimes cannot
find the SAT solution. You cannot find a satisfying assignment or
prove that one does not exist with reasonable computer resources.
Typically, you run out of time. You know, you just, you're just searching
and searching and searching and searching and you just, you just don't finish.
So, one of the things to be remembering is that, you know, the BDD does in fact build
a full representation of the function. It represents everything there is.
It is, in fact, a canonical representation of the function, that's one of the really
cool things about BDDs. But SAT solvers do not represent the
entire function. Which is to say, they do not represent it
in a way that supports a big, rich, beautiful set of manipulations.
You want to do a sort of an arbitrary kind of a computational thing on a Boolean
function. You probably want to start with a BDD
because you just have this rich pallet of operators.
But, if you just want to solve for the Boolean functions, say, hey, can I make it
0? Yes or no, that's when you want to use
SAT. So, for example, you can build the
functions that represent existential and universal quantifications.
That's, you know, one of the kinds of manipulations you can do in a BDD
universe. In the SAT universe, it turns out that
there are actually different versions of SAT solvers.
Not every SAT solver, but there are versions of SAT solvers.
They are called Quantified SAT solvers, where you can say, okay, look here's the
function and you give it to him in a CNF form.
And then you say, and here are the variables I would like to quantify away
please. And the SAT solver does some interesting
internal magic and then solves for satisfiability on the quantified function.
It's a whole different category of SAT solvers.
But, you cannot do arbitrary Boolean manipulations with SAT solvers.
You can solve for SAT. That's what they do.
If you want to do arbitrary things on a Boolean function, you probably want a BDD.
You can do SAT with a BDD. It's just probably the not, the most
efficient way. Okay?
So important? Maybe a little bit subtle set of
distinctions but, you know, if you sort of get this internalized.
You'll be, you'll be making some real progress toward, you know, toward being,
being a serious[UNKNOWN] person. So you know, what's a typical practical
SAT problem? Hey, I have two logic networks.
And they are both logic networks of exactly the same inputs and I would like
to know if they are the same Boolean function.
I would like to know if F does exactly the same thing as G.
So, I'm just asking the question is F the same thing as G?
How do you do that? Well, what you do typically is the
following. For every pair of outputs, and let's just
assume that F1 is supposed to be G1. They're supposed to be doing the same
thing. And F2 is supposed to be G2.
They're supposed to be doing the same thing.
For every pair of outputs, you put an Exclusive OR Gate.
So you put F1 in there and G1 in there. And then over here, you also put another
Exclusive OR Gate and you put F2 over there and G2 over there.
Now, let's think for a minute. What will make the Exclusive OR Gates 1.
And it's the answer if the F and the G inputs disagree.
All right. So, the only way to make a 1 with these
XOR gates is to have F and G not be the same function.
Ok. So, what are we looking for here?
We're looking for a single OR gate. Ok.
Let's call that Z. And what's going to be true?
Well what's going to be true is that Z is going to be 1.
It's going to be satisfiable, right? We shall be able to find a pattern of Xs,
that makes Z make a 1 if and only if F is not equal to G.
Right? That makes sense, right?
And so and if we can find Z satisfiable. Right?
Then we will find an X that has the property.
Right? That, that, you know, something that F
does with X is not equal to something that G does with X.
It's going to be, you know, at least, you know, one of those, one of those sets of
inputs is going to be different. So that's pretty cool, right?
I have two big complicated, you know, pieces of real engineering logic.
And I'd like to say, wow are these two things doing to the same thing?
Exclusively or the associated outputs, or together all of those exclusive ORs ask a
Boolean satisfiability solve it question. Hey, can I make Z equal to a 1?
If I can make Z equal to a 1, the networks are not the same.
This patterns of inputs makes the outputs different.
And not only will I discover that this is the case, but I will get an input X that
actually makes F and G different, that might be helpful as a debugging tool.
And if it unsatisfiable, if Z is always 0, then yes they are in fact the same logic.
They're doing the same thing. So that's pretty cool.
But that raises a whole bunch of questions.
And the first question is how do I start with a gate-level description and get a
CNF? Isn't this hard?
Right. I mean, don't I need Boolean algebra or
BDDs or something complicated? The CNF form was you know, a little weird.
You know, it certainly felt a little awkward.
And you know, if I have some big logic network with 50,000 gates in it, isn't
that just hideous? And the answer is no.
It's actually really, really easy. It's surprisingly easy.
But we have to build up a little bit of technology, a little bit of math to, to
get us there. So let's, let's take a look at that.
So, here's a little logic network. There is a NAND gate numbered 1 with two
inputs, and a NOR gate number 2. And of the three inputs of this circuit,
one of them is shared between gates 1 and 2.
Gate 1 goes to an inverter ,gate 3, and as one input of an OR gate, gate 4.
Nor gate 2 is also the other input to gate 4.
And gate 5 is an AND gate that takes the output of inverter 3 and OR gate 4, and
that's it. So, how do you do this CNF thing?
And the big wonderful simple idea is that you can build up the CNF one gate at a
time. So, we need to introduce a concept here.
And the concept is that there is a gate consistency function, which we will call.
If the whole, let's say the whole function is, is, you know, something called phi.
The gate consistency function is phi sub name of output.
So let's, let's say that we've got this NAND gate here, it has inputs a and b, and
it has an output called d. And so, the gate consistency function is
called phi d. And this is actually equal to d equivalent
to the function of the gate. So let's remember here that, you know,
what this gate is really doing. This gate is an, NAND gate.
So it's ab bar. That's what this gate is doing.
So, this is really nothing more than the symbol that we use for the output of the
gate, Exclusive NORd with the Boolean formula for what this gate is supposed to
be doing, which is ab bar. And if you do just a little Boolean
simplification on this, you will get a plus d, b plus d, a bar plus b bar, plus d
bar, and this is equal to phi sub d. Now, okay.
Why am I doing this? You know, what, what good is this?
This turns out to be a really, a really, you know, magical little, little helpful,
helper function that's going to actually let us get a CNF for the entire network no
matter how complicated it is, one gate at a time.
So first, just a little review, just so everybody's, you know, up on this.
Exclusive OR, XOR you know, we write that as A circle with a plus sign, B.
The output is 1 just if a and b are different.
Okay? Right.
So that's, that's typically this, this gate.
It's kind of an OR gate with another bar on it.
A and B are the inputs. Lets say Y is the output.
This is Y equals a bar b plus A B bar. So this is the gate that makes a 1 when
its input are different. Exclusive NOR I like to write it this way.
I like to write it as an Exclusive OR gate with a bar over it.
Other people like to write it as a, like an AND function with a circle around it.
I'm not, not a, not a big fan of that. It's a, personal taste thing.
It's again a NOR gate, but it has a bubble on it, so that you are reminded that it is
Exclusive NOR. It has two inputs, A and B, and again, an
output Y. And A is I'm sorry Y, the output is a 1,
just if the inputs are the same. Right?
And so, this is Y equals AB Plus A bar, B bar and you can just see from the Boolean
formulas they are that the Exclusive OR is a 1 just if they're different and the
Exclusive NOR is a 1 just if they are the same.
So, just kind of a reminder. Right.
And so, the gate consistency function is the Exclusive NOR of the symbol for the
gate output. Exclusive NOR'd with the Boolean formula
of what the gate does. Now, what does that do?
It is something actually rather nice. The gate consistency function makes a 1
just for combinations of inputs and the output.
There are consistent, with what the gate actually does.
And so, what that means is that, the gate consistency function is an interesting
little object where you can put in an a and you can put in a b and you can put in
a d and the gate consistency function will say, 1, yes, that's what the gate does or
0, no, that's not what the gate does. For example, what if I have a as a 0, b as
a 0 and d as a 1? Well, this is a NAND gate.
So, I put in a 0 here. I put in a 0 here.
0 and 0 is 0. 0 inverted is 1.
Yes, indeed I should make a 1. This is consistent.
And go ahead. Try it.
What you'll discover is if you do this, phi d is a 1.
Phi d will say yes, a is 0, b is 0, d is 1.
Yes indeed. That's what this gate does.
But what if you did instead, this. What if you put in two 1s.
1 and 1 is 1. 1 inverted is a 0.
Unfortunately, I've just said that I think d one.
This is inconsistent. What will actually happen here, is that
phi d will be a zero. Right?
And so that's what phi d does. Phi d is a function that says hey, is this
what the gate does? It turns out that all you really need to
do to make the satisfiability formula for the entire gate network, is to put
together and together, all of the gate consistency functions because every single
one of those gate consistency functions basically links its inputs to its outputs
and for most of those gates, the output is an input on the next gate.
Right? And so this is the mechanism by which the
clauses get glued together so their values are all overlapping.
So, the only way to make the entire function a 1 is to have everything
consistent all the way through. Its an interesting incredibly practical
concept. So, for your logic network, you now have
to label each wire. Everything, right?
And so here are the inputs of this network and here is the output of this network.
And this is the same logic network before. Gates 1, 2, 3, 4, 5.
1 is a NAND, inputs a b output d. 2 is a NOR, inputs b c output e.
3 is NOT input d output f. 4 is an OR, input d e output g.
5 is an AND, input f g output h. You have to label every single internal
wire with a variable name. Right?
And the reason is that you're going to be writing Boolean equations for every single
gate. So, every input and every output has got
to have a name. So, let us assume that we'd like to do
this for g. All right, and so what I need then is I
need to go look at that gate. Alright.
And so those are internal nodes that need a name.
And that's an internal node that needs a name.
And so this is the gate that's an OR gate. It's got d and e going into it.
And it's got g going out of it. If we were to actually do this, you know,
gate consistency function, phi g is going to be the name of the output, which is g.
And this is going to be Exclusive NOR'd with a Boolean expression for what this
thing does, which is d plus e. If we were to actually grind that out, we
would discover that, that is d bar plus g ANDed with e bar plus g, ANDed with d plus
e plus g bar. And, there we have it.
And, you know, it's you know, it's worth doing this for a few of these others to
just sort of try your hand and kind of convince yourself what's going on here.
So, what do we do next? Well, to get the entire CNF for the entire
net list, what you do is the following. You build this CNF.
Ok, for phi. And it's got two parts.
You actually have to put the output variable there, as one of the clauses.
And then really, you know, there's the output variable.
And you actually have to put it there and there it is right there.
And the idea is that we are solving for satisfiability for the whole thing.
One of the thing is that it's got to be true is that h is a one.
And the way you make sure that h is a 1 in this clause database is by putting a
clause which has an h in it, which can only be satisfied if h is equal to 1.
Right? And then it's got a product and that
product means a big AND over every gate in the network, and then you put the gate
consistency functions. That's what the phi k's are.
And so, there is a gate consistency function for, for gate 1, and a gate
consistency function for gate 2, and a gate consistency function for gate 3, and
a gate consistency function for a gate 4, and a gate consistency function for gate
5. Right.
So same logic network here, NAND gate 1, NOR gate 2, NOT gate 3, OR gate 4 AND gate
5, exactly the same. And I've got this wonderful big clause CNF
format which I could just literally read off.
Gate 1 makes the gate consistency function.
Bam, put it down. Gate 2 makes the gate consistency
function. Bam, put it down.
Gate 3 makes the gate consistency function.
Put it down. Put down the one for 4.
Put down the one for 5. Remember to put in a single clause which
is the output variable. There you have it.
This is the CNF for your logic network. You can do it from the gates and wires
themselves just walking the network. Yeah, it's going to be pretty big.
Sorry. That's just the way it works.
Hand it to the SAT solver. Ask the questions you want to do.
So, you don't read to do any real Boolean algebra simplification other than for each
individual gate level function. And at the network level you AND them all
together. Now, as the result of this, smart people
have written the formulas down, because it's really boring to have to continue to
derive these. And this is a big complicated slide.
So I got this these formulas from pretty famous paper by, from Fadi Aloul, Igor
Markov, and Karem Sakallah. All at the University of Michigan where
they were, you know, just doing some interesting things with SAT.
And here are the formulas. So, there's a formula for interestingly
any, enough, a wire. Because sometimes you just have a wire
where you have sort of the output of one gate is called let's say x and the input
of next gate is called, let's say z. And you have a wire that looks like a
Boolean function, z equals x. You need a Boolean CNF formula for it.
X bar plus z, x plus z bar. And then, you need formulas for NOR gates,
OR gates, NAND gates, AND gates, and inverters.
Inverters are easy. X plus z, x bar plus z bar.
All of the rest of them are kind of complicated.
And they're kind of complicated, but they're also kind of simple.
They've all got exactly three parts. So let's just look for example, at the nor
gate. The first part is a product.
And it's a product over all of the inputs. There are n inputs.
And this particular product is xi bar plus z bar.
So, you've got, if you had a four-input NOR gate, you get four products and they
all look like xi bar plus z bar. And then, that is ANDed with a sum term
that's got two things in it. Right.
So this is a sum, this is you know, an OR. This is an OR of all the inputs.
So, if you had 4 inputs, x1, x2, x3, x4. This is x1 plus x2 plus x3 plus x4.
And then you've got one more term in this sum, which in this case is just the z
term. And if you look at each of these equations
for NOR OR, NAND AND, what you will discover is that they only differ in where
the compliment bar, where the bars are, you know, where the inversions are.
And it's just the way it works out if you do the exclusive nor of the function and
grind out the algebra. This is just the pattern.
And so, you know, just worth remembering them.
Or, you know, write them down on the back of your hand.
I guess that might be a better answer. Now, one other thing that I will, I will
admit, and this is unfortunate, but you know, I have to tell you how EXOR gates
and EXNOR gates work because they also have gate consistency functions.
And the problem is EXOR gates and EXNOR gates are rather unpleasant for SAT
solvers. The, the basic either-or structure makes
for some tough SAT search and they have rather large gate consistency functions
too. So, just the small two input gates creates
a lot of terms. And so here's the, you know, what happens
if z is equal to the Exclusive OR. Of a and b the gate level consistency
function will be z XNOR ax OR b. That's a little bit of unpleasant Boolean
algebra. I'm, I'm just writing it down for you.
I strongly encourage you to go figure out the one for the XNOR.
We don't need to, you could if you want, you could derive the formula for more
inputs. It's just unpleasant.
It's just big and ugly. But now you know, you have the gate level
consistency functions for all the gates worth knowing.
And you could walk the Boolean expression, the Boolean logic network that you had and
you could build a gate level consistency function.
And it's just worth, you know, just really doing one here, just to kind of convince
ourselves we know. So here, here is the general formula for
an n input NAND gate. It's got a product term, and it's got
that's ANDed with a sum term, that has one additional out contribution term, related
to the output. What happens if n is just two?
Right? Well what do you get?
So here's the product term. Right?
Because this product just means AND. And because n is equal to 2.
Right. The product from i equals 1 to 2 of xi
plus z is x1 plus z and x2 plus z. That's all that means.
And then there's a sum term. And again, n is equal to 2.
And so this is the sum from i equals 1 to n.
And the sum means OR. Right?
So, there's one additional term here. And so the sum from i equals 1 to 2 of xi
bar is not x1 plus not x2. And then we are still inside the same sum.
And there's always one more term there, and this is in this case z bar.
And so that's how you read these formulas and that's how you do it.
It's all entirely mechanical. In fact nobody does this by hand.
You write a program. We're actually going to ask you to write
it by hand because you know, it's good to do this once in your life for something
with, you know, three or four, five gates in it.
Something that generates, you know, ten or 15 clauses.
By the time you mechanically do that in, you know, paper and pencil form.
Trust me, you're going to know how it works.
So that's it for, for Boolean satisfiability.
It's a wonderful important technology and, together with BDDs, it pretty much
represents the sort of the universe of, of representations and sort of large
computational tools for, for Boolean equations.
I'll note that SAT really has largely displaced binary decision diagrams for
that surprisingly large set of applications where I just need to solve
it. I just have to say, can I find a
satisfying assignment for this big Boolean function, yes or no?
Yes, give me one. No, okay that's what I need to know.
And so there are lots of things that have been transformed into forms that make SAT
the preferred technology but BDDs are still really important and all over the
place. The big reason for SAT is that its more
scalable. You can do gigantic problems, 50,000
variables, 25 million clauses, 50 million, against fifty million clauses.
Right? Sorry.
50 million literals you know, appearances of variables in the clauses.
But, you know, literally,you know, tens of thousands of variables, tens of millions
of clauses. Those are gigantic problems.
You can actually solve those things, you know, kind of remarkably quickly.
Still SAT, like BDDs, not, not, not guaranteed to find a solution in a
reasonable amount of time or space. The idea is, you know, 40 to 50 years old,
depending on which paper you're looking at.
But it's still the big idea. Davisputnamlogemannloveland is the, the
sort of the computational guts of the recursion.
But there have been some amazing engineering advances that make it
stupendously fast. And we're actually going to get to play
with this on some homework assignments. Before I finish this, this lecture riff, I
just wanted to have some acknowledgments to some of my friends.
Karem Sakallah is my buddy from the, the University of Michigan.
I'll admit, I'm a University of Michigan alum.
Like me and Claude Shannon and Karem was very generous with you know time and
inputs in some very early versions of these lecture materials.
And his former PHDA student Joao Marques-Silva, who did some of the
earliest work on conflict learning provided some the samples in some of the
papers that I'm using for this. And he's now at the University College
Dublin. So big thanks to both of those guys for
helping me out on this lecture. And now we're going to move from
representing things to synthesizing things.
So that's our next great set of topics. [music].
