Transcript slides

Formal Methods and Physical Design:
Match Made in Heaven
or Fools’ Paradise?
Dr. Carl Seger
Strategic CAD Labs, Intel
November 18, 2008
Outline
•
•
•
•
Brief Introduction to Physical Design
Using Formal Techniques in Physical Design
Two Illustrative Examples
 Electrical Level Example
 Physics Level Example
Lessons and Future Work
2
Introduction to Physical Design
3
Making Microprocessors
• The process from silicon (sand) to
•
•
finished microprocessor, can be
divided into two distinct phases:
 The design of the microprocessor
 The manufacturing of the
microprocessor
Intuitively, the design comes
before the manufacturing.
However, there are very many
aspects of the manufacturing
process influencing the design
process, so that both must be
understood for successful
processor design.
+
4
The Design Process at 10,000 ft
Architect
Ideas
Architecture
Analysis
MAS
MicroArchitect
Design
Engineer
Development
of microarchitecture
RTL
Mapping
of RTL to
transistors
Mask
Designer
Test
Engineer
Development
of mask
that yield
transistors
and wires
Schematics
Layout/
Mask
Making Silicon
+
Stepping(s)
Original
Product
Target
Chip
Validation
MAS: Micro-Architecture Specification
RTL: Register-Transfer Language
5
Physical Design
Architect
Ideas
Architecture
Analysis
MAS
MicroArchitect
Design
Engineer
Development
of microarchitecture
RTL
Mapping
of RTL to
transistors
Mask
Designer
Test
Engineer
Development
of mask
that yield
transistors
and wires
Schematics
Layout/
Mask
Making Silicon
+
Stepping(s)
Original
Product
Target
Chip
Validation
MAS: Micro-Architecture Specification
RTL: Register-Transfer Language
6
Characteristics of Physical Design
• Yesterday:
Individual problems often relatively simple
 Size of data main difficult
 Most logic designs could be realized
Today/tomorrow
 Accuracy requirements rapidly rising

•

Size of data growing extremely rapidly
-

The problems are by themselves much harder
E.g., modern micro-processor:
– 109 transistors
– 1010 wires
– 1012 polygons
Compare: 1011 is approximately all pages on the WEB
Some logic designs not realizable
-
There are constraints from physical implementation that
affects logic design as first order effects.
7
Formal/Symbolic Methods
8
Introduction
•
Suppose you have the following circuit and
would like to understand what Boolean
function the circuit computes.
•
Two approaches:
 Simulate every input combination
- Not feasible for larger/more realistic circuits
 Build the output expression by symbolically
simulating the circuit
9
Symbolic Simulation Using BDDs
A
~A
B
AB
A(~ B)
10
Traditional Use of Formal Methods
•
•
Formal Verification
 Formal Equivalence Verification
- Is spec model the same as imp model
- Used extensively and is a “must do” for tape-out
 Formal Property Verification
- Does this circuit satisfy some desired property
- Used extensively for “small” properties
- Starting to get more wide-spread use for “large”
properties
Synthesis
 Computation of don’t cares
 Simplification of logic
11
Symbolic Methods in Physical Design
•
Four major questions:
 Which level of abstraction?
- Electrical, component, layout, or mask
 Which question is to be answered?
- Find a (good) solution
- Find the best solution
- Make sure all cases satisfies something
- Characterize the viable design space
 Which encoding should be used?
- Bit-level or word level
- Arithmetic encoding: binary, unary, …
 Which formal method should be applied?
- BDDs, SAT, SMT, …
12
Electrical Level Example
13
Leakage Minimization
•
Background
 Transistors are not perfect switches
- Even when “off”, a small leakage current will go through
the transistor

Given a combinational circuit:
- What is the maximum leakage?
- Compute an input pattern that produces the minimum
leakage

For a circuit with a couple of gates, this is not
that difficult to compute. However, what if the
circuit looks like:
14
Interesting Problem
o[7:0]
a[7:0]
b[7:0]
15
Background
•
One can approximate a leaky transistor as:
R
where R>>r
r
16
Background cont.
•
Examples of CMOS gates:
a
o
a
b
a
a
b
o
o
a
o
a
b
17
Background cont.
•
From dusty secondary school Physics:
r1
r1+r2
r2
•
r1
r2
r1r2
r1+r2
We can use these to compute the equivalent
resistance of a gate if we know which
switches are on and off
18
Symbolic Algorithm
•
•
•
Try to re-phrase the algorithm to make it
“data independent” or “data oblivious”
Idea:
 Design a “circuit” that takes as inputs the
Boolean values of the primary input (in our
example a[7:0] and b[7:0]) and that computes a
bit-vector representation of the resulting leakage
 Questions:
