Transcript slides

Analysis of Microprocessor Components
with a Functional Language-based
Formal Verification Toolbox
Roope Kaivola
Intel
DEG/EMG
Agenda
• Microprocessor Design
• Validation
• Formal Verification
• Functional Programming Language reFLect
• Case: Execution Cluster Verification
• Observations
2
9/21/2006
Copyright © Intel Corporation, 2006. All rights reserved. Third-party marks and
brands are the property of their respective owners. All products, dates, and
figures are preliminary and subject to change without notice.
Microprocessor Design
Moore’s Law - 1965
4
9/21/2006
Copyright © Intel Corporation, 2006. All rights reserved. Third-party marks and
brands are the property of their respective owners. All products, dates, and
figures are preliminary and subject to change without notice.
Source: Intel Museum
Moore’s Law - 40 Years Later
Process Name P854
P856
P858
Px60
P1262
P1264 P1266
1st Production 1995
1997
1999
2001
2003
2005
2007
65nm
45nm
Lithography
0.35mm 0.25mm 0.18mm 0.13mm 90nm
Gate Length
0.35mm 0.20mm 0.13mm <70nm <50nm <35nm <25nm
Wafer Size
(mm)
200
200
200
200/300 300
A new process every two years
5
9/21/2006
Copyright © Intel Corporation, 2006. All rights reserved. Third-party marks and
brands are the property of their respective owners. All products, dates, and
figures are preliminary and subject to change without notice.
Source: Intel
300
300
Moore’s Law - Implications
• Each new process generation doubles the number of
transistors available to architects and designers
• Some of this increase is consumed by larger
structures (caches, TLB, etc.)
• The rest goes to increased complexity:
• Out-of-order, speculative execution machines
• Deeper pipelines
• New technologies (Hyper-Threading, 64-bit
extensions, virtualization, security, … )
• Multi-core designs
6
9/21/2006
Copyright © Intel Corporation, 2006. All rights reserved. Third-party marks and
brands are the property of their respective owners. All products, dates, and
figures are preliminary and subject to change without notice.
Microprocessor Design Scope
Typical lead CPU design requires:
• 500+ person design team:
–
–
–
–
logic and circuit design
physical design
validation and verification
design automation
• 2-2½ years from start of RTL coding to A0 tapeout
• 9-12 months from A0 tapeout to production qual
(may take longer for workstation/server products)
7
9/21/2006
Copyright © Intel Corporation, 2006. All rights reserved. Third-party marks and
brands are the property of their respective owners. All products, dates, and
figures are preliminary and subject to change without notice.
Design Hierarchy
System Bus
Bus Unit
Level 2 Cache
Memory Subsystem
Fetch/
Decode
Unit
Trace Cache
Microcode ROM
BTB/Branch Prediction
Front End
Level 1 Data Cache
Execution Units
Integer and FP Execution Units
Out-of-order
execution
logic
Retirement
Branch History Update
Out-of-order Engine
Pentium® 4 Basic Block Diagram
8
9/21/2006
Copyright © Intel Corporation, 2006. All rights reserved. Third-party marks and
brands are the property of their respective owners. All products, dates, and
figures are preliminary and subject to change without notice.
Cluster
Design Hierarchy
10000k
Full chip
1000k
Cluster
100k
Unit
10k
Fub
1k
gate
elements
9
9/21/2006
Sub-fub
Design level
Copyright © Intel Corporation, 2006. All rights reserved. Third-party marks and
brands are the property of their respective owners. All products, dates, and
figures are preliminary and subject to change without notice.
Validation
300mm Semiconductor Economics
Fab
$3 billion
Pilot line
$1-2 billion
R&D process team
$0.5-1 billion
$5 billion investment requires high volume
to achieve reasonable unit cost
11
9/21/2006
Copyright © Intel Corporation, 2006. All rights reserved. Third-party marks and
brands are the property of their respective owners. All products, dates, and
figures are preliminary and subject to change without notice.
Source: Intel
The Validation Challenge
• Validation driven by the economics of Moore’s Law
• High initial investment requires high volume
• Increased complexity 
increased validation effort and risk
High volumes magnify the cost of a
validation escape
12
9/21/2006
Copyright © Intel Corporation, 2006. All rights reserved. Third-party marks and
brands are the property of their respective owners. All products, dates, and
figures are preliminary and subject to change without notice.
RTL Pre-Silicon Validation Technologies
• Pre-silicon vs. post-silicon validation
• Coverage-based testing
• Cluster Test Environment
• Simulate each cluster in isolation
• Better visibility and controllability
• Full-Chip Test Environment
• Do all the pieces fit together?
• Have we implemented IA-32?
13
9/21/2006
Copyright © Intel Corporation, 2006. All rights reserved. Third-party marks and
brands are the property of their respective owners. All products, dates, and
figures are preliminary and subject to change without notice.
Dynamic Validation
• Pre-silicon simulation has some advantages …
• Fine-grained (cycle-by-cycle) checking
• Complete visibility of internal state
• APIs to allow event injection
• … but no amount of dynamic validation is enough
• A single dyadic extended-precision (80-bit) FP
instruction has ~10**50 possible combinations
• Exhaustive testing is impossible,
14
9/21/2006
even on real silicon
Copyright © Intel Corporation, 2006. All rights reserved. Third-party marks and
brands are the property of their respective owners. All products, dates, and
figures are preliminary and subject to change without notice.
Formal Verification
Organization
• Formal verification is carried out by an independent
team within design/pre-silicon validation
• Pentium® 4 project was the first large-scale effort at
Intel (~60 person years) to apply formal verification
techniques to a CPU design
• Currently FV is an established technology used in
most recent CPU development projects
• FV models are automatically compiled from RTL source
code (gate level)
16
9/21/2006
Copyright © Intel Corporation, 2006. All rights reserved. Third-party marks and
brands are the property of their respective owners. All products, dates, and
figures are preliminary and subject to change without notice.
FPV
Abstract
Model
Checker
Functional Validation
Domain of FV (FPV)
HLM
RTL
Netlist
17
9/21/2006
Copyright © Intel Corporation, 2006. All rights reserved. Third-party marks and
brands are the property of their respective owners. All products, dates, and
figures are preliminary and subject to change without notice.
Formal
Specifications
Formal Verification –
Execution Cluster
Verification Success Story
• Execution Cluster – all micro-operations executed here
• Task: guaranteeing functional correctness
• Huge state spaces (exceeding 2160 )
• Floating-point,
integer arithmetic etc
We can and do formally verify all of them!
• Abstract specifications: clean, precise (IEEE for FP)
• Proofs from low-level RTL to IEEE specification
• Found many high quality bugs on many CPU designs
• Verification highly repeatable
19
9/21/2006
Copyright © Intel Corporation, 2006. All rights reserved. Third-party marks and
brands are the property of their respective owners. All products, dates, and
figures are preliminary and subject to change without notice.
Verification Success Story
Techniques:
• Symbolic simulation (STE)
• Binary Decision Diagrams (BDD’s)
• Theorem-proved decompositions for most complex
micro-ops (div, sqrt, mul)
All this work takes place in the context of a
functional language-based toolbox.
20
9/21/2006
Copyright © Intel Corporation, 2006. All rights reserved. Third-party marks and
brands are the property of their respective owners. All products, dates, and
figures are preliminary and subject to change without notice.
reFLect
reFLect
An open functional programming environment
• Interpreted “ML-like” lazy functional language
• Supports development of libraries, scripting, rapid
prototyping and development of formal tools
let add xv yv =
letrec f [] [] = (F,[])
/\ f (x:xv) (y:yv) =
val (cin,res) = f xv yv in
//
let sum = ( x XOR y ) XOR cin in
let cout = ( x AND y ) OR ( x AND cin ) OR ( y AND cin ) in
//
( cout, ( sum : res ) )
in
snd ( f xv yv );
add::bool list -> bool list -> bool list
22
9/21/2006
Copyright © Intel Corporation, 2006. All rights reserved. Third-party marks and
brands are the property of their respective owners. All products, dates, and
figures are preliminary and subject to change without notice.
reFLect
We write in reFLect:
• System specifications
• Verification strategies
• Debug and analysis code
Language is customized for our FV needs:
• Binary decision diagrams
• Symbolic simulation / trajectory evaluation
• Reflection
23
9/21/2006
Copyright © Intel Corporation, 2006. All rights reserved. Third-party marks and
brands are the property of their respective owners. All products, dates, and
figures are preliminary and subject to change without notice.
reFLect – Booleans and BDD’s
• In addition to traditional Booleans (true/false),
reFLect supports symbolic representations of Boolean
functions with Binary Decision Diagrams (BDD’s), and
symbolic evaluation of objects containing BDD’s
• Useful for verification: we want to check that system
satisfied its specification for all input values
let k = variable "k";
let l = variable "l";
let m = variable "m";
( k OR l ) ==> m;
m + !l&!k::bool
( k AND l ) ==> ( l OR m );
T::bool
24
9/21/2006
Copyright © Intel Corporation, 2006. All rights reserved. Third-party marks and
brands are the property of their respective owners. All products, dates, and
figures are preliminary and subject to change without notice.
reFLect – Booleans and BDD’s
let a = variable_vector "a[2:0]";
let b = variable_vector "b[2:0]";
a;
[a[2], a[1], a[0]]::bool list
add a a;
[a[1], a[0], F]::bool list
add a b;
[b[1]&a[1]&b[2]&a[2] + b[0]&a[0]&a[1]&b[2]&a[2] +
b[0]&a[0]&b[1]&b[2]&a[2] + !b[0]&!b[1]&!b[2]&a[2] +
!a[0]&!b[1]&!b[2]&a[2] + ... ,
b[0]&a[0]&b[1]&a[1] + !b[0]&!b[1]&a[1] + !a[0]&!b[1]&a[1] +
!b[0]&b[1]&!a[1] + !a[0]&b[1]&!a[1] + ... ,
!b[0]&a[0] + b[0]&!a[0]]::bool list
25
9/21/2006
Copyright © Intel Corporation, 2006. All rights reserved. Third-party marks and
brands are the property of their respective owners. All products, dates, and
figures are preliminary and subject to change without notice.
reFLect - Symbolic Trajectory Evaluation
• STE is a built-in function in the reFLect functional
programming environment.
• Implemented as a symbolic four-valued event driven
simulator.
• Our primary approach for data-path dominated
property model checking
• Excels in verification of straight-line pipelined designs
26
9/21/2006
Copyright © Intel Corporation, 2006. All rights reserved. Third-party marks and
brands are the property of their respective owners. All products, dates, and
figures are preliminary and subject to change without notice.
reFLect – Simple Example
let in1 = node_vector "in1[2:0]" mH;
let in2 = node_vector "in2[2:0]" mH;
let out = node_vector "out[2:0]" mH;
let ante = ( gen_clock mclk ["clk"] ( 0 upto 10 ) ) @
( in1 isv a in_cycle 0 ) @
( in2 isv b in_cycle 0 );
let cons = ( out isv ( add a b ) in_cycle 2 );
let check = STE "-s" ckt [] ante cons [];
check;
T::bool
27
9/21/2006
Copyright © Intel Corporation, 2006. All rights reserved. Third-party marks and
brands are the property of their respective owners. All products, dates, and
figures are preliminary and subject to change without notice.
reFLect – Reflection
• Reflection gives programmatic access to source level
syntax
• Theorem-prover to reason about reFLect programs
• Reasoning about the specifications
• Reasoning about the verification engines
• Provides automation for first order and linear
arithmetic goals.
• Hooks to SAT solvers, automated reasoning engines.
28
9/21/2006
Copyright © Intel Corporation, 2006. All rights reserved. Third-party marks and
brands are the property of their respective owners. All products, dates, and
figures are preliminary and subject to change without notice.
EXEC Reusable Verification Framework
• Methodology and tools built in reFLect.
• Support structure
• IEEE compliant floating-point library
• Customized verification strategies
• Interface level proof design environment
• Theorems relating model checking to abstract
specifications
29
9/21/2006
Copyright © Intel Corporation, 2006. All rights reserved. Third-party marks and
brands are the property of their respective owners. All products, dates, and
figures are preliminary and subject to change without notice.
Case: FP Accumulator
• Verification of most micro-operations handled directly by symbolic
simulation: for example, floating point accumulator.
IEEE spec
Theorem proving
Environment
API
Executable
Reference
Model
STE model checking
API adds design-specific
information about signal
names, timing, ...
30
9/21/2006
Accumulator
RTL design
Copyright © Intel Corporation, 2006. All rights reserved. Third-party marks and
brands are the property of their respective owners. All products, dates, and
figures are preliminary and subject to change without notice.
Case: FP Multiplier
• Direct STE not feasible
• Algorithmic
decomposition
• Verify partial product
generation and addition
separately with STE
• Use the deductive
engines in to tie the
results together
S2
S1
Booth
Encoder
C
O
N
T
R
O
L
Exponent
datapath
Partial Products
generator
…
Wallace Tree
Adder Network
Rounder logic
31
9/21/2006
Copyright © Intel Corporation, 2006. All rights reserved. Third-party marks and
brands are the property of their respective owners. All products, dates, and
figures are preliminary and subject to change without notice.
Mantissa
datapath
Observations
Observations
• One of the most successful industrial FV programmes
• Functional language reFLect an essential ingredient
• Single language for
• specifications,
• verification methods and
• reasoning
33
9/21/2006
Copyright © Intel Corporation, 2006. All rights reserved. Third-party marks and
brands are the property of their respective owners. All products, dates, and
figures are preliminary and subject to change without notice.
Observations
• Functional language for specifications:
• Abstraction, clarity
• Well-defined semantics
• Interpreted language:
• Fast analysis
• Ad-hoc experimentation
• Performance penalty not significant, since most
computation resources are used in BDD operations
• Laziness
• essential in avoiding unnecessary computations
• confuses novice users
34
9/21/2006
Copyright © Intel Corporation, 2006. All rights reserved. Third-party marks and
brands are the property of their respective owners. All products, dates, and
figures are preliminary and subject to change without notice.
Questions ?
Opinions ?