Overview of Formal
Verification
S. Ramesh
CSE Dept.
IIT Bombay
The E-world
Computers everywhere
wristwatches, washing machines,
microwave ovens,
elevators, mobile telephones, printers,
FAX machines, Telephone exchanges,
automobiles, aircrafts
An average home in developed
countries
has one general purpose desktop PC
but dozens of embedded systems.
Safety-critical Systems
Aircrafts, Trains,
Nuclear & Industrial Plants, Avionics
Life Support Systems
Quality of Computational Systems
= Quality of life
Bugs are costly
Pentium bug
Intel Pentium chip, released in 1994 produced error in
floating point division
Cost : $475 million
ARIANE Failure
In December 1996, the Ariane 5 rocket exploded 40
seconds after take off . A software components threw an
exception
Cost : $400 million payload.
Therac-25 Accident :
A software failure caused wrong dosages of x-rays.
Cost: Human Loss.
Rigorous V&V Essential
What is Verification?
Process of ensuring system behaves as
intended
System is bug-free
Functional Correctness
Important Step
Nearly 70% of development time
Classification
Design Verification
Design or Coding errors
Specification bugs
Simulation and Formal Verification
Implementation Testing
Translation/Synthesis Errors
Fabrication defects
Traditional Design
Verification
Testing & Simulation
Reviews & Walkthroughs
Inadequate for safety-critical systems
Detects presence of bugs not
absence
Late Detection of bugs
When to stop testing
Coverage criteria
~70% of time
Testing/Simulation
Run (model of the) system with test vectors
Models at various levels
HLL, behavioral, State Machines, RTL, Gate level
(HW)
Functional and Delay models for timing
verification
Various Issues
What are the test vectors ?
Choose those that reveal the features or lack of them
Corner cases, boundary conditions
Issues in Simulation
How to generate vectors ?
Based upon specification
designer’s understanding
Random vectors
How to evaluate simulation results ?
Use Golden Model
Use specifications
When to stop simulating ?
Statement, condition and state coverage of
the model
Feature coverage over specification
Time to market
Simulation
Widely used validation technique
Many powerful commercial simulators
Many speed-up techniques – FPGA based
hardware emulators
Many simulations aids – assertion checkers
and event monitors
Many automatic tools for test bench
creation
Specman (Verisity), Vera (synopsys)
automatic generation of tests, monitors,
functional models, scoreboards
Coverage analysis tools
Problems in simulation
Simulation is slow, requires billions of
vectors for large designs
Exhaustive simulation infeasible
Coverage of design functionality
unknown
Correctness of golden model suspect
Bugs lurk deep in designs that get
revealed after complex input
sequences
Formal Methods
More rigorous approach
Founded on Mathematical methods
Proves correctness of Systems
Increased confidence
Early Detection of bugs
Design Verification
Complementary to traditional
techniques
Formal Verification
Formally check a formal model of the system
against a formal specification
Formal : Mathematical, Precise, unambiguous
Static analysis
No test vector
Exhaustive Verification
Proves absence of bugs
Complex and subtle bugs caught
Early Detection
Three-step process
Three steps are
Formal Specification
Formal Models
Verification
Formal specification
Precise statement of properties
System requirements and environmental
constraints
Logic - PL, FOL, temporal logic
Automata, labeled transition systems
Other steps
Models
Flexible to model general to specific
designs
Non-determinism, concurrency, fairness,
HLL, Transition systems, automata
Verification
Checking that model satisfies
specification
Static and exhaustive checking
Automatic or semi-automatic
An Example (Academic)
function gcd(x,y)
{
\*assume: x > 0 & y >0 & x=a & y=b
*\
while (x<>y)
{ if x>y then x=x-y else y=y-x
}
\*assert: gcd(x,y) = gcd(a,b) */
}
GCD Example (contd.)
Specification
Assume and Assert Conditions
environment constraints and requirements
Model
HLL code with precise semantics
Verification
Symbolic Execution
Theorem Proving
An Industrial Example
struct RCD3_data { double X, Y; };
void get_inputsXY(struct RCD3_data *final_data)
{ ret1 = read_from_reg( 1, &InputX );
/*postfunc ( InputX >= 0 /\ InputX <= 4095 ) end*/
change_to_v(InputX, input_src, &tempX );
/*assert !(tempX < 0 \/ tempX > 5) end*/
final_data->X= tempX;
convert_to_d(1, tempX, final_data);
/*post (#X final_data >= -180) /\ (#X final_data <= 180)
end*/
}
An abstract Design
example
3- floor elevator controller,
Si - in floor i
ri - request from floor I
U,d – up or down movement
Lift Controller (contd.)
Specification
When the lift is in motion door is closed
Every call is eventually attended
The lift is busy attending one of the
requests
Safety and Liveness Properties
Verification
State space exploration
Model Checking
Automatic
Third Example
Specification:
sum := (x y) cin
cout := (x y) ((x y) cin)
Full Adder (Contd.)
Model
Boolean expression corr.
implementation of full adder
Verification
Comparision of boolean expressions
Equivalence Checking
Theorem Proving, in general
Some Observations
Precise statement of requirements
and constraints
Nothing in the head, one has to
commit
No ambiguity, no escape
Precise description of Designs
Algorithmic or semi-automatic and
rigorous techniques for verification
Observation (contd.)
Verification fails
Specification can be wrong or
incomplete
Design could be too abstract
Design is buggy and hence does not
satisfy the specification
Verification succeeds
if specification is trivial
if specification derived from code
if design meets specification
Formal Specification
Thorough review of Specification
essential
Specification independent of
design
Additional Step
Better done before the design
starts
Further Observation
FV complicates the problem
Creates more work
No, not at all
Traditional approaches ignores
FV unearths the inherent problems
Definitely more work
High quality does not come free!
Formal Verification
Techniques
Three major techniques
Equivalence checking (HW)
Model checking(HW & SW)
Theorem proving(HW & SW)
Equivalence Checking
Checking equivalence of two similar circuits
Useful for validating optimizations, scan
chain insertions
Comparison fo two boolean expressions – use
of BDDs
Highly automatic and efficient
Most used formal Verification technique
Commercial tools :
Design VERIFYer (Chrysalis Inc.)
Formality (Synopsis, million gates in less than an
hour)
V-Formal
Model Checking
Another promising automatic technique
Checking design models against specification
Specifications temporal properties and
environment constraints; use of temporal logic
or automata
Design models are automata or HDl sub sets
Checking is automatic and bug traces
Very effective for control-intensive designs and
Protocols
Many Commercial and academic tools:
Spin (Bell Labs.), Formal-Check (Cadence), VIS
(UCB), SMV (CMU, Cadence)
In-house tools: Rule Base (IBM), Intel, SUN,
Theorem Proving
Most Powerful technique
Specification and design are logical
formulae
Checking involves proving a theorem
Semi-automatic
High degree of human expertise
required
Mainly confined to academic
Number of public domain tools
Nqthm, STeP, PVS, HOL
Formal verification
(experiences)
• Very effective for small control-intensive
designs-blocks of hundreds of latches or
state bits
• Many subtle bugs have been caught in
designs cleared by simulation or testing
• Strong theoretical foundation
• High degree of confidence
• Holds a lot of promise
• Requires a lot more effort and expertise
• Large designs need abstraction
• Many efforts are underway to improve
Systems verified
Various microprocessors (instruction level
verification):
DLX pipelined architectures, AAMP5 (avionics
applications), FM9001 (32 bit processor), PowerPC
Floating point units:
SRT division (Pentium), recent Intel ex-fpu, ADK
IEEE multiplier, AMD division
Multiprocessor coherence protocols
SGI, sun S3.Mp architectures, Gigamax, futurebus+
Memory subsystems of PowerPC
Fairisle ATM switch core
Challenges of formal
verification
Complexity of verification
Automatic for finite state systems
(HW, protocols)
Semi-automatic in the general case of
infinite state systems (software)
State explosion problem
Symbolic model checking
Compositional reasoning
Localization Reduction (FormalCheck)
Partial Order Reduction (Spin)
References
E.M. Clarke, O. Grumberg and D. Peled, Model
Checking, MIT Press, 1999.
C. Kern and M.R. Greenstreet, Formal
Verification in Hardware Design: A Survey,
ACM TODAES, 1999.
R. Kurshan, Computer - Aided Verification of
Co-ordinating Processes, Princeton Univ.Press,
1994
Z. Manna and A. Pnueli, Temporal
Specification and Verification of Reactive
Systems Vol. I and II, Springer 1995.
K. L. McMillan, Symbolic Model Checking,
Kluwer 1993.
Important web-sites:
http://www.comlab.ox.ac.uk/archive/formal-
methods.html
http://www.csl.sri.com
http://dimacs.rutgers.edu/workshops/syla
tutorials/program.html
http://www-cad.eecs.Berkeley.edu/ vis
http://godel.ece.utexas.edu/texas97-
benchmarks
http://www.cfdvs.iitb.ac.in
