Transcript Formal methods at Chalmers

Formal Methods in Hardware
Design
Mary Sheeran, Chalmers
www.cs.chalmers.se/~ms
Formal Methods
• Mathematical and logical methods used in
system development
• Aim to increase confidence in riktighet of
system
• Apply to both hardware and software
Formal methods
• Complement other analysis methods
• Are good at finding bugs
• Reduce development (and test) time
• Should ideally be automatic
The main point is NOT
• correctness proof of entire systems
• replacing test entirely
BUT
• one proof can replace many test cases
• formal methods can be used in automatic
test case generation
Successful formal methods
• Integrated in the design flow
• Avoid new demands on the user
• Work at large scale
• Save time or money in getting a good
quality product out
Some fundamental facts
Low level of abstraction, Finite state systems
=> automatic proofs possible
High level of abstraction, Fancy data types,
general programs
=>
automatic proofs IMPOSSIBLE
Two main approaches
• Squeeze the problem down into one that can
be handled automatically
– industrial success of model checkers
– automatic proof-based methods very hot
• Use powerful interactive theorem provers
and highly trained staff
– for example Harrison’s work at Intel on floating
point algorithms
Model Checking
G(p -> F q)
yes
property
MC
no
p
q
finite-state model
algorithm
p
q
counterexample
(Ken McMillan)
Model checkers usually based on
BDDs
• Binary Decision Diagrams
• Data structure for representing and
manipulating boolean functions
• More later...
Proof-based method
High level
requirements
High level
design
Compilation
Logical
formula
Compilation
Proof
Logical
formula
Interactive theorem proving
• Formalise system and requirements in a
suitable logical language
• Gradually construct a proof that the system
meets the requirements
– Computer checks all steps
• Slow, expensive, divorced from production
• Sometimes the only way!
• HOL, PVS, Coq, Isabelle ....
Refinement
•
•
•
•
Formal method used during design
Start with abstract specification
Decompose into communicating parts
Refine parts, adding details, and check each
step (proofs)
• stop at components that are already
implemented
• B method (Paris Metro driverless train)
Concentrate on hardware
• An easier application for formal methods
• Price of getting it wrong is high!
• Stronger tradition of analysis methods (e.g.
use of boolean algebra in synthesis, need to
do ATPG)
Nov. ’94 Intel FPU bug
• 824633702441.0 times (1/824633702441.0)
= 0.99999999274709702
• Fault in look-up table
• COST $475.000.000
$15 per transistor!!
• Answer ?? IP blocks and system level
design language
• ”We are heading for a brick wall”
• ”We can’t fill the fabs”
• ”A first requirement is a formal semantics”
Interactive methods
• Hawk (Haskell in top level design of
pipelined superscalar processors, OGI/Intel)
• IBM and AMD both do processor
verification using the interactive theorem
prover ACL2
Automatic methods
• Finite state
• BDD based verification widespread
– emphasison cost saving
– not on guaranteed correctness
– used in production 50% verification engineers
Binary Decision Diagrams
•
•
•
•
•
Idea from 70s (maybe earlier)
Adapted by Bryant ’86
Take a formula
Make decision tree for fixed variable order
Reduction rules
– merge duplicate nodes
– both children point to same node -- remove
redundant node
Plus points
• Efficient algorithms exits (and, or, not,
exists, forall …)
• For given variable order, BDD is canonical
• Many common functions have small BDDs
Minus points
• Some functions are exponential
(independent of variable ordering)
– multipliers 16 by 16 bit around 3.300 Mbytes
• Variable order essential
– change order : linear to exponential
– packages use dynamic reordering
• Injecting error can cause BDD to explode
Exercise
• Make BDD for
x xor y
xor
z
Rest of lecture
• Some selected BDD based methods (Alan
Hu paper)
• What actually happens at Intel
• A glimpse of our research
Combinational equivalence
checking
• Build BDDs of outputs in terms of (same)
primary inputs. Build up gradually and just
compare
• Even for suitable circuits, limit is a few
hundred primary inputs -- need tricks
Symbolic simulation
– Constants 1 0
– unknown
X
– symbolic values a,b,c…
• Adapt logic simulation to represent values
on wires
• BDDs represent functions of symbolic
values
• X halves # simulation runs but loses info.
• a halves # runs but makes BDDs bigger
• Tradeoff
• See also Lava, ACL2 (Rockwell)
Sequential equivalence checking
• Compare sequential circuits by symbolic
simulation (regard as finite state machines)
• Is out always high (safety property) for all
reachable states?
=
out
&
=
Compute reachable states
1 Set of states as BDD
– ex. 3 bool vars (one per latch)
– a + b represents {100,101,110,111,010,011}
–T
represents all 8 states
2 Image (applying the transition relation R)
– AND (BDDs for present state and R)
– Existentially quantify out vars for primary
inputs and present state
• Fixed point iteration
– R0 = BDD for reset state
– R1 = R0 + Image(R0)
–…
– R(i+1) = Ri + Image(Ri)
• Ri set of states reachable in i or fewer clock ticks
• Eventually Ri = R(i+1)
• Copes with ~200 latches
Model checking
• Clarke/Emerson/Sistla et al ’83
• Express properties in temporal logic
• Check if state machine satisfies property
– AG EF (reset)
– AG (req => AF ack)
• Generalisation of reachability analysis
• Same limits
Symbolic Trajectory Evaluation
• Symbolic simulation + temporal stuff
• Limit expressiveness >> automation
• Trajectory formula
– can specify values of circuit nodes for bounded
# of events into the future
– no negation or disjunction
• Unique symbolic simulation vector captures
all behaviours satifying formula >> one run
gives verification
• Problem is writing down the necessary
specifications in this funny language
• Too many symbolic variables >> BDD
blowup
• Can instead use a SAT solver (e.g. Recent
work at Compaq by Bjesse from our group)
General problem
• BDD blowup
– verify subsystems (eg Ericsson)
– use abstractions (ie verify a simplified and
smaller version)
• Still, BDD based verification very
successful!
• Alternative is SAT based methods (our
speciality) or combinations of methods
Large scale hardware verification
at Intel
• Formal verification methodology for
datapath-dominated hardware
• Algorithmic developments in basic tools not
enough
• Need a systematic approach to organising
activities in large scale verification
Forte: a formal verification
environment
• Efficient model checker (STE)
• Lightweight theorem prover
• Interfaced to and tightly integrated with FL,
a general purpose functional programming
language
• FL is both specification language and
scripting language
Phases
1 Understanding the circuit and its operating
environment
– FL circuit description (API)
2 Simple checking of circuit against
specification
– functional spec., improved circuit API, concrete
test vectors for regression testing
Phases
3 STE
– improved specification, detailed info. for model
checker, characterisation of parts of input space
for which MC works
– all of the above are FL programs
– most bugs found in this phase
Theorem proving
4 Check correctness of specification and
soundness of decomposition into MC cases
– Final functional specification, perhaps proofs of
properties of the specification
– top-level correctness statement, collection of
MC runs and a mechanized proof conneting
these two
Results
•
•
•
•
Used in production (large scale)
Use of a functional language vital
Stresses usability (but more work needed)
Aims at reuse of proofs
• Similar methods used at Motorola
Formal methods at Chalmers
• Lava: an FPGA design system based on the
functional progamming language Haskell
– state of the art formal verification methods
combined with advanced programming
language features
– Haskell used as scripting language
– a version that gives fine control of layout
developed and used at Xilinx Inc.
– interesting for prototyping on FPGA
Butterfly Layout on an FPGA
Shameless advertising
• Course in LP4
• Hardware description and verification
– What is a HDL?
– VHDL + model checking
– Lava (Haskell plus automatic verification)
Future Trends
• Design methods and coding rules that make
necessary proofs easier
• Combining automatic verification methods
using simple theorem provers
• Combining test and formal verification