1.1. Formal Verification

Verification is a Major bottleneck in design flow. It consumes upto 75% of the overall design cost and effort. This is why several (Formal) methods have been proposed in recent times as alternatives to classical simulation to speed up the process.

We can split up Formal techniques into different categories like

1. Equivalence checking (EC)
2. Property Checking
3. Symbolic simulation

The development/application of various tools using these techniques accelerates the process of verification and also points out numerous weaknesses and bugs of these techniques (especially on complex arithmetic ckts like Multipliers) on industrial scale designs to CAD developers :)

The state of the art formal tools make use of..

1. BDD (Binary Decision Diagrams)
2. SAT (Boolean SATisfiability)
3. ATPG (Automatic Test Pattern Generation)
4. Model Checking (MC), Bounded Model Checking (BMC, for large ckts)
5. Symbolic Simulation
6. Random Simulation
7. Term rewriting
8. Word level approaches like Binary Moment Diagrams (BMD's).

Most industrial quality formal tools make use of more than 3-4 (Multi-engine approaches!) of the above mentioned techniques which often work orthogonally (tough to combine!) to solve the verification problem at hand.

Formal techniques are not only popular these days for digital circuts but are gaining immense popularity in proving Linear/NonLinear analog systems as well.

I will discuss equivalence checking next..