- How to encode the circuit
- How to encode the resistances, currents, etc.
– Binary vs. unary encoding
How much accuracy is actually needed
…
Simplistic approach for illustration:
19
Modeling the transistors/gates
Transistor models
Interconnect models
Gate models
Example done in
Forte system
using reFLect
20
Examples
21
Examples
22
Complete Algorithm
•
•
•
•
Use symbolic simulation to compute the
Boolean expression over the input variables
for every gate.
For each gate:
 compute symbolically the resistance R for the
gate given the gate functions
 Compute (a scaled version) of 1/R
Add all the 1/R’s together and invert the
result
35 seconds later  a BDD with 3947 nodes is
produced representing every possible
equivalent resistance (i.e., the leakage) for
the whole circuit given it’s input values
23
In Forte:
24
In Forte:
25
To Answer Interesting Questions
26
To Answer Interesting Questions
• Notice: By picking suitable “sleep state”
inputs, we can reduce the leakage power by
>15%
27
Other Electrical Examples
•
•
•
Compute the pair of input vectors that causes
the largest amount of switching in the circuit
 Note: If gates have delays, one can get more
than n switchings in a circuit of size n!
Compute input vectors that cause the
maximum of noise in some wire
(inductive/capacitive coupling between
wires)
…
28
Physics Level Example
29
Mask Making
•
•
•
•
•
Start with extremely clean and
smooth glass plate
Deposit a layer of chrome
Using a laser or e-beam to draw
(by removing) the desired
pattern
Use a stepper to expose the
mask at every location.
 Extreme position accuracy is
needed!
Laser/
E-beam
This sounds fairly simple.
HOWEVER…
30
What Happens in Reality?
• Illuminate mask with
•
•
193nm wavelength light
(UV)
Consider the result for
various sizes of
patterns
The feature sizes are
much smaller than the
wavelength of the light
 diffraction destroys
the pattern
Mask
0.25µ
0.18µ
0.13µ
90-nm
65-nm
Source: Synopsys Inc.
31
What is going on?
• Assume we use 193nm
•
•
coherent (laser) light
Assume a simplistic
photo-resist model
 Simple threshold model
If we plot the intensity
and resist response for a
single small opening in
the mask for a typical
manufacturing lens
configuration, we get:
32
What is going on? Part 2
• With two holes we get:
33
In More Detail
•
Plotting the electrical field as well:
34
Potential Solutions
• Reduce the wavelength of the light

Extreme-UV (13.5nm) is being explored
using reflective optics and reflective masks
-
Incredibly complex and expensive process
• Increase the refractive index

Immersion lithography (optics in water)
-
Adds complexity
• Change what you try to pattern


Make a mask that after exposure yields
the desired pattern on silicon wafer
Some approaches:
-
Optical proximity correction
Phase shifting masks
Immersion lithography
35
Using “Optical Tricks”
• With two holes, but using opposite phase, we get:
36
Symbolic Formulation
•
•
•
•
•
The intensity is proportional to the square of the electric field
The individual contributions to the electric field are linear.
Every pixel with the same distance to the target contribute
the same amount
To avoid having to use large precision (many bits) or floating
point representation, a “quantization” approach works well.
 Each pixel at a specific distance can contribute a fixed (integer)
number of units of electric field.
 Adding up all the positive/negative contributions to the electric
field, translate into simply counting the number of positive and
negative quanta
 Rather than squaring the result and then threshold it for the
resist, use a magnitude function instead.
Past a certain distance, the contribution to the electrical field
is small enough to be ignored.
 Thus dependency between variables is limited (but still large)
37
1-Dimensional Example:
If we want the pattern:
which yields:
30nm
we can use the mask:
38
Lessons and Future Work
39
Observations
•
Four major questions:
 Which level of abstraction?
- All levels seem amenable to formal methods
 Which question is to be answered?
- Find a (good) solution
C+
- Find the best solution
B+
- Make sure all cases satisfies something A
- Characterize the viable design space
A+
 Which encoding should be used?
- Bit-level or word level Not clear…
- Arithmetic encoding: binary, unary, …
 Which formal method should be applied?
- BDDs, SAT, SMT, … Depends on question and size
40
Future Work
•
•
•
•
Explore usage of combining formal/symbolic
methods with more traditional search
algorithms
 Symbolic methods often only choice when highly
“disjunctive” problems and/or few solutions
 For subspaces, a traditional search algorithm
often beats symbolic methods
Symbolic representations for dynamic
programming algorithms
Experiment, experiment, experiment
Watch out for:
 “Has hammer. Looking for nail.”
41
So What is It?
Match Made in Heaven
or
Fool’s Paradise?
Time Will Tell
42
Questions?
43