Associate Professor of Computer Science
Ph.D., State University of New York at Stony Brook, 1986
Professor Gopalakrishnan's research is
in formal methods and self-timing.
Formal methods help build reliable computing systems through
powerful verification methods that unearth insidious bugs,
help improve the quality of the documentation, and offer
a reliable starting point for product upgrades.
The focus of our Utah Verifier group has been on verification,
and our recent results include a systematic method
for decomposing proofs of pipelined processors,
formalization and analysis of transaction ordering problems in
I/O systems, efficient partial order reduction algorithms
incorporated into new model-checkers, and
a model-checking method for verifying shared memory systems.
Self-timing contributes to the robustness of operation of
very large-scale integrated (VLSI) digital systems
through increased reliance on explicit completion sensing
as well as control orchestration through handshake signals.
Our focus has been to develop a tool-path called ACK
(asynchronous circuit compiler) to synthesize self-timed systems
consisting of data-paths and controllers,
and also develop efficient programmable self-timed
controllers based on microprogramming.
Professor Gopalakrishnan was a general co-Chair of the Internal Symposium
on Formal Methods in Computer-Aided Design (FMCAD) in November 1998
and of the International Symposium on Advanced Research in
Asynchronous Circuits and Systems (Async) in November 1994.
He is a member of IFIP WG 10.5 that coordinates as well as sponsors
conferences in design automation and verification.
Generally, he teaches applied theory classes as well as special topics
classes in design automation of hardware.
- Hans M. Jacobson and Ganesh Gopalakrishnan,
``Application-Specific Programmable Control for High-Performance
Asynchronous Circuits'',
Invited Paper, Proceedings of IEEE, Vol. 87, No. 2,
Feb 1999, pp. 319-331.
- Ratan Nalumasu and Ganesh Gopalakrishnan,
``Deriving Efficient Cache Coherence Protocols Through Refinement'',
Formal Methods in System Design (Kluwer). Special
issue on Unity. To appear.
- Ravi Hosabettu, Mandayam Srivas, and Ganesh Gopalakrishnan,
``Proof of Correctness of a Processor with
Reorder Buffer using the Completion
Functions Approach'',
Computer Aided Verification, 11th International Conference, CAV'99,
Trento, Italy, July 7-10, 1999. pp. 47-59.
- Ratan Nalumasu, Rajnish Ghughal, Abdel Mokkedem, and Ganesh
Gopalakrishnan,
``The `Test Model-checking' Approach to the Verification of Formal
Memory Models of Multiprocessors'',
Computer Aided Verification, 10th International Conference, CAV'98,
Vancouver, B.C., Canada, June/July 1998, Proceedings. Alan
J. Hu and Moshe Y. Vardi (editors). Springer-Verlag LNCS 1427.
pp. 464-476.
- Ganesh Gopalakrishnan and Phillip Windley, editors. Formal Methods
in Computer-Aided Design.
Proceedings of the 2nd International Conference, FMCAD '98. Lecture Notes in Computer
Science 1522, Springer-Verlag, 1998, 538 pages. ISSN 0302-9743.
