Transcript Systems Design and Verification Challenges

Using a Formal Specification
and a Model Checker
to Monitor and Guide Simulation
Verifying the Multiprocessing Hardware of the Alpha
21364 Microprocessor
Serdar Tasiran
Koç University, Istanbul, Turkey
(formerly Compaq/HP Systems Research Center)
Yuan Yu (Microsoft Research, formerly Compaq)
Brannon Batson (Intel, formerly Compaq)
But first
Formal Methods
(i.e. mathematical, algorithmic)
for
Software and Hardware Designs
or
“Why should you care?”
French Guyana, June 4, 1996
$800 million software failure
Mars, July 4, 1997
Lost contact due to real-time priority inversion bug
Faulty division algorithm (Intel Pentium)
$475 million replacement cost
Faulty floppy disk controller (Toshiba)
$2.1 billion court settlement
$4 billion development effort
> 50% system integration & validation cost
400 horses
100 microprocessors
Cost of Finding Flaws Late
Feb. 17, 2003
Comp 302, Spring 2003
SCIENCE
ENGINEERING
Natural Systems
Artificial Systems
PURE
Abstract
Systems
THEORY
ANALYSIS
Veri/Falsi
fication
APPLIED
Concrete
Systems
EXPERIMENT
DESIGN
DESIGN VERI/FALSIFICATION
INFORMAL
(ad hoc)
• by simulation
• by test
• by proof
• by algorithm
FORMAL
(systematic)
Poor coverage
High recovery cost
Typical Abstraction Layers for a Hardware Design
System (Behavioral) Level
Register Transfer Level (RTL)
Gate Level
Transistor Level
Layout Level
Koç University – ECE Graduate Program
Design Process
• Design : specify and enter
the design intent
Verify:
verify the
correctness of
design and
implementation
Implement:
refine the
design
through all
phases
Koç University – ECE Graduate Program
System (Behavioral) Level
• Abstract algorithmic description of high-level behavior
– e.g. C-Programming language
Port*
compute_optimal_route_for_packet(Packet_t *packet,
Channel_t *channel)
{
static Queue_t *packet_queue;
packet_queue = add_packet(packet_queue, packet);
...
}
– abstract because it does not contain any implementation details for
timing or data
– efficient to get a compact execution model as first design draft
– difficult to maintain throughout project because no link to
implementation
Koç University – ECE Graduate Program
RTL Level
• Cycle accurate model “close” to the hardware implementation
– bit-vector data types and operations as abstraction from bit-level
implementation
– sequential constructs (e.g. if - then - else, while loops) to support
modeling of complex control flow
module mark1;
reg [31:0] m[0:8192];
reg [12:0] pc;
reg [31:0] acc;
reg[15:0] ir;
always
begin
ir = m[pc];
if(ir[15:13] == 3b’000)
pc = m[ir[12:0]];
else if (ir[15:13] == 3’b010)
acc = -m[ir[12:0]];
...
end
endmodule
Koç University – ECE Graduate Program
Gate Level
• Model on finite-state machine level
– models function in Boolean logic using registers and gates
– various delay models for gates and wires
1ns
4ns
3ns
5ns
Koç University – ECE Graduate Program
Transistor Level
•
Model on CMOS transistor level
– depending on application function modeled as resistive switches
• used in functional equivalence checking
– or full differential equations for circuit simulation
• used in detailed timing analysis
Koç University – ECE Graduate Program
Layout Level
•
Transistors and wires are laid out as polygons in different
technology layers such as diffusion, poly-silicon, metal, etc.
Koç University – ECE Graduate Program
Flavors of Verification
System (Behavioral) Level
Register Transfer Level (RTL)
Gate Level
Transistor Level
Design Verification: Does the
design make sense? If I
implemented it as designed,
would it satisfy the design
requirements?
Implementation Verification:
Is the implementation at the
lower layer of abstraction
consistent with the higher
level?
Layout Level
Koç University – ECE Graduate Program
Systems Design and Verification Challenges
• Heterogeneity (analog, digital, HW/SW)
• Complexity (~billion transistors, ~millions of lines of code)
• Time-to-market
Koç University – ECE Graduate Program
Role of Computer-Aided Design and
Verification Tools: Helping humans cope
Intelligence
Quotient
Transistors
PPC603
Pentium
10M
80486
1M
68020
68000
100K
10K
Pentium Pro
PPC601
80386
180
68040
MIPS R4000
160
140
8086
120
4004
8080
1K
100
100
80
10
50
1
1975
1980
1985
1990
Processor Complexity
Avg. Human IQ
1995
Formal Verification Tools
Description of system
to be verified:
- Finite state machine
- Code written in a hardware
description language
Specification:
-Temporal logic formula
- Algorithm- or protocol-level
description for design
G(p F q)
p
q
Verifier
No
Yes
Error trace
Simulation vs. Formal Verification

Simulation
• Not complete
• Need to generate
expected behavior
• Difficult to cover corner
cases
• CPU intensive
– have to run billions of
cycles
• Can handle large
systems

Formal Verification
• Complete wrt specification
• No need to generate expected
behavior
• Corner cases are
automatically taken care of
• Most of the state-of-the-art
methods are memory
intensive
• Memory usage is strongly
related with the size of
systems to be verified
Exploring the State Space of an FSM
• Implicit methods: Represent
sets of states with decision
diagrams
• Representation size not
proportional to number of
states
• But still memory limited
1011 stars
107 transistors
10100,000 states
The Moral …

Verification is a serious problem

Formal verification methods are great, but not practical
yet on complex systems

Simulation is practical, but can’t provide strong enough
guarantees

Next part of talk: A hybrid technique:

Simulation + formal verification