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?
2 comments:
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.
Nick
www.cad-for-vlsi.blogspot.com)
Thanks Nick! Very helpful explanation and thanks for the pointer to present-day Model Checkers.
Post a Comment