dsad

Overview of Formal Verification : 

Overview of Formal Verification S. Ramesh CSE Dept. IIT Bombay

The E-world : 

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 : 

Safety-critical Systems Aircrafts, Trains, Nuclear & Industrial Plants, Avionics Life Support Systems Quality of Computational Systems = Quality of life

Bugs are costly : 

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? : 

What is Verification? Process of ensuring system behaves as intended System is bug-free Functional Correctness Important Step Nearly 70% of development time

Classification : 

Classification Design Verification Design or Coding errors Specification bugs Simulation and Formal Verification Implementation Testing Translation/Synthesis Errors Fabrication defects

Traditional Design Verification : 

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 : 

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 : 

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 : 

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 : 

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 : 

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 : 

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-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 : 

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) : 

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.) : 

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 : 

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 : 

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.) : 

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 : 

Third Example Specification: sum := (x Å y) Å cin cout := (x Ù y) Ú ((x Å y) Ù cin)

Full Adder (Contd.) : 

Full Adder (Contd.) Model Boolean expression corr. implementation of full adder Verification Comparision of boolean expressions Equivalence Checking Theorem Proving, in general

Some Observations : 

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.) : 

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 : 

Formal Specification Thorough review of Specification essential Specification independent of design Additional Step Better done before the design starts

Further Observation : 

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 : 

Formal Verification Techniques Three major techniques Equivalence checking (HW) Model checking(HW & SW) Theorem proving(HW & SW)

Equivalence Checking : 

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 : 

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, Bingo (Fujitsu), etc

Theorem Proving : 

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) : 

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 : 

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

State of the art : 

State of the art ~ 500 registers (5K latches and 1000 combinational variables Equivalence checking : ~ million gates designs Simulation : million gates capacity Various tools available Intel, Fujitsu, IBM, Motorola have in-house tools Commercial tools Abstracts HW (check-off of Siemanns), chrysalis, Formal Check, Vformal, frontline, view logic. Public domain tools: SMV, VIS, STE, SPIN, PVS, STeP, HOL

Challenges of formal verification : 

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 : 

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: : 

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