Friday, February 08, 2008

Prestigious Turing Award presented for Model Checking

Dr. Dobb's Journal: 2007 Turing Award Winners Announced gives details on the recipient of the annual Turing Award, one of the most prestigious awards in Computer Science. It's nice to see an EDA field being so recognized-- I've always admired the complexity of EDA problems and the intellectual power harnessed to solve them.

My impression is that Model Checking is still a nascent field of EDA, yet these guys invented it way back in the early 1980s! Talk about a long gestation period.

Has their work directly gone into any current-day EDA tools? Is there a rightful heir to this seminal innovation?


Nick said...

Hi John,
The problem that has plagued model checking is state space explosion.

BDD/symmetry/partial reduction have been used to reduce the complexity of the problem. These techniques are used in symbolic model checking (SMC)

SMC reduces complexity and allows large sized FSM's from synthesizable verilog designs to be verified.

Some commericial tools which make use of symbolic model checking are:

1. Incisive formal verifier
2. synopsys Magellan
3. 0-In formal verification

An assertion verifier + a model checking engine can serve as a good input to a modern day [automatic test bench generator ]which can be used to find corner case bugs in huge Finite state machines.


John said...

Thanks Nick! Very helpful explanation and thanks for the pointer to present-day Model Checkers.