Professor, School of Computing
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.